From 3ec022950ec233a2af418aacd1755fce4d701724 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 19 Feb 2014 09:55:45 +0000 Subject: 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 --- powerpc/SelectOpproof.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'powerpc/SelectOpproof.v') 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. -- cgit