aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Interp.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2016-03-10 13:35:48 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2016-03-10 13:35:48 +0100
commit5b05d3668571bd9b748b781b0cc29ae10f745f61 (patch)
treeaa235b80ff0666c34332be46664ae289d8afaa2c /driver/Interp.ml
parent272087e1bc62bead1d1e1bea3d64e12d013eea37 (diff)
downloadcompcert-kvx-5b05d3668571bd9b748b781b0cc29ae10f745f61.tar.gz
compcert-kvx-5b05d3668571bd9b748b781b0cc29ae10f745f61.zip
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.
Diffstat (limited to 'driver/Interp.ml')
-rw-r--r--driver/Interp.ml89
1 files changed, 43 insertions, 46 deletions
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 =
| [] -> "<unknown function>"
| (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
| [] -> "<unknown 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@ @[<hv 0>%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@ @[<hv 0>%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@ @[<hov 2>%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 "@[<hov 2>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 "@[<hov 2>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 "@[<hov 2>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 "@[<hov 2>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