diff options
| -rw-r--r-- | kvx/ValueAOpSSA.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kvx/ValueAOpSSA.v b/kvx/ValueAOpSSA.v index 8b76f77e..e94c0fc4 100644 --- a/kvx/ValueAOpSSA.v +++ b/kvx/ValueAOpSSA.v @@ -15,7 +15,7 @@ Require Import Coqlib Compopts. Require Import AST Integers Floats Values Memory Globalenvs. -Require Import Op ExtValues ExtFloats RTL ValueDomainSSA. +Require Import Op ExtValues ExtFloats SSA ValueDomainSSA. Definition minf := binop_float ExtFloat.min. Definition maxf := binop_float ExtFloat.max. Definition minfs := binop_single ExtFloat32.min. @@ -314,10 +314,10 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := Section SOUNDNESS. Variable bc: block_classification. -Variable ge: SSA.genv. +Variable ge: genv. Hypothesis GENV: genv_match bc ge. Variable sp: block. -Hypothesis STACK: bc sp = BCstack. +Hypothesis STACK: bc sp <> BCinvalid. Lemma minf_sound: forall v x w y, vmatch bc v x -> vmatch bc w y -> vmatch bc (ExtValues.minf v w) (minf x y). |