From 2514cd8a0767804a254addc9ac0ad8da2ce97dda Mon Sep 17 00:00:00 2001
From: Alex Auvolat <alex.auvolat@ansys.com>
Date: Thu, 19 Jun 2014 18:11:35 +0200
Subject: Actually, it works.

---
 abstract/abs_domain.ml  | 21 ++++++++++++++++++---
 abstract/abs_interp.ml  |  8 +++-----
 tests/source/half.scade |  2 +-
 3 files changed, 22 insertions(+), 9 deletions(-)

diff --git a/abstract/abs_domain.ml b/abstract/abs_domain.ml
index a30713a..64eefc7 100644
--- a/abstract/abs_domain.ml
+++ b/abstract/abs_domain.ml
@@ -223,8 +223,23 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct
 
     let var_itv x id =
         if List.mem_assoc id x.nvars
-          then IN (VMap.map (fun v -> ND.var_itv v id) x.value)
-          else not_implemented "var_itv for enum variable"
+          then
+            let x = List.fold_left
+              (fun x (v, _) ->
+                if v.[0] = 'N' || (String.length v > 3 && String.sub v 0 3 = "pre")
+                  then forgetvar x v else x)
+              x x.evars in
+            IN (VMap.map (fun v -> ND.var_itv v id) x.value)
+          else
+            let all = List.fold_left (fun a b -> SSet.add b a) SSet.empty
+                (List.assoc id x.evars) in
+            IE
+              (VMap.fold
+                (fun enum _ s ->
+                    try SSet.add (VarMap.find id enum) s
+                    with Not_found -> all)
+                x.value
+                SSet.empty)
 
     let set_disjunct x id p =
         { x with
@@ -356,7 +371,7 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct
           { x with value = VMap.empty }
 
     let print_all fmt x =
-        Format.fprintf fmt "@[<v 0>";
+        Format.fprintf fmt "@[<v>";
         VMap.iter
           (fun enum num ->
             Format.fprintf fmt "@[<hv 2>{ %a ∧@ %a }@]@ "
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index 7a53134..e55f199 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -127,14 +127,12 @@ end = struct
     let do_prog widen_delay rp =
       let st = init_state widen_delay rp in
 
-      let final, final_c = loop st st.env in
+      let final_nc, final = loop st st.env in
 
       Format.printf "@[<hov>F %a@]@.@."
-        E.print_all final;
-      (*
+        E.print_all final_nc;
       Format.printf "@[<hov>F' %a@]@.@."
-        E.print_all final_c;
-      *)
+        E.print_all final;
 
       let check_guarantee (id, f) =
         let cl = Formula.conslist_of_f f in
diff --git a/tests/source/half.scade b/tests/source/half.scade
index da90586..541e81c 100644
--- a/tests/source/half.scade
+++ b/tests/source/half.scade
@@ -1,4 +1,4 @@
-node test(i: int) returns (a, b, probe c: int; exit: bool)
+node test(i: int) returns (probe a, probe b, probe c: int; exit: bool)
 var
   la, lb: int;
   half: bool;
-- 
cgit v1.2.3