From 0be44be49c5be412a9d23e37c7b4554a9049ecbe Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 17 Nov 2013 16:18:46 +0000 Subject: 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 --- driver/Interp.ml | 23 +++-------------------- 1 file changed, 3 insertions(+), 20 deletions(-) (limited to 'driver/Interp.ml') 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 "\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') -- cgit