diff options
Diffstat (limited to 'arm/ConstpropOpproof.v')
| -rw-r--r-- | arm/ConstpropOpproof.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v index c7de86d..687e08f 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/ConstpropOpproof.v @@ -45,9 +45,10 @@ Definition val_match_approx (a: approx) (v: val) : Prop := | Unknown => True | I p => v = Vint p | F p => v = Vfloat p + | L p => v = Vlong p | G symb ofs => v = symbol_address ge symb ofs | S ofs => v = Val.add sp (Vint ofs) - | _ => False + | Novalue => False end. Inductive val_list_match_approx: list approx -> list val -> Prop := @@ -65,6 +66,8 @@ Ltac SimplVMA := simpl in H; (try subst v); SimplVMA | H: (val_match_approx (F _) ?v) |- _ => simpl in H; (try subst v); SimplVMA + | H: (val_match_approx (L _) ?v) |- _ => + simpl in H; (try subst v); SimplVMA | H: (val_match_approx (G _ _) ?v) |- _ => simpl in H; (try subst v); SimplVMA | H: (val_match_approx (S _) ?v) |- _ => |