diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-10 13:35:48 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-10 13:35:48 +0100 |
| commit | 5b05d3668571bd9b748b781b0cc29ae10f745f61 (patch) | |
| tree | aa235b80ff0666c34332be46664ae289d8afaa2c /backend/Linearizeaux.ml | |
| parent | 272087e1bc62bead1d1e1bea3d64e12d013eea37 (diff) | |
| download | compcert-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 'backend/Linearizeaux.ml')
| -rw-r--r-- | backend/Linearizeaux.ml | 13 |
1 files changed, 5 insertions, 8 deletions
diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml index 71ee2e56..41a98873 100644 --- a/backend/Linearizeaux.ml +++ b/backend/Linearizeaux.ml @@ -10,10 +10,7 @@ (* *) (* *********************************************************************) -open Coqlib -open Datatypes open LTL -open Lattice open Maps open Camlcoq @@ -82,13 +79,13 @@ let basic_blocks f joins = let rec do_instr_list = function | [] -> assert false | Lbranch s :: _ -> next_in_block blk minpc s - | Ltailcall (sig0, ros) :: _ -> end_block blk minpc - | Lcond (cond, args, ifso, ifnot) :: _ -> + | Ltailcall _ :: _ -> end_block blk minpc + | Lcond (_, _, ifso, ifnot) :: _ -> end_block blk minpc; start_block ifso; start_block ifnot - | Ljumptable(arg, tbl) :: _ -> + | Ljumptable(_, tbl) :: _ -> end_block blk minpc; List.iter start_block tbl | Lreturn :: _ -> end_block blk minpc - | instr :: b' -> do_instr_list b' in + | _ :: b' -> do_instr_list b' in do_instr_list b (* next_in_block: check if join point and either extend block or start block *) @@ -113,5 +110,5 @@ let flatten_blocks blks = (* Build the enumeration *) -let enumerate_aux f reach = +let enumerate_aux f _ = flatten_blocks (basic_blocks f (join_points f)) |