From 1fbdff1ec6a5733317e6332f563890bea767201d Mon Sep 17 00:00:00 2001 From: Granahir2 Date: Sat, 1 Jun 2024 19:35:36 +0200 Subject: [PATCH] Let user choose domain --- analyzer.ml | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) diff --git a/analyzer.ml b/analyzer.ml index 8249800..b31255f 100644 --- a/analyzer.ml +++ b/analyzer.ml @@ -7,15 +7,8 @@ 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 Cfg (* parse filename *) let doit filename = begin @@ -24,9 +17,11 @@ let doit filename = begin if !Options.verbose then Format.printf "%a" Cfg_printer.print_cfg cfg; Cfg_printer.output_dot !Options.cfg_out cfg; - let fa = ConstIterator.iterate cfg in - let fb = SignIterator.iterate cfg in - Format.printf "@[Failed asserts :@ %a@]" pp_asserts (ArcSet.inter fa fb) end + let f = match !Options.domain with + | "signs" -> SignIterator.iterate cfg + | "constants" -> ConstIterator.iterate cfg + | _ -> ConstIterator.iterate cfg in + Format.printf "@[Failed asserts :@ %a@]" pp_asserts f end (* parses arguments to get filename *)