Code

Contracts for a few core functions#3107

Code

Merged

celinval merged 15 commits intomodel-checking:mainmodel-checking/kani:mainfrom celinval:std-non-nullcelinval/kani-dev:std-non-nullCopy head branch name to clipboardMay 29, 2024

+667-153

Commits

Commits on Mar 28, 2024

• Add initial tests for NonNull and mem predicates

  celinval

  committed
  19a4769

• Improve library and change std tests to use crates.

  Show description for a9c5f62
  celinval

  committed
  a9c5f62

• Add support to write_bytes used in MaybeUninit

  Show description for 9a1dccf
  celinval

  committed
  9a1dccf

• Add contract for replace

  celinval

  committed
  86edd76

• Add missing Cargo.toml

  celinval

  committed
  c38136f

Commits on May 11, 2024

• Merge remote-tracking branch 'origin/main' into std-non-null

  celinval

  committed
  3c74b6c

Commits on May 13, 2024

• Rename a few things

  celinval

  committed
  3dffab5

Commits on May 14, 2024

• Add a new intrinsic to check value validity

  celinval

  committed
  e844934

• Finish polishing contracts and create expected

  celinval

  committed
  7469d61

• revert space changes

  celinval

  committed
  e2b4a20

• Clean up changes

  celinval

  committed
  122e3a8

Commits on May 24, 2024

• Address comments and fix issue in invalid values

  Show description for 5f4a69b
  celinval

  committed
  5f4a69b

Commits on May 28, 2024

• Fix regression

  celinval

  committed
  c18754d

Commits on May 29, 2024

• Update kani-compiler/src/kani_middle/transform/body.rs

  celinval

  authored
  2a8cfdb

• Merge branch 'main' into std-non-null

  celinval

  authored
  d295ce3