summaryrefslogtreecommitdiff
path: root/main.ml
diff options
context:
space:
mode:
Diffstat (limited to 'main.ml')
-rw-r--r--main.ml18
1 files changed, 13 insertions, 5 deletions
diff --git a/main.ml b/main.ml
index 5e9f087..2995e24 100644
--- a/main.ml
+++ b/main.ml
@@ -1,9 +1,10 @@
+open Cmdline
+
open Ast
open Num_domain
open Nonrelational
open Apron_domain
-open Abs_interp
module Interpret = Interpret.I
@@ -26,7 +27,7 @@ let ai_rel = ref false
let ai_itv_edd = ref false
let ai_rel_edd = ref false
let ai_root = ref "test"
-let ai_widen_delay = ref 3
+let ai_widen_delay = ref 5
let ai_no_time_scopes = ref ""
let ai_init_scopes = ref ""
let ai_disj_v = ref ""
@@ -106,9 +107,16 @@ let () =
if !ai_itv || !ai_rel || !ai_itv_edd || !ai_rel_edd then begin
let comma_split = Str.split (Str.regexp ",") in
let select_f x =
- if x = "all"
- then (fun _ -> true)
- else (fun i -> List.mem i (comma_split x))
+ if x = "all" then
+ (fun _ -> true)
+ else if x = "last" then
+ (fun i -> i.[0] = 'L')
+ else if String.length x > 5 && String.sub x 0 5 = "last+" then
+ let psl = comma_split
+ (String.sub x 5 (String.length x - 5)) in
+ (fun i -> i.[0] = 'L' || List.mem i psl)
+ else
+ (fun i -> List.mem i (comma_split x))
in
let rp = Typing.root_prog prog !ai_root
(select_f !ai_no_time_scopes)