diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-02-19 09:55:45 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-02-19 09:55:45 +0000 |
| commit | 3ec022950ec233a2af418aacd1755fce4d701724 (patch) | |
| tree | 154256c5c73fda06e874fb05695e14e610ba8ad4 /powerpc/SelectOpproof.v | |
| parent | 9aeba45962e8ba5cde5d81fb701a4c9a3963f4a5 (diff) | |
| download | compcert-kvx-3ec022950ec233a2af418aacd1755fce4d701724.tar.gz compcert-kvx-3ec022950ec233a2af418aacd1755fce4d701724.zip | |
Add option -Os to optimize for code size rather than for execution speed.
Refactored compilation flags that affect the Coq part (module Compopts).
Added support for C99 for loops with declarations.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2410 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc/SelectOpproof.v')
| -rw-r--r-- | powerpc/SelectOpproof.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 0cfa7074..4d26cf6c 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -14,6 +14,7 @@ Require Import Coqlib. Require Import Maps. +Require Import Compopts. Require Import AST. Require Import Integers. Require Import Floats. @@ -304,7 +305,8 @@ Proof. replace (Vint (Int.shl Int.one i)) with (Val.shl Vone (Vint i)). rewrite Val.shl_mul. apply eval_shlimm. auto. simpl. rewrite H0; auto with coqlib. destruct l. - intros. rewrite H1. simpl. + intros. destruct (optim_for_size tt). TrivialExists. + rewrite H1. simpl. exploit (eval_shlimm i (x :: le) (Eletvar 0) x). constructor; auto. intros [v1 [A1 B1]]. exploit (eval_shlimm i0 (x :: le) (Eletvar 0) x). constructor; auto. intros [v2 [A2 B2]]. exists (Val.add v1 v2); split. |