Code

Verifying methods of <*const T>#92

Code

Closed

stogaru wants to merge 27 commits intomodel-checking:mainmodel-checking/verify-rust-std:mainfrom stogaru:verify/ptr_const_offsetstogaru/verify-rust-std:verify/ptr_const_offsetCopy head branch name to clipboard

+159

Commits

Commits on Sep 13, 2024

• Add verification contract for *const T::add and *const T::add

  szlee118

  committed
  500f249

  Copy full SHA for 500f249

Commits on Sep 19, 2024

• Update const_ptr.rs

  xsxszab

  authored
  99701ff

  Copy full SHA for 99701ff

• Merge branch 'model-checking:main' into test

  stogaru

  authored
  31c82a9

  Copy full SHA for 31c82a9

• Changes generic type to i32 in proof.

  Show description for f84b7a6
  stogaru

  committed
  f84b7a6

  Copy full SHA for f84b7a6

Commits on Sep 20, 2024

• Remove unneeded file

  szlee118

  committed
  a839820

  Copy full SHA for a839820

• added comments for function contracts and harnesses

  

  xsxsz

  authored and

  xsxsz

  committed
  21e0ab8

  Copy full SHA for 21e0ab8

Commits on Sep 23, 2024

• Merge branch 'main' into verify/ptr_const_offset

  stogaru

  authored
  b54ce9e

  Copy full SHA for b54ce9e

Commits on Sep 30, 2024

• reverted library code format change and removed unnecessary comments

  xsxszab

  committed
  0c0078f

  Copy full SHA for 0c0078f

Commits on Oct 1, 2024

• added macros for verifying all integer types for offset and add

  xsxszab

  committed
  a192129

  Copy full SHA for a192129

• implemented function contract and integer type proofs for fn sub

  xsxszab

  committed
  2ef5923

  Copy full SHA for 2ef5923

• Add verification of slice type proofs for fn offset

  szlee118

  committed
  f1602aa

  Copy full SHA for f1602aa

• add TODOs for proof for contracts

  xsxszab

  committed
  1b467d5

  Copy full SHA for 1b467d5

• verified *mut T::offset for all integer types

  xsxszab

  committed
  9461027

  Copy full SHA for 9461027

Commits on Oct 3, 2024

• Add verification of slice type proofs for fn add and sub

  szlee118

  committed
  159137b

  Copy full SHA for 159137b

• Remove commented code

  szlee118

  committed
  df56d18

  Copy full SHA for df56d18

• removed unnecessary comments

  xsxszab

  committed
  eab0a15

  Copy full SHA for eab0a15

• reverted changes to mut_ptr.rs

  xsxszab

  committed
  e07040f

  Copy full SHA for e07040f

• removed necessary comments

  xsxszab

  committed
  0ff52b5

  Copy full SHA for 0ff52b5

• aligned format for mut_ptr.rs

  xsxszab

  committed
  ccd5c3c

  Copy full SHA for ccd5c3c

• aligned format for mut_ptr.rs

  xsxszab

  committed
  180a276

  Copy full SHA for 180a276

• Merge pull request #1 from stogaru/verify/ptr_const_integer_types

  Show description for 6a85e3e
  xsxszab

  authored
  6a85e3e

  Copy full SHA for 6a85e3e

• Merge branch 'model-checking:main' into verify/ptr_const_offset

  xsxszab

  authored
  6853284

  Copy full SHA for 6853284

• Adds proofs for composite type - tuple

  stogaru

  committed
  fb79caf

  Copy full SHA for fb79caf

• Change function proof names

  stogaru

  committed
  7d05c96

  Copy full SHA for 7d05c96

• Merge pull request #2 from stogaru/verify/ptr_const_composite

  Show description for 8e49dcd
  stogaru

  authored
  8e49dcd

  Copy full SHA for 8e49dcd

• Merge branch 'verify/ptr_const_offset' into verify/ptr_const_slice_type

  szlee118

  authored
  9af0e39

  Copy full SHA for 9af0e39

• Merge pull request #4 from stogaru/verify/ptr_const_slice_type

  Show description for 31532c9
  szlee118

  authored
  31532c9

  Copy full SHA for 31532c9