Merge of the "volatile" branch:

- native treatment of volatile accesses in CompCert C's semantics
- translation of volatile accesses to built-ins in SimplExpr
- native treatment of struct assignment and passing struct parameter by value
- only passing struct result by value remains emulated
- in cparser, remove emulations that are no longer used
- added C99's type _Bool and used it to express || and && more efficiently.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1814 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 20 insertions, 16 deletions

diff --git a/driver/Interp.ml b/driver/Interp.ml
index a1e01f02..50e512b2 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -113,12 +113,15 @@ let print_state prog p = function
   | Returnstate(res, k, m) ->
       fprintf p "returning@ %a"
               print_val res
+  | Stuckstate ->
+      fprintf p "stuck after an undefined expression"
 
 let mem_of_state = function
   | State(f, s, k, e, m) -> m
   | ExprState(f, r, k, e, m) -> m
   | Callstate(fd, args, k, m) -> m
   | Returnstate(res, k, m) -> m
+  | Stuckstate -> assert false
 
 (* Comparing memory states *)
 
@@ -211,6 +214,7 @@ let rank_state = function
   | ExprState _ -> 1
   | Callstate _ -> 2
   | Returnstate _ -> 3
+  | Stuckstate -> 4
 
 let compare_state s1 s2 =
   if s1 == s2 then 0 else
@@ -382,16 +386,17 @@ let do_step p prog ge time s =
         exit (Int32.to_int (camlint_of_coqint r))
       end
   | None ->
-      match Cexec.do_step ge world s with
-      | [] ->
-          if !trace = 1 then
-            fprintf p "@[<hov 2>Time %d: %a@]@." time (print_state prog) s;
-          fprintf p "ERROR: Undefined behavior@.";
-          fprintf p "@].";
-          exit 126
-      | l ->
-          List.iter (fun (t, s') -> do_events p ge time s t) l;
-          List.map snd l
+      let l = Cexec.do_step ge world s in
+      if l = [] || List.exists (fun (t,s) -> s = Stuckstate) l then begin
+        if !trace = 1 then
+          fprintf p "@[<hov 2>Time %d: %a@]@." time (print_state prog) s;
+        fprintf p "ERROR: Undefined behavior@.";
+        fprintf p "@].";
+        exit 126
+      end else begin
+        List.iter (fun (t, s') -> do_events p ge time s t) l;
+        List.map snd l
+      end
 
 let rec explore p prog ge time ss =
   let succs =
@@ -415,14 +420,13 @@ let unvolatile prog =
   {prog with prog_vars = List.map unvolatile_globvar prog.prog_vars}
 
 let change_main_function p old_main old_main_ty =
-  let tint = Tint(I32, Signed) in
   let old_main = Evalof(Evar(old_main, old_main_ty), old_main_ty) in
-  let arg1 = Eval(Vint(coqint_of_camlint 0l), tint) in
+  let arg1 = Eval(Vint(coqint_of_camlint 0l), type_int32s) in
   let arg2 = arg1 in
   let body =
-    Sreturn(Some(Ecall(old_main, Econs(arg1, Econs(arg2, Enil)), tint))) in
+    Sreturn(Some(Ecall(old_main, Econs(arg1, Econs(arg2, Enil)), type_int32s))) in
   let new_main_fn =
-    { fn_return = tint; fn_params = []; fn_vars = []; fn_body = body } in
+    { fn_return = type_int32s; fn_params = []; fn_vars = []; fn_body = body } in
   let new_main_id = intern_string "___main" in
   { p with
     prog_main = new_main_id;
@@ -431,9 +435,9 @@ let change_main_function p old_main old_main_ty =
 let fixup_main p =
   try
     match type_of_fundef (List.assoc p.prog_main p.prog_funct) with
-    | Tfunction(Tnil, Tint(I32, Signed)) ->
+    | Tfunction(Tnil, Tint(I32, Signed, _)) ->
         Some p
-    | Tfunction(Tcons(Tint _, Tcons(Tpointer(Tpointer(Tint(I8,_))), Tnil)),
+    | Tfunction(Tcons(Tint _, Tcons(Tpointer(Tpointer(Tint(I8,_,_),_),_), Tnil)),
                 Tint _) as ty ->
         Some (change_main_function p p.prog_main ty)
     | _ ->