We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent dcfe2aa commit 73bb6a9Copy full SHA for 73bb6a9
src/Assembly/WithBedrock/Semantics.v
@@ -339,7 +339,7 @@ Definition DenoteNormalInstruction (st : machine_state) (instr : NormalInstructi
339
if cnt =? 0 then Some st else
340
if Z.of_N s <? cnt then Some (HavocFlags st) else
341
let st := HavocFlagsFromResult s st l in
342
- let signchange := xorb (signed s hv <? 0)%Z (signed s v <? 0)%Z in
+ let signchange := xorb (Z.signed s hv <? 0)%Z (Z.signed s v <? 0)%Z in
343
(* Note: IA-32 SDM does not make it clear what sign change is in question *)
344
let st := if cnt =? 1 then SetFlag st OF signchange else st in
345
let st := SetFlag st CF (Z.testbit hv (Z.of_N s - cnt)) in
0 commit comments