Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Read-only memory sections maintained throughout program #92

Merged
merged 9 commits into from
Oct 17, 2023
Merged
  •  
  •  
  •  
Prev Previous commit
Next Next commit
update expected files
  • Loading branch information
l-kent committed Oct 9, 2023
commit 9208d1d2fb6da509a3d23f0f2eda165ab0c463a1
153 changes: 104 additions & 49 deletions src/test/correct/arrays_simple/clang/arrays_simple.expected
Original file line number Diff line number Diff line change
Expand Up @@ -34,9 +34,44 @@ function memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) returns
function {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
procedure rely();
modifies mem, Gamma_mem;
ensures (forall i: bv64 :: (((mem[i] == old(mem[i])) ==> (Gamma_mem[i] == old(Gamma_mem[i])))));
ensures (mem == old(mem));
ensures (Gamma_mem == old(Gamma_mem));
free ensures (memory_load8_le(mem, 1872bv64) == 1bv8);
free ensures (memory_load8_le(mem, 1873bv64) == 0bv8);
free ensures (memory_load8_le(mem, 1874bv64) == 2bv8);
free ensures (memory_load8_le(mem, 1875bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69064bv64) == 16bv8);
free ensures (memory_load8_le(mem, 69065bv64) == 7bv8);
free ensures (memory_load8_le(mem, 69066bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69067bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69068bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69069bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69070bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69071bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69072bv64) == 192bv8);
free ensures (memory_load8_le(mem, 69073bv64) == 6bv8);
free ensures (memory_load8_le(mem, 69074bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69075bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69076bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69077bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69078bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69079bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69592bv64) == 20bv8);
free ensures (memory_load8_le(mem, 69593bv64) == 7bv8);
free ensures (memory_load8_le(mem, 69594bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69595bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69596bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69597bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69598bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69599bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69672bv64) == 40bv8);
free ensures (memory_load8_le(mem, 69673bv64) == 16bv8);
free ensures (memory_load8_le(mem, 69674bv64) == 1bv8);
free ensures (memory_load8_le(mem, 69675bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69676bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69677bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69678bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);

procedure rely_transitive()
modifies mem, Gamma_mem;
Expand All @@ -54,42 +89,42 @@ procedure guarantee_reflexive();

procedure main()
modifies Gamma_R0, Gamma_R31, Gamma_R8, Gamma_stack, R0, R31, R8, stack;
free requires (memory_load8_le(mem, 69664bv64) == 0bv8);
free requires (memory_load8_le(mem, 69665bv64) == 0bv8);
free requires (memory_load8_le(mem, 69666bv64) == 0bv8);
free requires (memory_load8_le(mem, 69667bv64) == 0bv8);
free requires (memory_load8_le(mem, 69668bv64) == 0bv8);
free requires (memory_load8_le(mem, 69669bv64) == 0bv8);
free requires (memory_load8_le(mem, 69670bv64) == 0bv8);
free requires (memory_load8_le(mem, 69671bv64) == 0bv8);
free requires (memory_load8_le(mem, 69672bv64) == 40bv8);
free requires (memory_load8_le(mem, 69673bv64) == 16bv8);
free requires (memory_load8_le(mem, 69674bv64) == 1bv8);
free requires (memory_load8_le(mem, 69675bv64) == 0bv8);
free requires (memory_load8_le(mem, 69676bv64) == 0bv8);
free requires (memory_load8_le(mem, 69677bv64) == 0bv8);
free requires (memory_load8_le(mem, 69678bv64) == 0bv8);
free requires (memory_load8_le(mem, 69679bv64) == 0bv8);
free requires (memory_load8_le(mem, 1872bv64) == 1bv8);
free requires (memory_load8_le(mem, 1873bv64) == 0bv8);
free requires (memory_load8_le(mem, 1874bv64) == 2bv8);
free requires (memory_load8_le(mem, 1875bv64) == 0bv8);
free requires (memory_load8_le(mem, 69560bv64) == 216bv8);
free requires (memory_load8_le(mem, 69561bv64) == 13bv8);
free requires (memory_load8_le(mem, 69562bv64) == 1bv8);
free requires (memory_load8_le(mem, 69563bv64) == 0bv8);
free requires (memory_load8_le(mem, 69564bv64) == 0bv8);
free requires (memory_load8_le(mem, 69565bv64) == 0bv8);
free requires (memory_load8_le(mem, 69566bv64) == 0bv8);
free requires (memory_load8_le(mem, 69567bv64) == 0bv8);
free requires (memory_load8_le(mem, 69568bv64) == 0bv8);
free requires (memory_load8_le(mem, 69569bv64) == 0bv8);
free requires (memory_load8_le(mem, 69570bv64) == 0bv8);
free requires (memory_load8_le(mem, 69571bv64) == 0bv8);
free requires (memory_load8_le(mem, 69572bv64) == 0bv8);
free requires (memory_load8_le(mem, 69573bv64) == 0bv8);
free requires (memory_load8_le(mem, 69574bv64) == 0bv8);
free requires (memory_load8_le(mem, 69575bv64) == 0bv8);
free requires (memory_load8_le(mem, 69576bv64) == 0bv8);
free requires (memory_load8_le(mem, 69577bv64) == 0bv8);
free requires (memory_load8_le(mem, 69578bv64) == 0bv8);
free requires (memory_load8_le(mem, 69579bv64) == 0bv8);
free requires (memory_load8_le(mem, 69580bv64) == 0bv8);
free requires (memory_load8_le(mem, 69581bv64) == 0bv8);
free requires (memory_load8_le(mem, 69582bv64) == 0bv8);
free requires (memory_load8_le(mem, 69583bv64) == 0bv8);
free requires (memory_load8_le(mem, 69584bv64) == 0bv8);
free requires (memory_load8_le(mem, 69585bv64) == 0bv8);
free requires (memory_load8_le(mem, 69586bv64) == 0bv8);
free requires (memory_load8_le(mem, 69587bv64) == 0bv8);
free requires (memory_load8_le(mem, 69588bv64) == 0bv8);
free requires (memory_load8_le(mem, 69589bv64) == 0bv8);
free requires (memory_load8_le(mem, 69590bv64) == 0bv8);
free requires (memory_load8_le(mem, 69591bv64) == 0bv8);
free requires (memory_load8_le(mem, 69064bv64) == 16bv8);
free requires (memory_load8_le(mem, 69065bv64) == 7bv8);
free requires (memory_load8_le(mem, 69066bv64) == 0bv8);
free requires (memory_load8_le(mem, 69067bv64) == 0bv8);
free requires (memory_load8_le(mem, 69068bv64) == 0bv8);
free requires (memory_load8_le(mem, 69069bv64) == 0bv8);
free requires (memory_load8_le(mem, 69070bv64) == 0bv8);
free requires (memory_load8_le(mem, 69071bv64) == 0bv8);
free requires (memory_load8_le(mem, 69072bv64) == 192bv8);
free requires (memory_load8_le(mem, 69073bv64) == 6bv8);
free requires (memory_load8_le(mem, 69074bv64) == 0bv8);
free requires (memory_load8_le(mem, 69075bv64) == 0bv8);
free requires (memory_load8_le(mem, 69076bv64) == 0bv8);
free requires (memory_load8_le(mem, 69077bv64) == 0bv8);
free requires (memory_load8_le(mem, 69078bv64) == 0bv8);
free requires (memory_load8_le(mem, 69079bv64) == 0bv8);
free requires (memory_load8_le(mem, 69592bv64) == 20bv8);
free requires (memory_load8_le(mem, 69593bv64) == 7bv8);
free requires (memory_load8_le(mem, 69594bv64) == 0bv8);
Expand All @@ -98,22 +133,6 @@ procedure main()
free requires (memory_load8_le(mem, 69597bv64) == 0bv8);
free requires (memory_load8_le(mem, 69598bv64) == 0bv8);
free requires (memory_load8_le(mem, 69599bv64) == 0bv8);
free requires (memory_load8_le(mem, 69600bv64) == 0bv8);
free requires (memory_load8_le(mem, 69601bv64) == 0bv8);
free requires (memory_load8_le(mem, 69602bv64) == 0bv8);
free requires (memory_load8_le(mem, 69603bv64) == 0bv8);
free requires (memory_load8_le(mem, 69604bv64) == 0bv8);
free requires (memory_load8_le(mem, 69605bv64) == 0bv8);
free requires (memory_load8_le(mem, 69606bv64) == 0bv8);
free requires (memory_load8_le(mem, 69607bv64) == 0bv8);
free requires (memory_load8_le(mem, 69664bv64) == 0bv8);
free requires (memory_load8_le(mem, 69665bv64) == 0bv8);
free requires (memory_load8_le(mem, 69666bv64) == 0bv8);
free requires (memory_load8_le(mem, 69667bv64) == 0bv8);
free requires (memory_load8_le(mem, 69668bv64) == 0bv8);
free requires (memory_load8_le(mem, 69669bv64) == 0bv8);
free requires (memory_load8_le(mem, 69670bv64) == 0bv8);
free requires (memory_load8_le(mem, 69671bv64) == 0bv8);
free requires (memory_load8_le(mem, 69672bv64) == 40bv8);
free requires (memory_load8_le(mem, 69673bv64) == 16bv8);
free requires (memory_load8_le(mem, 69674bv64) == 1bv8);
Expand All @@ -124,6 +143,42 @@ procedure main()
free requires (memory_load8_le(mem, 69679bv64) == 0bv8);
free ensures (Gamma_R31 == old(Gamma_R31));
free ensures (R31 == old(R31));
free ensures (memory_load8_le(mem, 1872bv64) == 1bv8);
free ensures (memory_load8_le(mem, 1873bv64) == 0bv8);
free ensures (memory_load8_le(mem, 1874bv64) == 2bv8);
free ensures (memory_load8_le(mem, 1875bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69064bv64) == 16bv8);
free ensures (memory_load8_le(mem, 69065bv64) == 7bv8);
free ensures (memory_load8_le(mem, 69066bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69067bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69068bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69069bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69070bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69071bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69072bv64) == 192bv8);
free ensures (memory_load8_le(mem, 69073bv64) == 6bv8);
free ensures (memory_load8_le(mem, 69074bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69075bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69076bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69077bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69078bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69079bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69592bv64) == 20bv8);
free ensures (memory_load8_le(mem, 69593bv64) == 7bv8);
free ensures (memory_load8_le(mem, 69594bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69595bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69596bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69597bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69598bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69599bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69672bv64) == 40bv8);
free ensures (memory_load8_le(mem, 69673bv64) == 16bv8);
free ensures (memory_load8_le(mem, 69674bv64) == 1bv8);
free ensures (memory_load8_le(mem, 69675bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69676bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69677bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69678bv64) == 0bv8);
free ensures (memory_load8_le(mem, 69679bv64) == 0bv8);
{
lmain:
R31, Gamma_R31 := bvadd64(R31, 18446744073709551584bv64), Gamma_R31;
Expand Down
Loading