Switch GCC-12 CI job to GCC 13

.github/workflows/pull-request-checks.yaml

@@ -391,7 +391,7 @@ jobs:
         run: cd build; ctest . -V -L CORE -j2
 
   # This job takes approximately 26 to 46 minutes
-  check-ubuntu-22_04-cmake-gcc-12:
+  check-ubuntu-22_04-cmake-gcc-13:
     runs-on: ubuntu-22.04
     steps:
       - uses: actions/checkout@v3
@@ -404,7 +404,13 @@ jobs:
           DEBIAN_FRONTEND: noninteractive
         run: |
           sudo apt-get update
-          sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc-12 gdb g++-12 maven flex bison libxml2-utils dpkg-dev ccache doxygen z3
+          sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc-13 gdb g++-13 maven flex bison libxml2-utils dpkg-dev ccache doxygen z3
+          # Update symlinks so that any use of gcc (including our regression
+          # tests) will use GCC 13.
+          sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-13 110 \
+            --slave /usr/bin/g++ g++ /usr/bin/g++-13 \
+            --slave /usr/bin/gcov gcov /usr/bin/gcov-13
+          sudo ln -sf cpp-13 /usr/bin/cpp
       - name: Confirm z3 solver is available and log the version installed
         run: z3 --version
       - name: Download cvc-5 from the releases page and make sure it can be deployed
@@ -417,29 +423,22 @@ jobs:
         uses: actions/cache@v3
         with:
           path: .ccache
-          key: ${{ runner.os }}-22.04-Release-gcc-12-${{ github.ref }}-${{ github.sha }}-PR
+          key: ${{ runner.os }}-22.04-Release-gcc-13-${{ github.ref }}-${{ github.sha }}-PR
           restore-keys: |
-            ${{ runner.os }}-22.04-Release-gcc-12-${{ github.ref }}
-            ${{ runner.os }}-22.04-Release-gcc-12
+            ${{ runner.os }}-22.04-Release-gcc-13-${{ github.ref }}
+            ${{ runner.os }}-22.04-Release-gcc-13
       - name: ccache environment
         run: |
           echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
           echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
       - name: Configure using CMake
-        run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc-12 -DCMAKE_CXX_COMPILER=/usr/bin/g++-12
-      - name: Check that doc task works
-        run: ninja -C build doc
+        run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release
       - name: Zero ccache stats and limit in size
         run: ccache -z --max-size=500M
       - name: Build with Ninja
         run: ninja -C build -j2
       - name: Print ccache stats
         run: ccache -s
-      - name: Check if package building works
-        run: |
-          cd build
-          ninja package
-          ls *.deb
       - name: Run tests
         run: cd build; ctest . -V -L CORE -j2
 

src/ansi-c/compiler_headers/clang_builtins.py

@@ -43,7 +43,7 @@
         'v': 'void',
         'w': 'wchar_t',
         'x': '_Float16',
-        'y': '_Float16', # would be '__bf16', but we don't support that yet
+        'y': '__bf16',
         'z': '__CPROVER_size_t'
         }
 

src/ansi-c/compiler_headers/gcc_builtin_headers_generic.h

@@ -44,6 +44,7 @@ long __builtin_expect_with_probability(long, long, double);
 void __builtin_clear_padding();
 void __builtin_speculation_safe_value();
 void* __builtin_speculation_safe_value_ptr(void*, ...);
+_Bool __builtin_is_constant_evaluated(void);
 
 void* __builtin_dwarf_cfa();
 unsigned __builtin_dwarf_sp_column();

src/ansi-c/scanner.l

@@ -530,6 +530,12 @@
                     return make_identifier();
                 }
 
