diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index ba6a8c166..06e55afcd 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -406,7 +406,7 @@ jobs: - name: Set up CBMC runner uses: FreeRTOS/CI-CD-Github-Actions/set_up_cbmc_runner@main with: - cbmc_version: "5.95.1" + cbmc_version: "6.1.1" - env: stepName: Install Dependencies diff --git a/test/cbmc/proofs/Makefile.template b/test/cbmc/proofs/Makefile.template index 15cf815db..847b0a8f2 100644 --- a/test/cbmc/proofs/Makefile.template +++ b/test/cbmc/proofs/Makefile.template @@ -124,13 +124,13 @@ goto: # report if the proof failed. If the proof failed, we separately fail # the entire job using the check-cbmc-result rule. cbmc.xml: $(ENTRY).goto - -cbmc $(CBMCFLAGS) $(SOLVER) --unwinding-assertions --trace --xml-ui @RULE_INPUT@ > $@ 2>&1 + -cbmc $(CBMCFLAGS) $(SOLVER) --trace --xml-ui @RULE_INPUT@ > $@ 2>&1 property.xml: $(ENTRY).goto - cbmc $(CBMCFLAGS) --unwinding-assertions --show-properties --xml-ui @RULE_INPUT@ > $@ 2>&1 + cbmc $(CBMCFLAGS) --show-properties --xml-ui @RULE_INPUT@ > $@ 2>&1 coverage.xml: $(ENTRY).goto - cbmc $(CBMCFLAGS) --cover location --xml-ui @RULE_INPUT@ > $@ 2>&1 + cbmc $(CBMCFLAGS) --no-standard-checks --malloc-may-fail --malloc-fail-null --cover location --xml-ui @RULE_INPUT@ > $@ 2>&1 cbmc: cbmc.xml diff --git a/test/cbmc/proofs/MakefileCommon.json b/test/cbmc/proofs/MakefileCommon.json index 7ada3e1dc..79e8b7bfb 100644 --- a/test/cbmc/proofs/MakefileCommon.json +++ b/test/cbmc/proofs/MakefileCommon.json @@ -32,9 +32,7 @@ "CBMCFLAGS ": [ "--object-bits 8", - "--32", - "--bounds-check", - "--pointer-check" + "--32" ], "FORWARD_SLASH": ["/"],