Let user choose domain
This commit is contained in:
parent
041d492986
commit
1fbdff1ec6
1 changed files with 5 additions and 10 deletions
15
analyzer.ml
15
analyzer.ml
|
@ -7,15 +7,8 @@
|
||||||
Ecole normale supérieure, Paris, France / CNRS / INRIA
|
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 Iterator
|
open Iterator
|
||||||
open Cfg
|
|
||||||
|
|
||||||
(* parse filename *)
|
(* parse filename *)
|
||||||
let doit filename = begin
|
let doit filename = begin
|
||||||
|
@ -24,9 +17,11 @@ let doit filename = begin
|
||||||
if !Options.verbose then
|
if !Options.verbose then
|
||||||
Format.printf "%a" Cfg_printer.print_cfg cfg;
|
Format.printf "%a" Cfg_printer.print_cfg cfg;
|
||||||
Cfg_printer.output_dot !Options.cfg_out cfg;
|
Cfg_printer.output_dot !Options.cfg_out cfg;
|
||||||
let fa = ConstIterator.iterate cfg in
|
let f = match !Options.domain with
|
||||||
let fb = SignIterator.iterate cfg in
|
| "signs" -> SignIterator.iterate cfg
|
||||||
Format.printf "@[<v 0>Failed asserts :@ %a@]" pp_asserts (ArcSet.inter fa fb) end
|
| "constants" -> ConstIterator.iterate cfg
|
||||||
|
| _ -> ConstIterator.iterate cfg in
|
||||||
|
Format.printf "@[<v 0>Failed asserts :@ %a@]" pp_asserts f end
|
||||||
|
|
||||||
|
|
||||||
(* parses arguments to get filename *)
|
(* parses arguments to get filename *)
|
||||||
|
|
Loading…
Reference in a new issue