+"__bf16"        { if(PARSER.ts_18661_3_Floatn_types)
+                  { loc(); return TOK_GCC_FLOAT16; }
+                  else
+                    return make_identifier();
+                }
+
 "_Float32"      { if(PARSER.ts_18661_3_Floatn_types)
                   { loc(); return TOK_GCC_FLOAT32; }
                   else

src/cpp/parse.cpp

@@ -267,7 +267,7 @@ class Parser // NOLINT(readability/identifiers)
   bool optStorageSpec(cpp_storage_spect &);
   bool optCvQualify(typet &);
   bool optAlignas(typet &);
-  bool rAttribute(typet &);
+  bool rGCCAttribute(typet &);
   bool optAttribute(typet &);
   bool optIntegralTypeOrClassSpec(typet &);
   bool rConstructorDecl(
@@ -852,15 +852,9 @@ bool Parser::rNamespaceSpec(cpp_namespace_spect &namespace_spec)
   // inline namespace __cxx11 __attribute__((__abi_tag__ ("cxx11"))) { }
   // which occurs in glibc. Obviously we need to better than just throw attribs
   // away like this in the future.
-  if(lex.LookAhead(0)==TOK_GCC_ATTRIBUTE)
-  {
-    cpp_tokent tk;
-    lex.get_token(tk);
-
-    typet discard;
-    if(!rAttribute(discard))
-      return false;
-  }
+  typet discard;
+  if(!optAttribute(discard))
+    return false;
 
   switch(lex.LookAhead(0))
   {
@@ -1418,6 +1412,10 @@ bool Parser::rDeclaration(cpp_declarationt &declaration)
   if(!optCvQualify(cv_q))
     return false;
 
+  if(member_spec.is_empty())
+    if(!optMemberSpec(member_spec))
+      return false;
+
   // added these two to do "const static volatile int i=1;"
   if(!optStorageSpec(storage_spec))
     return false;
@@ -2073,7 +2071,7 @@ bool Parser::optCvQualify(typet &cv)
         break;
 
       case TOK_GCC_ATTRIBUTE:
-        if(!rAttribute(cv))
+        if(!rGCCAttribute(cv))
           return false;
         break;
 
@@ -2162,11 +2160,11 @@ bool Parser::optAlignas(typet &cv)
   return false;
 }
 
-bool Parser::rAttribute(typet &t)
+bool Parser::rGCCAttribute(typet &t)
 {
 #ifdef DEBUG
   indenter _i;
-  std::cout << std::string(__indent, ' ') << "Parser::rAttribute "
+  std::cout << std::string(__indent, ' ') << "Parser::rGCCAttribute "
             << lex.LookAhead(0);
 #endif
   cpp_tokent tk;
@@ -2176,7 +2174,7 @@ bool Parser::rAttribute(typet &t)
   {
   case '(':
     if(lex.LookAhead(0)!=')')
-      rAttribute(t);
+      rGCCAttribute(t);
 
     if(lex.LookAhead(0)!=')')
       return false;
@@ -2360,11 +2358,19 @@ bool Parser::rAttribute(typet &t)
   if(lex.LookAhead(0)==')')
     return true;
 
-  return rAttribute(t);
+  return rGCCAttribute(t);
 }
 
 bool Parser::optAttribute(typet &t)
 {
+  if(lex.LookAhead(0) == TOK_GCC_ATTRIBUTE)
+  {
+    lex.get_token();
+
+    if(!rGCCAttribute(t))
+      return false;
+  }
+
   if(lex.LookAhead(0)!='[' ||
      lex.LookAhead(1)!='[')
     return true;
@@ -4487,13 +4493,8 @@ bool Parser::rClassSpec(typet &spec)
     if(!optAlignas(spec))
       return false;
 
-    if(lex.LookAhead(0)==TOK_GCC_ATTRIBUTE)
-    {
-      lex.get_token(tk);
-
-      if(!rAttribute(spec))
-        return false;
-    }
+    if(!optAttribute(spec))
+      return false;
 
     irept name;
 

src/goto-cc/ms_cl_cmdline.h

@@ -19,6 +19,7 @@ Date: June 2006
 class ms_cl_cmdlinet:public goto_cc_cmdlinet
 {
 public:
+  using cmdlinet::parse;
   virtual bool parse(int, const char **);
 
   ms_cl_cmdlinet()

src/goto-cc/ms_link_cmdline.h

@@ -19,6 +19,7 @@ Date: July 2018
 class ms_link_cmdlinet : public goto_cc_cmdlinet
 {
 public:
+  using cmdlinet::parse;
   virtual bool parse(int, const char **);
 
   ms_link_cmdlinet()

src/goto-programs/elf_reader.cpp

@@ -10,8 +10,10 @@ Module: Read ELF
 /// Read ELF
 
 #include "elf_reader.h"
+
 #include <util/exception_utils.h>
 
+#include <cstdint>
 #include <istream>
 
 static void u16_to_native_endian_inplace(bool le_input, uint16_t &input)