blob: 7e6279c06cff8ee601a516504eea18f3c2ee9a7a (
plain) (
blame)
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
|
(*
Cours "Sémantique et Application à la Vérification de programmes"
Antoine Miné 2014
Ecole normale supérieure, Paris, France / CNRS / INRIA
*)
(*
Simple driver: parses the file given as argument and prints it back.
You should modify this file to call your functions instead!
*)
open Abstract_syntax_tree
module Env_dom_const = Nonrelational.NonRelational(Constant_domain.Constants)
module Interp_const = Interpret.Make(Env_dom_const)
module Env_dom_interv = Nonrelational.NonRelational(Intervals_domain.Intervals)
module Interp_interv = Interpret.Make(Env_dom_interv)
module Interp_rel = Interpret.Make(Relational_apron.RelationalDomain)
(* option parsing *)
let dump = ref false
let const_interp = ref false
let interv_interp = ref false
let rel_interp = ref false
let get_interp () =
if !interv_interp then
Interp_interv.interpret
else if !rel_interp then
Interp_rel.interpret
else
Interp_const.interpret
let ifile = ref ""
let set_var v s = v := s
let usage = "usage: analyzer [options] file.c"
let options = [
"--dump", Arg.Set dump, "Dump program source.";
"--const-interp", Arg.Set const_interp, "Use constant lattice interpreter.";
"--interv-interp", Arg.Set interv_interp, "Use interval lattice interpreter.";
"--rel-interp", Arg.Set rel_interp, "Use relationnal (Apron) lattice.";
]
(* parse and print filename *)
let doit filename =
let prog = File_parser.parse_file filename in
if !dump then Abstract_syntax_printer.print_prog Format.std_formatter prog;
(get_interp ()) prog
(* parses arguments to get filename *)
let main () =
Arg.parse options (set_var ifile) usage;
if !ifile = "" then begin
Format.eprintf "No input file...@.";
exit 1
end;
doit !ifile
let _ = main ()
|
