diff options
Diffstat (limited to 'main.ml')
| -rw-r--r-- | main.ml | 44 |
1 files changed, 37 insertions, 7 deletions
@@ -13,19 +13,49 @@ open Abstract_syntax_tree -module Env_dom = Nonrelational.NonRelational(Constant_domain.Constants) -module Interp = Interpret.Make(Env_dom) +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) + +(* option parsing *) +let dump = ref false +let const_interp = ref false +let interv_interp = ref false +let poly_interp = ref false +let get_interp () = + if !interv_interp + then Interp_interv.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."; + "--poly-interp", Arg.Set poly_interp, "Use polyhedra lattice interpreter."; +] (* parse and print filename *) let doit filename = let prog = File_parser.parse_file filename in - Abstract_syntax_printer.print_prog Format.std_formatter prog; - Interp.interpret prog + if !dump then Abstract_syntax_printer.print_prog Format.std_formatter prog; + (get_interp ()) prog (* parses arguments to get filename *) let main () = - match Array.to_list Sys.argv with - | _::filename::_ -> doit filename - | _ -> invalid_arg "no source file specified" + Arg.parse options (set_var ifile) usage; + + if !ifile = "" then begin + Format.eprintf "No input file...@."; + exit 1 + end; + + doit !ifile let _ = main () |