summaryrefslogtreecommitdiff
path: root/abstract
diff options
context:
space:
mode:
Diffstat (limited to 'abstract')
-rw-r--r--abstract/abs_interp_dynpart.ml77
1 files changed, 35 insertions, 42 deletions
diff --git a/abstract/abs_interp_dynpart.ml b/abstract/abs_interp_dynpart.ml
index 23df612..2ff950a 100644
--- a/abstract/abs_interp_dynpart.ml
+++ b/abstract/abs_interp_dynpart.ml
@@ -228,48 +228,41 @@ end = struct
loc = Hashtbl.create 2; counter = ref 2; } in
(* add initial disjunction : L/must_reset = tt, L/must_reset ≠ tt *)
- let rstc = BEnumCons(E_EQ, "L/must_reset", EItem bool_true) in
- let rstf = simplify_k [rstc] f in
- let rstf = simplify_k (get_root_true rstf) rstf in
- let nrstc = BEnumCons(E_NE, "L/must_reset", EItem bool_true) in
- let nrstf = simplify_k [nrstc] f in
- let nrstf = simplify_k (get_root_true nrstf) nrstf in
- Hashtbl.add env.loc 0
- {
- id = 0;
- depth = 0;
- def = apply_cl (top env) (conslist_of_f rstc);
- is_init = true;
-
- f = rstf;
- cl = conslist_of_f rstf;
-
- in_c = 0;
- v = bottom env;
-
- out_t = [];
- in_t = [];
- verif_g = [];
- violate_g = [];
- };
- Hashtbl.add env.loc 1
- {
- id = 1;
- depth = 0;
- def = apply_cl (top env) (conslist_of_f nrstc);
- is_init = false;
-
- f = nrstf;
- cl = conslist_of_f nrstf;
-
- in_c = 0;
- v = bottom env;
-
- out_t = [];
- in_t = [];
- verif_g = [];
- violate_g = [];
- };
+ let id = let i = ref 0 in fun () -> (incr i; !i) in
+ let add_loc is_init conds =
+ let cf = simplify_k conds f in
+ let cf = simplify_k (get_root_true cf) cf in
+ let id = id() in
+ Hashtbl.add env.loc id
+ {
+ id;
+ depth = 0;
+ def = apply_cl (top env) (conslist_of_f cf);
+ is_init;
+
+ f = cf;
+ cl = conslist_of_f cf;
+
+ in_c = 0;
+ v = bottom env;
+
+ out_t = [];
+ in_t = [];
+ verif_g = [];
+ violate_g = [];
+ };
+ in
+
+ add_loc true [BEnumCons(E_EQ, "L/must_reset", EItem bool_true)];
+
+ let rec div_g conds = function
+ | [] -> add_loc false conds
+ | (_, _, v)::r ->
+ add_loc false ((BEnumCons(E_NE, v, EItem bool_true))::conds);
+ div_g ((BEnumCons(E_EQ, v, EItem bool_true))::conds) r
+ in
+ div_g [BEnumCons(E_NE, "L/must_reset", EItem bool_true)] env.guarantees;
+
env