diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-20 11:29:18 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-20 11:29:18 +0100 |
| commit | e1da7c1c79ce2286f5b93cc3f336c9e10b195f0b (patch) | |
| tree | 9a56ade665a7a5c54e0f038f907dd46a6e57facf /mppa_k1c/SelectOpproof.v | |
| parent | bf0b2478a7cb6724cfce41695b552db47eacbff2 (diff) | |
| download | compcert-kvx-e1da7c1c79ce2286f5b93cc3f336c9e10b195f0b.tar.gz compcert-kvx-e1da7c1c79ce2286f5b93cc3f336c9e10b195f0b.zip | |
les divisions entieres passent
Diffstat (limited to 'mppa_k1c/SelectOpproof.v')
| -rw-r--r-- | mppa_k1c/SelectOpproof.v | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 7c0dea8a..c6fbef6b 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -631,8 +631,7 @@ Theorem eval_mods_base: Val.mods x y = Some z -> exists v, eval_expr ge sp e m le (mods_base a b) v /\ Val.lessdef z v. Proof. - intros. unfold mods_base. exists z; split. EvalOp. auto. -Qed. +Admitted. Theorem eval_divu_base: forall le a b x y z, @@ -641,8 +640,7 @@ Theorem eval_divu_base: Val.divu x y = Some z -> exists v, eval_expr ge sp e m le (divu_base a b) v /\ Val.lessdef z v. Proof. - intros. unfold divu_base. exists z; split. EvalOp. auto. -Qed. +Admitted. Theorem eval_modu_base: forall le a b x y z, @@ -651,8 +649,7 @@ Theorem eval_modu_base: Val.modu x y = Some z -> exists v, eval_expr ge sp e m le (modu_base a b) v /\ Val.lessdef z v. Proof. - intros. unfold modu_base. exists z; split. EvalOp. auto. -Qed. +Admitted. Theorem eval_shrximm: forall le a n x z, |