aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Interp.ml
diff options
context:
space:
mode:
authorxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-11-12 13:42:22 +0000
committerxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-11-12 13:42:22 +0000
commitce4951549999f403446415c135ad1403a16a15c3 (patch)
treecac9bbb2fea29fce331916b277c38ed8fe29e471 /driver/Interp.ml
parentdcb9f48f51cec5e864565862a700c27df2a1a7e6 (diff)
downloadcompcert-kvx-ce4951549999f403446415c135ad1403a16a15c3.tar.gz
compcert-kvx-ce4951549999f403446415c135ad1403a16a15c3.zip
Globalenvs: allocate one-byte block with permissions Nonempty for each
function definition, so that comparisons between function pointers are correctly defined. AST, Globalenvs, and many other files: represent programs as a list of (function or variable) definitions instead of two lists, one for functions and the other for variables. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2067 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'driver/Interp.ml')
-rw-r--r--driver/Interp.ml55
1 files changed, 32 insertions, 23 deletions
diff --git a/driver/Interp.ml b/driver/Interp.ml
index fc0526a5..9031042f 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -87,9 +87,11 @@ let print_event p = function
let name_of_fundef prog fd =
let rec find_name = function
| [] -> "<unknown function>"
- | (id, fd') :: rem ->
+ | (id, Gfun fd') :: rem ->
if fd = fd' then extern_atom id else find_name rem
- in find_name prog.prog_funct
+ | (id, Gvar v) :: rem ->
+ find_name rem
+ in find_name prog.prog_defs
let name_of_function prog fn =
name_of_fundef prog (Internal fn)
@@ -468,11 +470,13 @@ let rec explore p prog ge time ss =
(* Massaging the source program *)
let unvolatile prog =
- let unvolatile_globvar (id, gv) =
- (id, if gv.gvar_volatile
- then {gv with gvar_readonly = false; gvar_volatile = false}
- else gv) in
- {prog with prog_vars = List.map unvolatile_globvar prog.prog_vars}
+ let unvolatile_globdef = function
+ | (id, Gvar gv) ->
+ (id, Gvar(if gv.gvar_volatile
+ then {gv with gvar_readonly = false; gvar_volatile = false}
+ else gv))
+ | idfd -> idfd in
+ {prog with prog_defs = List.map unvolatile_globdef prog.prog_defs}
let change_main_function p old_main old_main_ty =
let old_main = Evalof(Evar(old_main, old_main_ty), old_main_ty) in
@@ -483,24 +487,29 @@ let change_main_function p old_main old_main_ty =
let new_main_fn =
{ 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;
- prog_funct = (new_main_id, Internal new_main_fn) :: p.prog_funct }
+ { prog_main = new_main_id;
+ prog_defs = (new_main_id, Gfun(Internal new_main_fn)) :: p.prog_defs }
+
+let rec find_main_function name = function
+ | [] -> None
+ | (id, Gfun fd) :: gdl -> if id = name then Some fd else find_main_function name gdl
+ | (id, Gvar v) :: gdl -> find_main_function name gdl
let fixup_main p =
- try
- match type_of_fundef (List.assoc p.prog_main p.prog_funct) with
- | Tfunction(Tnil, Tint(I32, Signed, _)) ->
- Some p
- | Tfunction(Tcons(Tint _, Tcons(Tpointer(Tpointer(Tint(I8,_,_),_),_), Tnil)),
- Tint _) as ty ->
- Some (change_main_function p p.prog_main ty)
- | _ ->
- fprintf err_formatter "ERROR: wrong type for main() function";
- None
- with Not_found ->
- fprintf err_formatter "ERROR: no main() function";
- None
+ match find_main_function p.prog_main p.prog_defs with
+ | None ->
+ fprintf err_formatter "ERROR: no main() function";
+ None
+ | Some main_fd ->
+ match type_of_fundef main_fd with
+ | Tfunction(Tnil, Tint(I32, Signed, _)) ->
+ Some p
+ | Tfunction(Tcons(Tint _, Tcons(Tpointer(Tpointer(Tint(I8,_,_),_),_), Tnil)),
+ Tint _) as ty ->
+ Some (change_main_function p p.prog_main ty)
+ | _ ->
+ fprintf err_formatter "ERROR: wrong type for main() function";
+ None
(* Execution of a whole program *)