diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-27 18:18:24 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-27 18:18:24 +0200 |
| commit | 28e66eb4b60c485bebb1e217bc8f50bdc2cc6ddb (patch) | |
| tree | 9a99e19fdec1846b513cf18b6f5f82258338d66c /mppa_k1c/SelectOpproof.v | |
| parent | 87615fd17854019e12a5acdebab11adc62eec5c1 (diff) | |
| download | compcert-kvx-28e66eb4b60c485bebb1e217bc8f50bdc2cc6ddb.tar.gz compcert-kvx-28e66eb4b60c485bebb1e217bc8f50bdc2cc6ddb.zip | |
moved operators to specific file instead of common file
Diffstat (limited to 'mppa_k1c/SelectOpproof.v')
| -rw-r--r-- | mppa_k1c/SelectOpproof.v | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 4df87bea..b23e2aa8 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -23,6 +23,7 @@ Require Import AST. Require Import Integers. Require Import Floats. Require Import Values. +Require Import ExtValues. Require Import Memory. Require Import Globalenvs. Require Import Cminor. @@ -311,14 +312,14 @@ Proof. simpl negb. cbn iota. destruct (_ && _ && _) eqn:BOUNDS. - + exists (Val.extfz (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) + + exists (extfz (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) (Z.sub (Z.add (Z.add (Int.unsigned n) (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one))) Z.one) Int.zwordsize) v1). split. ++ EvalOp. - ++ unfold Val.extfz. + ++ unfold extfz. rewrite BOUNDS. destruct v1; try (simpl; apply Val.lessdef_undef). replace (Z.sub Int.zwordsize @@ -368,14 +369,14 @@ Proof. simpl negb. cbn iota. destruct (_ && _ && _) eqn:BOUNDS. - + exists (Val.extfs (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) + + exists (extfs (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) (Z.sub (Z.add (Z.add (Int.unsigned n) (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one))) Z.one) Int.zwordsize) v1). split. ++ EvalOp. - ++ unfold Val.extfs. + ++ unfold extfs. rewrite BOUNDS. destruct v1; try (simpl; apply Val.lessdef_undef). replace (Z.sub Int.zwordsize |