Revised modeling of external functions and built-in functions: just axiomatize

them.


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

1 files changed, 3 insertions, 20 deletions

diff --git a/driver/Interp.ml b/driver/Interp.ml
index 6f9336ed..47779008 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -364,11 +364,7 @@ let do_printf ge m fmt args =
     end
   in scan 0 args; Buffer.contents b
 
-(* Implementing external functions *)
-
-let re_stub = Str.regexp "\\$[ifl]*$"
-
-let chop_stub name = Str.replace_first re_stub "" name
+(* Implementing external functions producing observable events *)
 
 let (>>=) opt f = match opt with None -> None | Some arg -> f arg
 
@@ -376,17 +372,7 @@ let rec world ge m =
   Determinism.World(world_io ge m, world_vload ge m, world_vstore ge m)
 
 and world_io ge m id args =
-  match chop_stub(extern_atom id), args with
-  | "printf", EVptr_global(id, ofs) :: args' ->
-      flush stderr;
-      begin match extract_string ge m id ofs with
-      | Some fmt -> print_string (do_printf ge m fmt args')
-      | None -> print_string "<bad printf>\n"
-      end;
-      flush stdout;
-      Some(EVint Integers.Int.zero, world ge m)
-  | _, _ ->
-      None
+  None
 
 and world_vload ge m chunk id ofs =
   Genv.find_symbol ge id >>= fun b ->
@@ -567,8 +553,7 @@ let rec explore_all p prog ge seen queue =
    executing events.  
    Volatile variables are turned into non-volatile ones, so that
      reads and writes can be performed.
-   Readonly variables are kept, for string literals in particular.
-   Writable variables are turned into empty vars, so that
+   Other variables are turned into empty vars, so that
      reads and writes just fail.
    Functions are preserved, although they are not used. *)
 
@@ -579,8 +564,6 @@ let world_program prog =
         let gv' =
           if gv.gvar_volatile then
             {gv with gvar_readonly = false; gvar_volatile = false}
-          else if gv.gvar_readonly then
-            gv
           else
             {gv with gvar_init = []} in
         (id, Gvar gv')