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