diff options
Diffstat (limited to 'x86/ConstpropOp.vp')
| -rw-r--r-- | x86/ConstpropOp.vp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/x86/ConstpropOp.vp b/x86/ConstpropOp.vp index 0bf143d2..759d7c16 100644 --- a/x86/ConstpropOp.vp +++ b/x86/ConstpropOp.vp @@ -46,7 +46,7 @@ Definition const_for_result (a: aval) : option operation := one if some of its arguments are statically known. These are again large pattern-matchings expressed in indirect style. *) -Nondetfunction cond_strength_reduction +Nondetfunction cond_strength_reduction (cond: condition) (args: list reg) (vl: list aval) := match cond, args, vl with | Ccomp c, r1 :: r2 :: nil, I n1 :: v2 :: nil => @@ -65,7 +65,7 @@ Nondetfunction cond_strength_reduction (Ccompluimm (swap_comparison c) n1, r2 :: nil) | Ccomplu c, r1 :: r2 :: nil, v1 :: L n2 :: nil => (Ccompluimm c n2, r1 :: nil) - | _, _, _ => + | _, _, _ => (cond, args) end. @@ -350,7 +350,7 @@ Definition make_cast16signed (r: reg) (a: aval) := Definition make_cast16unsigned (r: reg) (a: aval) := if vincl a (Uns Ptop 16) then (Omove, r :: nil) else (Ocast16unsigned, r :: nil). -Nondetfunction op_strength_reduction +Nondetfunction op_strength_reduction (op: operation) (args: list reg) (vl: list aval) := match op, args, vl with | Ocast8signed, r1 :: nil, v1 :: nil => make_cast8signed r1 v1 |