diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-19 19:28:03 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-19 19:28:03 +0100 |
| commit | 50ea35fceb52c5f66ccbc4f709df3a3471b12647 (patch) | |
| tree | cbbe994acd0e7e50c8a0302c5b62c84b0e753709 /backend/SelectDiv.vp | |
| parent | 202050c6240a11c94cc8b6ab599022fee7bd2471 (diff) | |
| download | compcert-kvx-50ea35fceb52c5f66ccbc4f709df3a3471b12647.tar.gz compcert-kvx-50ea35fceb52c5f66ccbc4f709df3a3471b12647.zip | |
added helper functions but strange
idiv.c: error: __compcert_i32_sdiv: missing or incorrect declaration
Diffstat (limited to 'backend/SelectDiv.vp')
| -rw-r--r-- | backend/SelectDiv.vp | 11 |
1 files changed, 4 insertions, 7 deletions
diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp index 357fab5e..6ddcd6ac 100644 --- a/backend/SelectDiv.vp +++ b/backend/SelectDiv.vp @@ -19,6 +19,9 @@ Require Import Op CminorSel SelectOp SplitLong SelectLong. Local Open Scope cminorsel_scope. +Section SELECT. +Context {hf: helper_functions}. + Definition is_intconst (e: expr) : option int := match e with | Eop (Ointconst n) _ => Some n @@ -221,10 +224,6 @@ Definition mods (e1: expr) (e2: expr) := (** 64-bit integer divisions *) -Section SELECT. - -Context {hf: helper_functions}. - Definition modl_from_divl (equo: expr) (n: int64) := subl (Eletvar O) (mullimm n equo). @@ -311,8 +310,6 @@ Definition modls (e1 e2: expr) := | _, _ => modls_base e1 e2 end. -End SELECT. - (** Floating-point division by a constant can also be turned into a FP multiplication by the inverse constant, but only for powers of 2. *) @@ -340,4 +337,4 @@ Nondetfunction divfs (e1: expr) (e2: expr) := | _ => Eop Odivfs (e1 ::: e2 ::: Enil) end. - +End SELECT.
\ No newline at end of file |