diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index f2915acc..176e671a 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -261,8 +261,8 @@ jobs: - name: Set up CBMC runner uses: FreeRTOS/CI-CD-Github-Actions/set_up_cbmc_runner@main with: - cbmc_version: "5.61.0" - cbmc_viewer_version: "3.5" + cbmc_version: "5.95.1" + cbmc_viewer_version: "latest" - name: Install cmake run: | sudo apt-get install -y cmake diff --git a/test/cbmc/proofs/C_CreateObject/Makefile b/test/cbmc/proofs/C_CreateObject/Makefile index cce61508..d987f12f 100644 --- a/test/cbmc/proofs/C_CreateObject/Makefile +++ b/test/cbmc/proofs/C_CreateObject/Makefile @@ -25,6 +25,8 @@ MAX_LABEL_SIZE=32 # Should be one more than the total number of objects in the PKCS stack. MAX_OBJECT_NUM=2 +CBMC_OBJECT_BITS=9 + DEFINES += -DTEMPLATE_SIZE=$(TEMPLATE_SIZE) DEFINES += -DTEMPLATE_ATTRIBUTE_MAX_SIZE=$(TEMPLATE_ATTRIBUTE_MAX_SIZE)