From 272a5b812b72f4c3e409ccdbeaf3476d95c4b552 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 15 Mar 2016 15:07:47 +0100 Subject: Deactivate warning 27 and added back removed code. The code was mostly there for documentation effort. So warning 27 is deactivated again. Bug 18349 --- driver/Driver.ml | 10 ++++----- driver/Interp.ml | 68 ++++++++++++++++++++++++++++---------------------------- 2 files changed, 39 insertions(+), 39 deletions(-) (limited to 'driver') diff --git a/driver/Driver.ml b/driver/Driver.ml index 7b245e6e..16267128 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -58,7 +58,7 @@ let command ?stdout args = if stdout <> None then Unix.close fd_out; match status with | Unix.WEXITED rc -> rc - | Unix.WSIGNALED _ | Unix.WSTOPPED _ -> + | Unix.WSIGNALED n | Unix.WSTOPPED n -> eprintf "Command '%s' killed on a signal.\n" argv.(0); -1 with Unix.Unix_error(err, fn, param) -> eprintf "Error executing '%s': %s: %s %s\n" @@ -681,13 +681,13 @@ let cmdline_actions = Exact "-fall", Self (fun _ -> set_all language_support_options); Exact "-fnone", Self (fun _ -> unset_all language_support_options); (* Debugging options *) - Exact "-g", Self (fun _ -> option_g := true; + Exact "-g", Self (fun s -> option_g := true; option_gdwarf := 3); - Exact "-gdwarf-2", Self (fun _ -> option_g:=true; + Exact "-gdwarf-2", Self (fun s -> option_g:=true; option_gdwarf := 2); - Exact "-gdwarf-3", Self (fun _ -> option_g := true; + Exact "-gdwarf-3", Self (fun s -> option_g := true; option_gdwarf := 3); - Exact "-frename-static", Self (fun _ -> option_rename_static:= true); + Exact "-frename-static", Self (fun s -> option_rename_static:= true); Exact "-gdepth", Integer (fun n -> if n = 0 || n <0 then begin option_g := false end else begin diff --git a/driver/Interp.ml b/driver/Interp.ml index 8dd4a7c9..e3a7d3b8 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -81,7 +81,7 @@ let name_of_fundef prog fd = | [] -> "" | (id, Gfun fd') :: rem -> if fd == fd' then extern_atom id else find_name rem - | (_, Gvar _) :: rem -> + | (id, Gvar v) :: rem -> find_name rem in find_name prog.Csyntax.prog_defs @@ -90,7 +90,7 @@ let name_of_function prog fn = | [] -> "" | (id, Gfun(Csyntax.Internal fn')) :: rem -> if fn == fn' then extern_atom id else find_name rem - | _ :: rem -> + | (id, _) :: rem -> find_name rem in find_name prog.Csyntax.prog_defs @@ -118,22 +118,22 @@ let print_val_list p vl = let print_state p (prog, ge, s) = match s with - | State(f, s, _, e, _) -> + | State(f, s, k, e, m) -> 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, _, e, _) -> + | ExprState(f, r, k, e, m) -> 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, _, _) -> + | Callstate(fd, args, k, m) -> 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, _, _) -> + | Returnstate(res, k, m) -> PrintCsyntax.print_pointer_hook := print_pointer ge.genv_genv Maps.PTree.empty; fprintf p "returning@ %a" print_val res @@ -220,10 +220,10 @@ let rank_state = function | Stuckstate -> assert false let mem_state = function - | State(_, _, _, _, m) -> m - | ExprState(_, _, _, _, m) -> m - | Callstate(_, _, _, m) -> m - | Returnstate(_, _, m) -> m + | 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 let compare_state s1 s2 = @@ -394,14 +394,14 @@ let do_external_function id sg ge w args m = | _ -> None -let do_inline_assembly _ _ _ _ _ _ = None +let do_inline_assembly txt sg ge w args m = 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 _ _ _ _ = +and world_io ge m id args = None and world_vload ge m chunk id ofs = @@ -416,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 _ time w ev = +let do_event p ge time w ev = if !trace >= 1 then fprintf p "@[Time %d: observable event:@ %a@]@." time print_event ev; @@ -438,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 _ a _ e m = +let diagnose_stuck_expr p ge w f a kont e m = let rec diagnose k a = (* diagnose subexpressions first *) let found = match k, a with - | 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 + | 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 | _, _ -> 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 (_,red) -> red = Cexec.Stuckred) l then begin + if List.exists (fun (ctx,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; @@ -496,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(_,_,s)) -> s = Stuckstate) l + || List.exists (fun (Cexec.TR(r,t,s)) -> s = Stuckstate) l then begin pp_set_max_boxes p 1000; fprintf p "@[Stuck state: %a@]@." print_state (prog, ge, s); @@ -529,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, _) -> + (fun (n, s, w) -> fprintf p "@[State %d.%d: @ %a@]@." time n print_state (prog, ge, s)) states @@ -579,7 +579,7 @@ let world_program prog = else {gv with gvar_init = []} in (id, Gvar gv') - | Gfun _ -> + | Gfun fd -> (id, gd) in {prog with Csyntax.prog_defs = List.map change_def prog.Csyntax.prog_defs} @@ -604,7 +604,7 @@ 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 - | (_, Gvar _) :: gdl -> find_main_function name gdl + | (id, Gvar v) :: gdl -> find_main_function name gdl let fixup_main p = match find_main_function p.Csyntax.prog_main p.prog_defs with -- cgit