Commit e699df30 authored by Jonathan Moerman's avatar Jonathan Moerman

Remove outdated comment

parent 98b93981
......@@ -471,7 +471,7 @@ requires {
requires { S.synchronized S.shadow reg }
ensures {reg[1] = 0}
ensures {reg[8] = old reg[8]}
ensures {uint 32 mem (uint 2 (old reg) r24) === old (121666* uint 32 mem (uint 2 reg r22))} (* Haven't checked, but I think this congruent to this result, but not equal *)
ensures {uint 32 mem (uint 2 (old reg) r24) === old (121666* uint 32 mem (uint 2 reg r22))}
ensures { S.synchronized S.shadow reg }
= 'L1:
push r8;
......
Markdown is supported
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