From 5b05d3668571bd9b748b781b0cc29ae10f745f61 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 10 Mar 2016 13:35:48 +0100 Subject: Code cleanup. Removed some unused variables, functions etc. and resolved some problems which occur if all warnings except 3,4,9 and 29 are active. Bug 18394. --- driver/Interp.ml | 89 +++++++++++++++++++++++++++----------------------------- 1 file changed, 43 insertions(+), 46 deletions(-) (limited to 'driver/Interp.ml') diff --git a/driver/Interp.ml b/driver/Interp.ml index fb1c85f0..8dd4a7c9 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -12,20 +12,17 @@ (* Interpreting CompCert C sources *) -open Format +open !Format open Camlcoq -open Datatypes open AST open Integers open Values open Memory open Globalenvs open Events -open Ctypes -open Cop -open Csyntax +open !Ctypes +open !Csyntax open Csem -open Clflags (* Configuration *) @@ -84,18 +81,18 @@ let name_of_fundef prog fd = | [] -> "" | (id, Gfun fd') :: rem -> if fd == fd' then extern_atom id else find_name rem - | (id, Gvar v) :: rem -> + | (_, Gvar _) :: rem -> find_name rem - in find_name prog.prog_defs + in find_name prog.Csyntax.prog_defs let name_of_function prog fn = let rec find_name = function | [] -> "" - | (id, Gfun(Internal fn')) :: rem -> + | (id, Gfun(Csyntax.Internal fn')) :: rem -> if fn == fn' then extern_atom id else find_name rem - | (id, _) :: rem -> + | _ :: rem -> find_name rem - in find_name prog.prog_defs + in find_name prog.Csyntax.prog_defs let invert_local_variable e b = Maps.PTree.fold @@ -121,22 +118,22 @@ let print_val_list p vl = let print_state p (prog, ge, s) = match s with - | State(f, s, k, e, m) -> + | State(f, s, _, e, _) -> PrintCsyntax.print_pointer_hook := print_pointer ge.genv_genv e; fprintf p "in function %s, statement@ @[%a@]" (name_of_function prog f) PrintCsyntax.print_stmt s - | ExprState(f, r, k, e, m) -> + | ExprState(f, r, _, e, _) -> PrintCsyntax.print_pointer_hook := print_pointer ge.genv_genv e; fprintf p "in function %s, expression@ @[%a@]" (name_of_function prog f) PrintCsyntax.print_expr r - | Callstate(fd, args, k, m) -> + | Callstate(fd, args, _, _) -> PrintCsyntax.print_pointer_hook := print_pointer ge.genv_genv Maps.PTree.empty; fprintf p "calling@ @[%s(%a)@]" (name_of_fundef prog fd) print_val_list args - | Returnstate(res, k, m) -> + | Returnstate(res, _, _) -> PrintCsyntax.print_pointer_hook := print_pointer ge.genv_genv Maps.PTree.empty; fprintf p "returning@ %a" print_val res @@ -223,10 +220,10 @@ let rank_state = function | Stuckstate -> assert false let mem_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 + | State(_, _, _, _, m) -> m + | ExprState(_, _, _, _, m) -> m + | Callstate(_, _, _, m) -> m + | Returnstate(_, _, m) -> m | Stuckstate -> assert false let compare_state s1 s2 = @@ -397,14 +394,14 @@ let do_external_function id sg ge w args m = | _ -> None -let do_inline_assembly txt sg ge w args m = None +let do_inline_assembly _ _ _ _ _ _ = None (* Implementing external functions producing observable events *) let rec world ge m = lazy (Determinism.World(world_io ge m, world_vload ge m, world_vstore ge m)) -and world_io ge m id args = +and world_io _ _ _ _ = None and world_vload ge m chunk id ofs = @@ -419,7 +416,7 @@ and world_vstore ge m chunk id ofs ev = Mem.store chunk m b ofs v >>= fun m' -> Some(world ge m') -let do_event p ge time w ev = +let do_event p _ time w ev = if !trace >= 1 then fprintf p "@[Time %d: observable event:@ %a@]@." time print_event ev; @@ -441,30 +438,30 @@ let rec do_events p ge time w t = let (|||) a b = a || b (* strict boolean or *) -let diagnose_stuck_expr p ge w f a kont e m = +let diagnose_stuck_expr p ge w _ a _ e m = let rec diagnose k a = (* diagnose subexpressions first *) let found = match k, a with - | LV, Ederef(r, ty) -> diagnose RV r - | LV, Efield(r, f, ty) -> diagnose RV r - | RV, Evalof(l, ty) -> diagnose LV l - | RV, Eaddrof(l, ty) -> diagnose LV l - | RV, Eunop(op, r1, ty) -> diagnose RV r1 - | RV, Ebinop(op, r1, r2, ty) -> diagnose RV r1 ||| diagnose RV r2 - | RV, Ecast(r1, ty) -> diagnose RV r1 - | RV, Econdition(r1, r2, r3, ty) -> diagnose RV r1 - | RV, Eassign(l1, r2, ty) -> diagnose LV l1 ||| diagnose RV r2 - | RV, Eassignop(op, l1, r2, tyres, ty) -> diagnose LV l1 ||| diagnose RV r2 - | RV, Epostincr(id, l, ty) -> diagnose LV l - | RV, Ecomma(r1, r2, ty) -> diagnose RV r1 - | RV, Eparen(r1, tycast, ty) -> diagnose RV r1 - | RV, Ecall(r1, rargs, ty) -> diagnose RV r1 ||| diagnose_list rargs - | RV, Ebuiltin(ef, tyargs, rargs, ty) -> diagnose_list rargs + | LV, Ederef(r, _) -> diagnose RV r + | LV, Efield(r, _, _) -> diagnose RV r + | RV, Evalof(l, _) -> diagnose LV l + | RV, Eaddrof(l, _) -> diagnose LV l + | RV, Eunop(_, r1, _) -> diagnose RV r1 + | RV, Ebinop(_, r1, r2, _) -> diagnose RV r1 ||| diagnose RV r2 + | RV, Ecast(r1, _) -> diagnose RV r1 + | RV, Econdition(r1, _, _, _) -> diagnose RV r1 + | RV, Eassign(l1, r2, _) -> diagnose LV l1 ||| diagnose RV r2 + | RV, Eassignop(_, l1, r2, _, _) -> diagnose LV l1 ||| diagnose RV r2 + | RV, Epostincr(_, l, _) -> diagnose LV l + | RV, Ecomma(r1, _, _) -> diagnose RV r1 + | RV, Eparen(r1, _, _) -> diagnose RV r1 + | RV, Ecall(r1, rargs, _) -> diagnose RV r1 ||| diagnose_list rargs + | RV, Ebuiltin(_, _, rargs, _) -> 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 - if List.exists (fun (ctx,red) -> red = Cexec.Stuckred) l then begin + if List.exists (fun (_,red) -> red = Cexec.Stuckred) l then begin PrintCsyntax.print_pointer_hook := print_pointer ge.genv_genv e; fprintf p "@[Stuck subexpression:@ %a@]@." PrintCsyntax.print_expr a; @@ -499,7 +496,7 @@ let do_step p prog ge time s w = | None -> let l = Cexec.do_step ge do_external_function do_inline_assembly w s in if l = [] - || List.exists (fun (Cexec.TR(r,t,s)) -> s = Stuckstate) l + || List.exists (fun (Cexec.TR(_,_,s)) -> s = Stuckstate) l then begin pp_set_max_boxes p 1000; fprintf p "@[Stuck state: %a@]@." print_state (prog, ge, s); @@ -532,7 +529,7 @@ let rec explore_one p prog ge time s w = let rec explore_all p prog ge time states = if !trace >= 2 then begin List.iter - (fun (n, s, w) -> + (fun (n, s, _) -> fprintf p "@[State %d.%d: @ %a@]@." time n print_state (prog, ge, s)) states @@ -582,9 +579,9 @@ let world_program prog = else {gv with gvar_init = []} in (id, Gvar gv') - | Gfun fd -> + | Gfun _ -> (id, gd) in - {prog with prog_defs = List.map change_def prog.prog_defs} + {prog with Csyntax.prog_defs = List.map change_def prog.Csyntax.prog_defs} (* Massaging the program to get a suitable "main" function *) @@ -599,7 +596,7 @@ let change_main_function p old_main old_main_ty = fn_params = []; fn_vars = []; fn_body = body } in let new_main_id = intern_string "___main" in { prog_main = new_main_id; - prog_defs = (new_main_id, Gfun(Internal new_main_fn)) :: p.prog_defs; + Csyntax.prog_defs = (new_main_id, Gfun(Internal new_main_fn)) :: p.Csyntax.prog_defs; prog_public = p.prog_public; prog_types = p.prog_types; prog_comp_env = p.prog_comp_env } @@ -607,10 +604,10 @@ let change_main_function p old_main old_main_ty = 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 + | (_, Gvar _) :: gdl -> find_main_function name gdl let fixup_main p = - match find_main_function p.prog_main p.prog_defs with + match find_main_function p.Csyntax.prog_main p.prog_defs with | None -> fprintf err_formatter "ERROR: no main() function@."; None -- cgit