path: root/main.ml

(*
  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)

(* 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
  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 ()