From 3ec022950ec233a2af418aacd1755fce4d701724 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
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/SelectOp.vp | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'powerpc/SelectOp.vp')

diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index bdb94bd..ad4f3b9 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -37,6 +37,7 @@
 *)
 
 Require Import Coqlib.
+Require Import Compopts.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
@@ -190,9 +191,12 @@ Definition mulimm_base (n1: int) (e2: expr) :=
   | i :: nil =>
       shlimm e2 i
   | i :: j :: nil =>
-      Elet e2
-        (Eop Oadd (shlimm (Eletvar 0) i :::
-                   shlimm (Eletvar 0) j ::: Enil))
+      if optim_for_size tt then
+        Eop (Omulimm n1) (e2:::Enil)
+      else
+        Elet e2
+          (Eop Oadd (shlimm (Eletvar 0) i :::
+                     shlimm (Eletvar 0) j ::: Enil))
   | _ =>
       Eop (Omulimm n1) (e2:::Enil)
   end.
-- 
cgit v1.2.3