[Individual PRs to follow] C++ standard support: C++11 through C++26 parser, type-checker, and STL improvements

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

@@ -8,6 +8,10 @@ env:
   cvc5-version: "1.2.1"
   linux-vcpus: 4
   windows-vcpus: 4
+  # Per-test virtual memory limit (KB) for test.pl.
+  # CI runners have ~10 GB RAM; with 4 parallel jobs, each test
+  # gets ~2.5 GB. This prevents OOM kills from masking real failures.
+  CBMC_TEST_MEMLIMIT: 2500000
 
 jobs:
   # This job takes approximately 15 to 40 minutes
@@ -24,7 +28,7 @@ jobs:
           DEBIAN_FRONTEND: noninteractive
         run: |
           sudo apt-get update
-          sudo apt-get install --no-install-recommends -yq gcc gdb g++ maven jq flex bison libxml2-utils ccache cmake z3
+          sudo apt-get install --no-install-recommends -yq gcc gdb g++ maven jq flex bison libxml2-utils ccache cmake z3 clang libc++-dev libc++abi-dev
       - 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
@@ -109,7 +113,7 @@ jobs:
           DEBIAN_FRONTEND: noninteractive
         run: |
           sudo apt-get update
-          sudo apt-get install --no-install-recommends -yq clang-19 clang++-19 gdb maven jq flex bison libxml2-utils cpanminus ccache z3
+          sudo apt-get install --no-install-recommends -yq clang-19 clang++-19 gdb maven jq flex bison libxml2-utils cpanminus ccache z3 libc++-dev libc++abi-dev
           make -C src minisat2-download cadical-download
           cpanm Thread::Pool::Simple
       - name: Confirm z3 solver is available and log the version installed
@@ -181,7 +185,7 @@ jobs:
           DEBIAN_FRONTEND: noninteractive
         run: |
           sudo apt-get update
-          sudo apt-get install --no-install-recommends -yq clang-19 clang++-19 gdb maven jq flex bison libxml2-utils cpanminus ccache z3
+          sudo apt-get install --no-install-recommends -yq clang-19 clang++-19 gdb maven jq flex bison libxml2-utils cpanminus ccache z3 libc++-dev libc++abi-dev
           make -C src minisat2-download
           cpanm Thread::Pool::Simple
       - name: Confirm z3 solver is available and log the version installed
@@ -222,7 +226,7 @@ jobs:
           DEBIAN_FRONTEND: noninteractive
         run: |
           sudo apt-get update
-          sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc gdb g++ maven flex bison libxml2-utils dpkg-dev ccache doxygen graphviz z3
+          sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc gdb g++ maven flex bison libxml2-utils dpkg-dev ccache doxygen graphviz z3 clang libc++-dev libc++abi-dev
       - 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
@@ -299,7 +303,7 @@ jobs:
           DEBIAN_FRONTEND: noninteractive
         run: |
           sudo apt-get update
-          sudo apt-get install --no-install-recommends -yq clang clang-14 gdb maven jq flex bison libxml2-utils cpanminus ccache z3
+          sudo apt-get install --no-install-recommends -yq clang clang-14 gdb maven jq flex bison libxml2-utils cpanminus ccache z3 libc++-dev libc++abi-dev
           make -C src minisat2-download cadical-download
           cpanm Thread::Pool::Simple
       - name: Confirm z3 solver is available and log the version installed
@@ -368,7 +372,7 @@ jobs:
           DEBIAN_FRONTEND: noninteractive
         run: |
           sudo apt-get update
-          sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc gdb g++ maven flex bison libxml2-utils dpkg-dev ccache doxygen graphviz z3
+          sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc gdb g++ maven flex bison libxml2-utils dpkg-dev ccache doxygen graphviz z3 clang libc++-dev libc++abi-dev
       - 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
@@ -422,7 +426,7 @@ jobs:
           DEBIAN_FRONTEND: noninteractive
         run: |
           sudo apt-get update
-          sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc-14 gdb g++-14 maven flex bison libxml2-utils dpkg-dev ccache doxygen z3
+          sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc-14 gdb g++-14 maven flex bison libxml2-utils dpkg-dev ccache doxygen z3 clang libc++-dev libc++abi-dev
           # Update symlinks so that any use of gcc (including our regression
           # tests) will use GCC 14.
           sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-14 110 \
@@ -475,7 +479,7 @@ jobs:
           DEBIAN_FRONTEND: noninteractive
         run: |
           sudo apt-get update
-          sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc gdb g++ maven flex bison libxml2-utils dpkg-dev ccache doxygen graphviz z3
+          sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc gdb g++ maven flex bison libxml2-utils dpkg-dev ccache doxygen graphviz z3 clang libc++-dev libc++abi-dev
       - 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
