Commit 6e65fb15 authored by Marc Schoolderman's avatar Marc Schoolderman
Browse files

int_flag -> cpu_flag

parent 5f955d6b
This diff is collapsed.
......@@ -619,7 +619,9 @@ ensures { reg[20] = 0 /\ reg[21] = 0 }
adc r19 r21;
end;
abstract
ensures { uint 10 reg 12 = old(uint 10 reg 12 + pow2 24*uint 2 reg 5*uint 5 reg 7) }
ensures { uint 7 reg 15 = old(uint 7 reg 15 + uint 2 reg 5*uint 5 reg 7) }
(*ensures { uint 10 reg 12 = old(uint 10 reg 12 + pow2 24*uint 2 reg 5*uint 5 reg 7) }*)
ensures { eq 3 reg (old reg) 12 }
ensures { eq 5 reg (at reg 'S) 2 }
ensures { eq 5 reg (at reg 'S) 7 }
'B:
......@@ -840,7 +842,9 @@ ensures { reg[23] = 0 /\ reg[24] = 0 /\ reg[25] = 0 }
adc r22 r1;
end;
abstract
ensures { uint 12 reg 14 = old(uint 12 reg 14 + pow2 24*uint 3 reg 5*uint 6 reg 8) }
ensures { uint 9 reg 17 = old(uint 9 reg 17 + uint 3 reg 5*uint 6 reg 8) }
(* ensures { uint 12 reg 14 = old(uint 12 reg 14 + pow2 24*uint 3 reg 5*uint 6 reg 8) } *)
ensures { eq 3 reg (old reg) 14 }
ensures { eq 6 reg (at reg 'S) 2 }
ensures { eq 6 reg (at reg 'S) 8 }
'B:
......@@ -915,7 +919,7 @@ ensures { eq 6 reg (at reg 'S) 8 }
adc r23 r27;
adc r24 r0;
adc r25 r1;
assert { uint 9 reg 17 = at(uint 9 reg 17 + uint 3 reg 5*uint 6 reg 8)'B };
(* assert { uint 9 reg 17 = at(uint 9 reg 17 + uint 3 reg 5*uint 6 reg 8)'B }; *)
()
end
......
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