Code

Adopt CBMC 6.1 and cbmc-viewer 3.9#4661

Code

Merged

lrstewart merged 54 commits intoaws:mainaws/s2n-tls:mainfrom rod-chapman:cbmc_6_minimalrod-chapman/s2n-tls:cbmc_6_minimalCopy head branch name to clipboardAug 2, 2024

+197-36

Commits

Commits on Jun 25, 2024

• Remove local vsnprintf() function here, since it causes CBMC 6.0.0 to fail

  Show description for 2830362
  rod-chapman

  committed
  2830362

  Copy full SHA for 2830362

• Add s2n_calculate_stacktrace() function to all proofs, and remove --object_bits option for goto-cc 6.0.0

  Show description for 4e5a743
  rod-chapman

  committed
  4e5a743

  Copy full SHA for 4e5a743

• Do NOT remove abort() function - CBMC 6.0.0 objects to its absence, so keep it.

  Show description for 13beb9a
  rod-chapman

  committed
  13beb9a

  Copy full SHA for 13beb9a

• Add CONTRACT_ASSUME and CONTRACT_ASSERT macros

  Show description for 5ca69b0
  rod-chapman

  committed
  5ca69b0

  Copy full SHA for 5ca69b0

• Change __CPROVER_assume to CONTRACT_ASSUME throughout here.

  Show description for b06b855
  rod-chapman

  committed
  b06b855

  Copy full SHA for b06b855

• Add dummy stub function to avoid missing function body on macOS/Darwin CBMC runs

  Show description for 1502b48
  rod-chapman

  committed
  1502b48

  Copy full SHA for 1502b48

• Add missing source file

  Show description for ed73009
  rod-chapman

  committed
  ed73009

  Copy full SHA for ed73009

• Adjust Makefiles to address missing functions reported by CBMC 6

  Show description for fc0c256
  rod-chapman

  committed
  fc0c256

  Copy full SHA for fc0c256

• Rename static/global flag to avoid name clash with same in s2n_libcrypto_is_awslc.c

  Show description for bad1efc
  rod-chapman

  committed
  bad1efc

  Copy full SHA for bad1efc

• Do not remove function that is needed to avoid warning from CBMC 6

  Show description for 1f9460c
  rod-chapman

  committed
  1f9460c

  Copy full SHA for 1f9460c

• Add stub for madvise.c

  Show description for 4d14445
  rod-chapman

  committed
  4d14445

  Copy full SHA for 4d14445

Commits on Jun 26, 2024

• Add stub units required by CBMC 6.0.0

  Show description for 536b8b7
  rod-chapman

  committed
  536b8b7

  Copy full SHA for 536b8b7

• Restore local stub of vsnprintf() for now. Works on Linux, fails on macOS.

  Show description for 9c8c961
  rod-chapman

  committed
  9c8c961

  Copy full SHA for 9c8c961

• Add missing sources and stubs for CBMC 6.0.0

  Show description for 47526fd
  rod-chapman

  committed
  47526fd

  Copy full SHA for 47526fd

• Add one missing stub

  Show description for bf26198
  rod-chapman

  committed
  bf26198

  Copy full SHA for bf26198

• Add one stub needed for verification on Linux

  Show description for f8950e7
  rod-chapman

  committed
  f8950e7

  Copy full SHA for f8950e7

• Merge branch 'aws:main' into cbmc_6_minimal

  rod-chapman

  authored
  62c96ac

  Copy full SHA for 62c96ac

Commits on Jul 15, 2024

• Merge branch 'aws:main' into cbmc_6_minimal

  rod-chapman

  authored
  384cb51

  Copy full SHA for 384cb51

• Increase CBMC_OBJECT_BITS to 10 for CBMC 6.0.1

  Show description for 8d9feb8
  rod-chapman

  committed
  8d9feb8

  Copy full SHA for 8d9feb8

• Remove cbmc_utils.c from PROOF_SOURCES for now - missing functions TBD

  Show description for a37e2b4
  rod-chapman

  committed
  a37e2b4

  Copy full SHA for a37e2b4

Commits on Jul 16, 2024

• Add required sources to Makefile, and correct double-free bug in harness.

  Show description for 177d2dd
  rod-chapman

  committed
  177d2dd

  Copy full SHA for 177d2dd

• Add support for download and install of Z3 in CI to support CBMC 6.1.0 and beyond

  Show description for 71cdb71
  rod-chapman

  committed
  71cdb71

  Copy full SHA for 71cdb71

Commits on Jul 17, 2024

• If vsnprintf is defined as macro (as on macOS), then undef that symbol for CBMC verification

  Show description for fef7f76
  rod-chapman

  committed
  fef7f76

  Copy full SHA for fef7f76

• Add resources and actions to build Bitwuzla

  Show description for 89cfe5a
  rod-chapman

  committed
  89cfe5a

  Copy full SHA for 89cfe5a

• Corrections following dry-run of this script on an Ubuntu 20.04 instance.

  Show description for 046de30
  rod-chapman

  committed
  046de30

  Copy full SHA for 046de30

• Use sudo to install cbmc-viewer so it is on PATH automatically

  Show description for ee2cedb
  rod-chapman

  committed
  ee2cedb

  Copy full SHA for ee2cedb

• Merge branch 'aws:main' into cbmc_6_minimal

  rod-chapman

  authored
  dd1c266

  Copy full SHA for dd1c266

Commits on Jul 18, 2024

• Merge branch 'aws:main' into cbmc_6_minimal

  rod-chapman

  authored
  1355770

  Copy full SHA for 1355770

Commits on Jul 19, 2024

• Merge branch 'aws:main' into cbmc_6_minimal

  rod-chapman

  authored
  20dff74

  Copy full SHA for 20dff74

Commits on Jul 23, 2024

• Correct UNWINDSET for this proof to avoid warning from CBMC

  Show description for 34c3d91
  rod-chapman

  committed
  34c3d91

  Copy full SHA for 34c3d91

• Add COVERFLAGS=--no-standard-checks to restore performance of coverage analysis phase of all proofs

  Show description for 2e13921
  rod-chapman

  committed
  2e13921

  Copy full SHA for 2e13921

• Upgrade to CBMC 6.1.0 for CI runs

  Show description for 0a66c40
  rod-chapman

  committed
  0a66c40

  Copy full SHA for 0a66c40

• Merge branch 'aws:main' into cbmc_6_minimal

  rod-chapman

  authored
  265fabc

  Copy full SHA for 265fabc

Commits on Jul 24, 2024

• Merge branch 'aws:main' into cbmc_6_minimal

  rod-chapman

  authored
  0ded2bd

  Copy full SHA for 0ded2bd

• Correct 2 typos spotted in review by @backphan

  Show description for 17a7cc2
  rod-chapman

  committed
  17a7cc2

  Copy full SHA for 17a7cc2

• Address two review comments from @beckphan

  Show description for b34ef83
  rod-chapman

  committed
  b34ef83

  Copy full SHA for b34ef83

• Correct to use /* comment style not //

  Show description for 229ceba
  rod-chapman

  committed
  229ceba

  Copy full SHA for 229ceba

Commits on Jul 25, 2024

• Merge branch 'aws:main' into cbmc_6_minimal

  rod-chapman

  authored
  5286eb8

  Copy full SHA for 5286eb8

• Attempt to correct PATH setting code for Z3

  Show description for b8dbfb1
  rod-chapman

  committed
  b8dbfb1

  Copy full SHA for b8dbfb1

• Run clang-format on this file to correct layout

  Show description for 921cb97
  rod-chapman

  committed
  921cb97

  Copy full SHA for 921cb97

• Correct syntax for shell commands when adding Z3 to PATH

  Show description for 3f62624
  rod-chapman

  committed
  3f62624

  Copy full SHA for 3f62624

• Correction for new Rust clippy lint

  Show description for 1de1f3e
  rod-chapman

  committed
  1de1f3e

  Copy full SHA for 1de1f3e

Commits on Jul 29, 2024

• Merge branch 'aws:main' into cbmc_6_minimal

  rod-chapman

  authored
  4187f61

  Copy full SHA for 4187f61

• Correction to command that removes z3.zip file.

  Show description for 701e7ab
  rod-chapman

  committed
  701e7ab

  Copy full SHA for 701e7ab

• Try again to correct command to remove z3.zip

  Show description for 6808602
  rod-chapman

  committed
  6808602

  Copy full SHA for 6808602

• Correct commands to add bitwuzla to PATH

  Show description for 87bb1ef
  rod-chapman

  committed
  87bb1ef

  Copy full SHA for 87bb1ef

Commits on Jul 30, 2024

• Merge branch 'aws:main' into cbmc_6_minimal

  rod-chapman

  authored
  1b8b350

  Copy full SHA for 1b8b350

Commits on Jul 31, 2024

• Merge branch 'aws:main' into cbmc_6_minimal

  rod-chapman

  authored
  398f64e

  Copy full SHA for 398f64e

• Remove undef of vsnprintf here. Proof of this unit on macOS will be re-visited in a separate Issue

  Show description for b694f05
  rod-chapman

  committed
  b694f05

  Copy full SHA for b694f05

Commits on Aug 1, 2024

• Merge branch 'aws:main' into cbmc_6_minimal

  rod-chapman

  authored
  660d4fb

  Copy full SHA for 660d4fb

• Merge branch 'main' into cbmc_6_minimal

  lrstewart

  authored
  e4b76a3

  Copy full SHA for e4b76a3

Commits on Aug 2, 2024

• Merge branch 'aws:main' into cbmc_6_minimal

  rod-chapman

  authored
  edfa9f7

  Copy full SHA for edfa9f7

• Add missing stubs to satisfy CBMC 6.1 for these proofs

  Show description for 850d50c
  rod-chapman

  committed
  850d50c

  Copy full SHA for 850d50c

• Add one more stub function to satisfy CBMC 6.1 on EC2/Linux

  Show description for 8b0b1f0
  rod-chapman

  committed
  8b0b1f0

  Copy full SHA for 8b0b1f0