@@ -529,7 +533,7 @@ jobs:
           DEBIAN_FRONTEND: noninteractive
         run: |
           sudo apt-get update
-          sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc gdb g++ maven flex bison libxml2-utils ccache doxygen z3 g++-multilib
+          sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc gdb g++ maven flex bison libxml2-utils ccache doxygen z3 g++-multilib clang libc++-dev libc++abi-dev
       - 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
@@ -576,7 +580,7 @@ jobs:
           DEBIAN_FRONTEND: noninteractive
         run: |
           sudo apt-get update
-          sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc g++ maven flex bison libxml2-utils ccache z3
+          sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc g++ maven flex bison libxml2-utils ccache z3 clang libc++-dev libc++abi-dev
       - name: Prepare ccache
         uses: actions/cache@v5
         with:
@@ -623,7 +627,7 @@ jobs:
           DEBIAN_FRONTEND: noninteractive
         run: |
           sudo apt-get update
-          sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc g++ maven flex bison libxml2-utils ccache z3
+          sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc g++ maven flex bison libxml2-utils ccache z3 clang libc++-dev libc++abi-dev
       - name: Prepare ccache
         uses: actions/cache@v5
         with:
@@ -698,6 +702,31 @@ jobs:
           ./unit_tests "[z3]"
       - name: Run JBMC unit tests
         run: cd jbmc/unit; ./unit_tests
+      - name: Preprocess libc++ headers for debugging
+        if: always()
+        run: |
+          mkdir -p macos-preprocessed
+          cbmc=src/cbmc/cbmc
+          for hdr in vector iterator; do
+            echo "#include <$hdr>" > pp_$hdr.cpp
+            echo "int main() {}" >> pp_$hdr.cpp
+            $cbmc --cpp11 --preprocess pp_$hdr.cpp > macos-preprocessed/$hdr.ii 2>/dev/null || true
+          done
+          # Preprocess failing test programs
+          for t in Address_of_Method1 Vector1 STL1 STL2 cpp11_vector_size cpp17_any_basic cpp20_coroutine_types; do
+            src="regression/cbmc-cpp/$t/main.cpp"
+            if [ -f "$src" ]; then
+              flags=$(sed -n '3p' "regression/cbmc-cpp/$t/test.desc")
+              $cbmc $flags --preprocess "$src" > "macos-preprocessed/test_$t.ii" 2>/dev/null || true
+            fi
+          done
+      - name: Upload preprocessed headers
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: macos-preprocessed-headers
+          path: macos-preprocessed/
+          retention-days: 7
       - name: Run regression tests
         run: |
           export PATH=$PATH:`pwd`/src/solvers
@@ -826,10 +855,55 @@ jobs:
       - name: Print ccache stats
         run: clcache -s
       - uses: ilammy/msvc-dev-cmd@v1
-      - name: Test cbmc
+      - name: Preprocess MSVC headers for debugging
+        if: always()
+        run: |
+          New-Item -ItemType Directory -Force -Path msvc-preprocessed
+          $cbmc = "build\bin\Release\cbmc.exe"
+          foreach ($hdr in @("tuple", "string_view", "variant", "any", "string", "map", "optional", "vector", "list", "set", "thread", "mutex", "filesystem", "chrono", "valarray", "iostream", "memory", "functional")) {
+            $src = "#include <$hdr>`nint main() {}"
+            $src | Set-Content "pp_$hdr.cpp"
+            & $cbmc --cpp17 --preprocess "pp_$hdr.cpp" 2>$null | Set-Content "msvc-preprocessed\$hdr.ii"
+          }
+          foreach ($hdr in @("array", "numeric")) {
+            $src = "#include <$hdr>`nint main() {}"
+            $src | Set-Content "pp_${hdr}_20.cpp"
+            & $cbmc --cpp20 --preprocess "pp_${hdr}_20.cpp" 2>$null | Set-Content "msvc-preprocessed\${hdr}_cpp20.ii"
+          }
+          # Preprocess all cbmc-cpp test programs that fail on MSVC
+          $tests = @(
+            "STL1", "STL2", "Vector1",
+            "cpp11_condition_variable_header", "cpp11_future_header",
+            "cpp11_map_insert", "cpp11_map_verify", "cpp11_set_insert",
+            "cpp11_shared_ptr", "cpp11_vector_front_body",
+            "cpp11_vector_probe", "cpp11_vector_push_back",
+            "cpp11_vector_pushback", "cpp11_vector_verify",
+            "cpp14_chrono_basic", "cpp17_filesystem_basic",
+            "cpp17_filesystem_path_ops", "cpp17_mutex_basic",
+            "cpp17_numeric_basic", "cpp17_shared_ptr",
+            "cpp17_string_view", "cpp17_string_view_basic",
+            "cpp17_thread_basic", "cpp17_valarray_basic",
+            "cpp17_vector_basic", "cpp20_iostream_basic"
+          )
+          foreach ($t in $tests) {
+            $src = "regression\cbmc-cpp\$t\main.cpp"
+            if (Test-Path $src) {
+              $flags = (Get-Content "regression\cbmc-cpp\$t\test.desc" | Select-Object -Index 2).Trim()
+              & $cbmc $flags.Split(" ") --preprocess $src 2>$null | Set-Content "msvc-preprocessed\test_$t.ii"
+            }
+          }
+      - name: Upload preprocessed headers
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: msvc-preprocessed-headers
+          path: msvc-preprocessed/
+          retention-days: 7
+      - name: Run tests
         run: |
           Set-Location build
