diff options
Diffstat (limited to 'backend/ValueDomain.v')
-rw-r--r-- | backend/ValueDomain.v | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 81a52bab..f1a46baa 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -2711,6 +2711,28 @@ Proof. all: try constructor. Qed. +Lemma floatofint_total_sound: + forall v x, vmatch v x -> + vmatch (Val.maketotal (Val.floatofint v)) (floatofint x). +Proof. + unfold Val.floatofint, floatofint; intros. + inv H; simpl. + all: auto with va. + all: unfold ntop1, provenance. + all: try constructor. +Qed. + +Lemma floatofintu_total_sound: + forall v x, vmatch v x -> + vmatch (Val.maketotal (Val.floatofintu v)) (floatofintu x). +Proof. + unfold Val.floatofintu, floatofintu; intros. + inv H; simpl. + all: auto with va. + all: unfold ntop1, provenance. + all: try constructor. +Qed. + Definition divs_total (v w: aval) := match w, v with @@ -5187,6 +5209,8 @@ Hint Resolve cnot_sound symbol_address_sound singleoflongu_total_sound floatoflong_total_sound floatoflongu_total_sound + floatofint_total_sound + floatofintu_total_sound divu_total_sound divs_total_sound modu_total_sound mods_total_sound shrx_total_sound divlu_total_sound divls_total_sound |