diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-21 22:48:45 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-21 22:48:45 +0200 |
| commit | cdb48111d4baff50d8708b979f8b31ef21505247 (patch) | |
| tree | cf989a9b938f1d4c3d9fde26d568157790bc516f /backend/ValueDomain.v | |
| parent | 9c2c662a2a70545858d95b2f9f0a3625c506bc24 (diff) | |
| download | compcert-kvx-cdb48111d4baff50d8708b979f8b31ef21505247.tar.gz compcert-kvx-cdb48111d4baff50d8708b979f8b31ef21505247.zip | |
risc-V now without trapping instructions
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 |