1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
|
(****************************************************************************)
(* the diy toolsuite *)
(* *)
(* Jade Alglave, University College London, UK. *)
(* Luc Maranget, INRIA Paris-Rocquencourt, France. *)
(* *)
(* Copyright 2012-present Institut National de Recherche en Informatique et *)
(* en Automatique and the authors. All rights reserved. *)
(* *)
(* This software is governed by the CeCILL-B license under French law and *)
(* abiding by the rules of distribution of free software. You can use, *)
(* modify and/ or redistribute the software under the terms of the CeCILL-B *)
(* license as circulated by CEA, CNRS and INRIA at the following URL *)
(* "http://www.cecill.info". We also give a copy in LICENSE.txt. *)
(****************************************************************************)
(********************)
(* Change condition *)
(********************)
open Printf
module type Out = sig
type t = out_channel
val open_file : string -> t
val close : t -> unit
end
module OutTar(O:Tar.Option) = struct
module T = Tar.Make(O)
type t = out_channel
let open_file name = open_out (T.outname name)
let close chan = close_out chan
end
module type Config = sig
val verbose : int
val hexa : bool
end
module Make(Config:Config)(Out:Out) =
struct
module D = Splitter.Default
module LU = LexUtils.Make(D)
module S = Splitter.Make(D)
let dump_outcomes name chan c =
let _k =
CondUtils.fold_outcomes c
(fun bds k ->
let fname = sprintf "cond%02i.txt" k in
Printf.fprintf chan "%s\n" fname ;
Misc.output_protect_gen
Out.open_file
(fun chan ->
Printf.fprintf chan "%s \"(%s)\"\n" name
(String.concat " /\\ "
(List.map
(fun (loc,v) ->
sprintf "%s=%s"
(MiscParser.dump_location loc)
(ToolsConstant.pp Config.hexa v))
bds)))
fname ;
k+1)
0 in
()
let from_chan fname in_chan =
try
let { Splitter.locs = locs; name;_} =
S.split fname in_chan in
let _,_,(constr_start,constr_end),(_last_start,_loc_eof) = locs in
let sec = constr_start,constr_end in
let cond =
match LogConstr.parse_locs_cond (LU.from_section sec in_chan) with
| Some (_,cond) -> cond
| None -> assert false in
dump_outcomes name.Name.name stdout cond ;
with LexMisc.Error (msg,pos) ->
Printf.eprintf
"%a: Lex error %s (in %s)\n" Pos.pp_pos pos msg fname ;
raise Misc.Exit
let from_file name =
try
Misc.input_protect
(fun in_chan -> from_chan name in_chan)
name
with Misc.Exit -> ()
| Misc.Fatal msg|Misc.UserError msg ->
eprintf "Fatal error, %s\n" msg ;
raise Misc.Exit
end
(**********)
(* Driver *)
(**********)
let tar = ref Filename.current_dir_name
and verbose = ref 0
and hexa = ref false
let set_tar x = tar := x
let arg = ref None
let opts =
[ "-v",
Arg.Unit (fun () -> incr verbose),
" be verbose";
"-hexa",Arg.Bool (fun b -> hexa := b),
" <bool> print numbers in hexadecimal";
"-o", Arg.String set_tar,
sprintf
"<name> output to directory or tar file <name>, default %s" !tar;
]
let prog =
if Array.length Sys.argv > 0 then Sys.argv.(0)
else "splitcond"
let () =
Arg.parse opts
(fun a -> match !arg with
| None -> arg := Some a
| Some _ ->
raise (Arg.Bad "takes exactly one argument"))
(sprintf "Usage %s [options] [test]*" prog)
let from_file =
let module X =
Make
(struct
let verbose = !verbose
let hexa = !hexa
end) in
let module T =
OutTar
(struct
let verbose = !verbose
let outname = Some !tar
end) in
let module Y = X(T) in
Y.from_file
let () = match !arg with
| Some arg ->
begin try from_file arg
with Misc.Exit -> () end
| None ->
eprintf "%s takes exactly one argument!!!\n" prog ;
exit 2
|
