summaryrefslogblamecommitdiff
path: root/main.ml
blob: e09ac0e287cfb999faa5b551e41e7778a5296f2d (plain) (tree)
1
2
3
4
5
6
7
8
9
10
11
12
13












                                                                      
                         


                                                                       



                                               
                                                               
                       







                                               
(*
  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 = Nonrelational.NonRelational(Constant_domain.Constants)
module Interp = Interpret.Make(Env_dom)

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

(* parses arguments to get filename *)
let main () =
  match Array.to_list Sys.argv with
  | _::filename::_ -> doit filename
  | _ -> invalid_arg "no source file specified"

let _ = main ()