Read-only memory sections maintained throughout program#92

Merged

l-kent merged 9 commits intomainfrom read-only-memory

Oct 17, 2023

+67,196-36,859

Commits on Oct 8, 2023

add read-only memory sections to pre/post-conditions for all procedures, add useArrayAxioms flag to test suite, update readme with information about that
l-kent
committed

Commits on Oct 9, 2023

don't add ensures (forall i: bv64 :: (((mem[i] == old(mem[i])) ==> (Gamma_mem[i] == old(Gamma_mem[i]))))) to empty relies
l-kent
committed
Merge branch 'main' into read-only-memory
l-kent
committed
update expected files
l-kent
committed
missed a few expected files
l-kent
committed

Commits on Oct 17, 2023

add comment
l-kent
committed
Merge branch 'main' into read-only-memory
l-kent
committed
make unresolved indirect calls cause 'assert fail;' again because that went missing in a merge
l-kent
committed
update expected
l-kent
committed