diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-01-10 12:39:34 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-01-10 12:39:34 +0100 |
| commit | e4443dfc20fb76c49a168636d1252c93b89ea7fb (patch) | |
| tree | a5f8216aaac002f674bec1072ad4052bdcdcb1e9 | |
| parent | 688adfa1f614a390a2835b62dfecfec685ee3b35 (diff) | |
| download | compcert-kvx-e4443dfc20fb76c49a168636d1252c93b89ea7fb.tar.gz compcert-kvx-e4443dfc20fb76c49a168636d1252c93b89ea7fb.zip | |
fix for SSA
| -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). |