-          ctest -V -L CORE -C Release . -j${{env.windows-vcpus}}
+          $env:CBMC_TEST_MEMLIMIT = "3000000"
+          ctest -V -L CORE -C Release . -j${{env.windows-vcpus}} --timeout 600
 
   # This job takes approximately 65 to 84 minutes
   check-vs-2022-make-build-and-test:
@@ -928,7 +1002,9 @@ jobs:
           make CXX=clcache BUILD_ENV=MSVC -C unit test TAGS="[z3]"
           make CXX=clcache BUILD_ENV=MSVC -C jbmc/unit test
       - name: Run CBMC regression tests
-        run: make CXX=clcache BUILD_ENV=MSVC -j${{env.windows-vcpus}} -C regression test-parallel-jobs
+        run: |
+          $env:CBMC_TEST_MEMLIMIT = "3000000"
+          make CXX=clcache BUILD_ENV=MSVC -j${{env.windows-vcpus}} -C regression test-parallel-jobs
 
   # This job takes approximately 7 to 32 minutes
   windows-msi-package:
@@ -1002,6 +1078,52 @@ jobs:
           echo "msi_installer=build/$msi_name" >> $env:GITHUB_OUTPUT
           echo "msi_name=$msi_name" >> $env:GITHUB_OUTPUT
 
+  # This job takes approximately 10 to 15 minutes
+  check-dogfood-goto-cc:
+    # Compile a curated sample of CBMC's own .cpp files with
+    # goto-cc itself ("dog-fooding"): the baseline is expected to
+    # produce clean goto binaries.  New entries are added to the
+    # baseline as the underlying front-end bugs are fixed.  The
+    # expanded sample is reported for visibility but does not
+    # fail the job.
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@v6
+        with:
+          submodules: recursive
+      - name: Fetch dependencies
+        env:
+          DEBIAN_FRONTEND: noninteractive
+        run: |
+          sudo apt-get update
+          sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc g++ flex bison libxml2-utils ccache python3
+      - name: Prepare ccache
+        uses: actions/cache@v5
+        with:
+          save-always: true
+          path: .ccache
+          key: ${{ runner.os }}-24.04-dogfood-${{ github.ref }}-${{ github.sha }}-PR
+          restore-keys: |
+            ${{ runner.os }}-24.04-dogfood-${{ github.ref }}
+            ${{ runner.os }}-24.04-dogfood
+      - name: ccache environment
+        run: |
+          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
+          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
+      - name: Configure using CMake
+        run: cmake -S . -B build -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -DCMAKE_EXPORT_COMPILE_COMMANDS=1
+      - name: Zero ccache stats and limit in size
+        run: ccache -z --max-size=500M
+      - name: Build goto-cc
+        run: ninja -C build -j${{env.linux-vcpus}} goto-cc
+      - name: Print ccache stats
+        run: ccache -s
+      - name: Run dog-food harness on baseline (gate)
+        run: ./scripts/dogfood_goto_cc.sh --baseline
+      - name: Run dog-food harness on extended sample (report only)
+        continue-on-error: true
+        run: ./scripts/dogfood_goto_cc.sh
+
   # This job takes approximately 2 to 3 minutes
   check-string-table:
     runs-on: ubuntu-latest

AGENTS.md

@@ -30,6 +30,7 @@ formal verification of C and C++ programs.
 ### What CBMC Does
 - Bounded model checking for C/C++ programs
 - Supports C89, C99, most of C11, C17, C23
+- Supports C++98, C++03, C++11, C++14, and C++17
 - Supports most compiler extensions from gcc and Visual Studio
 - Verifies array bounds, pointer safety, exceptions, and user-specified
   assertions