Harnesses verifying slice types for add, sub and offset#179

Merged

tautschnig merged 39 commits intomodel-checking:mainfrom

stogaru:verify/ptr_mut_slice_types

Dec 10, 2024

Commits on Oct 7, 2024

Commits on Oct 12, 2024

Commits on Oct 23, 2024

refactored function contracts for add, sub and offset using the same_allocation api, modified their proof for harness accordingly
xsxszab
committed
merged macros for add, sub and offset
xsxszab
committed

Commits on Oct 24, 2024

updated function contracts and proof for contracts for add(), sub() and offset()
xsxszab
committed

Commits on Oct 31, 2024

added support for unit type pointers
xsxszab
committed

Commits on Nov 6, 2024

Commits on Nov 7, 2024

Commits on Nov 12, 2024

Add slice harness for mut
szlee118
committed

Commits on Nov 22, 2024

Merge branch 'main' into verify/ptr_mut_slice_types
carolynzech
authored

Commits on Nov 28, 2024

Commits on Dec 2, 2024

Resolve merge conflict
szlee118
committed

Commits on Dec 3, 2024

Commits on Dec 5, 2024

Commits on Dec 6, 2024

Merge branch 'main' into verify/ptr_mut_slice_types
szlee118
authored

Commits on Dec 9, 2024

Commits on Dec 10, 2024

Merge branch 'main' into verify/ptr_mut_slice_types
tautschnig
authored