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
---
 driver/Interp.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'driver/Interp.ml')

diff --git a/driver/Interp.ml b/driver/Interp.ml
index 25d363cf..5975ae39 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -454,6 +454,7 @@ let diagnose_stuck_expr p ge w f a kont e m =
     | RV, Ecomma(r1, r2, ty) -> diagnose RV r1
     | RV, Eparen(r1, ty) -> diagnose RV r1
     | RV, Ecall(r1, rargs, ty) -> diagnose RV r1 ||| diagnose_list rargs
+    | RV, Ebuiltin(ef, tyargs, rargs, ty) -> diagnose_list rargs
     | _, _ -> false in
   if found then true else begin
     let l = Cexec.step_expr ge do_external_function do_inline_assembly e w k a m in
-- 
cgit