Commit 481616e5 authored by Jonathan Moerman's avatar Jonathan Moerman
Browse files

Fix last failing (was wrong) postcondition

parent 5286c418
......@@ -339,8 +339,6 @@ S.init();
begin ensures { S.synchronized S.shadow reg }
ensures { uint 6 reg 20 + pow2 48*uint 2 reg 2 = old (uint 4 reg 2*uint 4 reg 6) }
ensures { valid_addr_space reg }
ensures { valid_addr_space mem }
ensures { valid_addr_space stack }
(* compute m *)
mul r2 r6;
......@@ -422,8 +420,6 @@ begin
ensures { S.synchronized S.shadow reg }
ensures { uint 8 reg 10 + ?cf*pow2 64 = old(uint 8 reg 10 + uint 4 reg 14 + pow2 32*uint 2 reg 28 + pow2 48*uint 2 reg 18) }
ensures { valid_addr_space reg }
ensures { valid_addr_space mem }
ensures { valid_addr_space stack }
(* add l4 h0 to l0 and h4 *)
label B in
add r10 r14;
......@@ -443,7 +439,7 @@ begin
ensures { S.synchronized S.shadow reg }
ensures { uint 6 reg 20 + pow2 48*uint 2 reg 2 = ?cf*(pow2 64 - 1) + (if !tf then 1 else -1)*old(uint 6 reg 20 + pow2 48*uint 2 reg 2) }
ensures { let cor = reg[26] + (pow2 8+pow2 16+pow2 24)*reg[0] in cor = (old ?cf) - ?cf \/ cor = pow2 32 + (old ?cf) - ?cf }
ensures { let cor = reg[26] + (pow2 8 + pow2 16 + pow2 24)*reg[0] in cor = mod ((old ?cf) - ?cf) 256 \/ cor = pow2 32 + (old ?cf) - ?cf }
(*
ensures { let cor = reg[26] + (pow2 8+pow2 16+pow2 24)*reg[0] in cor = (old ?cf) - ?cf + (if ?cf > old ?cf then pow2 32 else 0) }
......
This diff is collapsed.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment