diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-20 11:30:49 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-20 11:30:49 +0100 |
| commit | c10a470bf10e0f1caf0df9d8491ae01464146b55 (patch) | |
| tree | fee0729c08881b3997e558345e05e0c17aa66362 /backend | |
| parent | 37e78559ccf9b1db585442ff0b8ca4cf2d613386 (diff) | |
| parent | 7bd5d66520bfae2bdef6573a40798a5d6375be79 (diff) | |
| download | compcert-kvx-c10a470bf10e0f1caf0df9d8491ae01464146b55.tar.gz compcert-kvx-c10a470bf10e0f1caf0df9d8491ae01464146b55.zip | |
Merge branch 'mppa-mul' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-mul
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/SelectDivproof.v | 2 | ||||
| -rw-r--r-- | backend/SplitLongproof.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v index 3fd50b76..9b99fcbf 100644 --- a/backend/SelectDivproof.v +++ b/backend/SelectDivproof.v @@ -702,7 +702,7 @@ Proof. || Int.eq i (Int.repr Int.min_signed) && Int.eq n2 Int.mone) eqn:Z2; inv DIV. destruct (Int.is_power2 n2) as [l | ] eqn:P2. - destruct (Int.ltu l (Int.repr 31)) eqn:LT31. - + exploit (eval_shrximm ge sp e m (Vint i :: le) (Eletvar O)). + + exploit (eval_shrximm prog sp e m (Vint i :: le) (Eletvar O)). constructor. simpl; eauto. eapply Val.divs_pow2; eauto. intros [v1 [X LD]]. inv LD. econstructor; split. econstructor. eauto. diff --git a/backend/SplitLongproof.v b/backend/SplitLongproof.v index 3b74b216..a74276c7 100644 --- a/backend/SplitLongproof.v +++ b/backend/SplitLongproof.v @@ -313,7 +313,7 @@ Theorem eval_longofint: unary_constructor_sound longofint Val.longofint. Proof. red; intros. unfold longofint. destruct (longofint_match a). - InvEval. econstructor; split. apply eval_longconst. auto. -- exploit (eval_shrimm ge sp e m (Int.repr 31) (x :: le) (Eletvar 0)). EvalOp. +- exploit (eval_shrimm prog sp e m (Int.repr 31) (x :: le) (Eletvar 0)). EvalOp. intros [v1 [A B]]. econstructor; split. EvalOp. destruct x; simpl; auto. |