Repository navigation

Contracts and Harnesses for `<*const T>::add`, `sub` and `offset` - #166

Merged

tautschnig merged 61 commits into

model-checking:mainfrom

stogaru:verify/ptr_const

Dec 3, 2024

Merged

Contracts and Harnesses for `<*const T>::add`, `sub` and `offset`#166
tautschnig merged 61 commits into
model-checking:mainfrom
stogaru:verify/ptr_const

Commits on Sep 13, 2024
- Add verification contract for *const T::add and *const T::add
  szlee118
  committed
  500f249
Commits on Sep 19, 2024
- Update const_ptr.rs
  xsxszab
  authored
  99701ff
- Merge branch 'model-checking:main' into test
  stogaru
  authored
  31c82a9
- Changes generic type to i32 in proof.
  stogaru
  committed
  f84b7a6
Commits on Sep 20, 2024
- Remove unneeded file
  szlee118
  committed
  a839820
- added comments for function contracts and harnesses
  
  xsxsz
  authored and
  xsxsz
  committed
  21e0ab8
Commits on Sep 23, 2024
- Merge branch 'main' into verify/ptr_const_offset
  stogaru
  authored
  b54ce9e
Commits on Sep 30, 2024
- reverted library code format change and removed unnecessary comments
  xsxszab
  committed
  0c0078f
Commits on Oct 1, 2024
- added macros for verifying all integer types for offset and add
  xsxszab
  committed
  a192129
- implemented function contract and integer type proofs for fn sub
  xsxszab
  committed
  2ef5923
- Add verification of slice type proofs for fn offset
  szlee118
  committed
  f1602aa
- add TODOs for proof for contracts
  xsxszab
  committed
  1b467d5
- verified *mut T::offset for all integer types
  xsxszab
  committed
  9461027
Commits on Oct 3, 2024
- Add verification of slice type proofs for fn add and sub
  szlee118
  committed
  159137b
- Remove commented code
  szlee118
  committed
  df56d18
- removed unnecessary comments
  xsxszab
  committed
  eab0a15
- reverted changes to mut_ptr.rs
  xsxszab
  committed
  e07040f
- removed necessary comments
  xsxszab
  committed
  0ff52b5
- aligned format for mut_ptr.rs
  xsxszab
  committed
  ccd5c3c
- aligned format for mut_ptr.rs
  xsxszab
  committed
  180a276
- Merge pull request #1 from stogaru/verify/ptr_const_integer_types
  xsxszab
  authored
  6a85e3e
- Merge branch 'model-checking:main' into verify/ptr_const_offset
  xsxszab
  authored
  6853284
- Adds proofs for composite type - tuple
  stogaru
  committed
  fb79caf
- Change function proof names
  stogaru
  committed
  7d05c96
- Merge pull request #2 from stogaru/verify/ptr_const_composite
  stogaru
  authored
  8e49dcd
- Merge branch 'verify/ptr_const_offset' into verify/ptr_const_slice_type
  szlee118
  authored
  9af0e39
- Merge pull request #4 from stogaru/verify/ptr_const_slice_type
  szlee118
  authored
  31532c9
Commits on Oct 7, 2024
- Added changes for *const T::add & *const::sub verifying unit type
  MayureshJoshi25
  committed
  f9f5371
Commits on Oct 12, 2024
- Updated proofs for const ptr (unit type)
  MayureshJoshi25
  committed
  eab900e
Commits on Oct 17, 2024
- Merge branch 'verify/ptr_const' into verify/ptr_const_unit_type
  stogaru
  authored
  05c0fdd
- Merge pull request #5 from stogaru/verify/ptr_const_unit_type
  stogaru
  authored
  098f171
Commits on Oct 18, 2024
- Merge branch 'model-checking:main' into verify/ptr_const
  stogaru
  authored
  8c75da8
Commits on Oct 25, 2024
- Generate slice harness for array
  szlee118
  committed
  bd418a4
- Remove redundant declaration
  szlee118
  committed
  e05b5f8
Commits on Nov 7, 2024
Commits on Nov 8, 2024
- Merge branch 'verify/ptr_const' into verify/ptr_const_slice_types
  szlee118
  authored
  2bc0a0f
- Modify document
  szlee118
  committed
  554e003
- Fix indentation error
  szlee118
  committed
  a69688f
- Merge pull request #14 from stogaru/verify/ptr_const_slice_types
  szlee118
  authored
  b18ee62
Commits on Nov 14, 2024
- improved comments and function naming
  xsxszab
  committed
  3effadd
- fixed a typo
  xsxszab
  committed
  c3cb7fe
- Merge branch 'main' into verify/ptr_const
  stogaru
  committed
  949eb9c
Commits on Nov 15, 2024
- updated proofs using pointer generator
  xsxszab
  committed
  cc5d490
- Merge branch 'main' into verify/ptr_const
  xsxszab
  authored
  ef71817
Commits on Nov 27, 2024
- Reformatted code using rustfmt.
  xsxszab
  committed
  5edd16e
- Reverted unnecessary rustfmt formatting
  xsxszab
  committed
  dd2a8eb
Commits on Nov 28, 2024
- Merge branch 'main' into verify/ptr_const
  szlee118
  authored
  7b83329
- Resolved compilation error after previous merge.
  xsxszab
  committed
  576483f
- Enhanced comments to clarify proof for contracts.
  xsxszab
  committed
  330f06b
Commits on Nov 29, 2024
Commits on Dec 2, 2024
- Refactored contracts to improve performance
  xsxszab
  committed
  6ee7941
Commits on Dec 3, 2024

Commits

Commits on Sep 13, 2024

Commits on Sep 19, 2024

Commits on Sep 20, 2024

Commits on Sep 23, 2024

Commits on Sep 30, 2024

Commits on Oct 1, 2024

Commits on Oct 3, 2024

Commits on Oct 7, 2024

Commits on Oct 12, 2024

Commits on Oct 17, 2024

Commits on Oct 18, 2024

Commits on Oct 25, 2024

Commits on Nov 7, 2024

Commits on Nov 8, 2024

Commits on Nov 14, 2024

Commits on Nov 15, 2024

Commits on Nov 27, 2024

Commits on Nov 28, 2024

Commits on Nov 29, 2024

Commits on Dec 2, 2024

Commits on Dec 3, 2024