From 5281141d38a492eea3e080e087b91a314b0be020 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 22 Mar 2019 09:51:56 +0100
Subject: ARM repasse

---
 arm/SelectOpproof.v | 28 ++++++++++++++++++++++++++--
 1 file changed, 26 insertions(+), 2 deletions(-)

(limited to 'arm/SelectOpproof.v')

diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v
index d4aac9b6..212bcfd7 100644
--- a/arm/SelectOpproof.v
+++ b/arm/SelectOpproof.v
@@ -24,6 +24,7 @@ Require Import Cminor.
 Require Import Op.
 Require Import CminorSel.
 Require Import SelectOp.
+Require Import OpHelpers OpHelpersproof.
 
 Local Open Scope cminorsel_scope.
 Local Transparent Archi.ptr64.
@@ -76,8 +77,10 @@ Ltac TrivialExists :=
 (** * Correctness of the smart constructors *)
 
 Section CMCONSTR.
-
-Variable ge: genv.
+Variable prog: program.
+Variable hf: helper_functions.
+Hypothesis HELPERS: helper_functions_declared prog hf.
+Let ge := Genv.globalenv prog.
 Variable sp: val.
 Variable e: env.
 Variable m: mem.
@@ -893,4 +896,25 @@ Proof.
 - constructor; auto.
 Qed.
 
+
+(* floating-point division without HELPERS *)
+Theorem eval_divf_base:
+  forall le a b x y,
+  eval_expr ge sp e m le a x ->
+  eval_expr ge sp e m le b y ->
+  exists v, eval_expr ge sp e m le (divf_base a b) v /\ Val.lessdef (Val.divf x y) v.
+Proof.
+  intros; unfold divf_base.
+  TrivialExists.
+Qed.
+
+Theorem eval_divfs_base:
+  forall le a b x y,
+  eval_expr ge sp e m le a x ->
+  eval_expr ge sp e m le b y ->
+  exists v, eval_expr ge sp e m le (divfs_base a b) v /\ Val.lessdef (Val.divfs x y) v.
+Proof.
+  intros; unfold divfs_base.
+  TrivialExists.
+Qed.
 End CMCONSTR.
-- 
cgit