Experiment on dynamic partitionning (guarantee initial partition).

3 files changed, 98 insertions, 98 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
 
 
diff --git a/doc/readme.pdf b/doc/readme.pdf
index aa680ca..89e5d4e 100644
--- a/doc/readme.pdf
+++ b/doc/readme.pdf
diff --git a/doc/readme.tm b/doc/readme.tm
index f21a66c..c6cde6d 100644
--- a/doc/readme.tm
+++ b/doc/readme.tm
@@ -1705,10 +1705,6 @@
   <subsection|Analyse des propriétés des nombres flottants>
 
   <\itemize>
-    <item>Implémenter un domaine d'intervalles permettant de gérer les
-    rationnels en précision arbitraire, ou se brancher sur le module Box
-    d'Apron
-
     <item>Utiliser un opérateur de widening aproprié (cf Astrée)
 
     <item>Implémenter la sémantique des nombres flottants machine (ce qui
@@ -1794,29 +1790,29 @@
     <associate|auto-3|<tuple|2.1|1>>
     <associate|auto-30|<tuple|5.2.3.3|?>>
     <associate|auto-31|<tuple|5.2.5.2|16>>
-    <associate|auto-32|<tuple|5.3|16>>
-    <associate|auto-33|<tuple|5.3.0.3|?>>
-    <associate|auto-34|<tuple|5.3.0.4|?>>
-    <associate|auto-35|<tuple|5.3.0.4.1|?>>
-    <associate|auto-36|<tuple|6|?>>
-    <associate|auto-37|<tuple|6.1|?>>
-    <associate|auto-38|<tuple|6.2|?>>
-    <associate|auto-39|<tuple|6.3|?>>
+    <associate|auto-32|<tuple|5.3|17>>
+    <associate|auto-33|<tuple|5.3.0.3|17>>
+    <associate|auto-34|<tuple|5.3.0.4|17>>
+    <associate|auto-35|<tuple|5.3.0.4.1|17>>
+    <associate|auto-36|<tuple|6|17>>
+    <associate|auto-37|<tuple|6.1|18>>
+    <associate|auto-38|<tuple|6.2|18>>
+    <associate|auto-39|<tuple|6.3|18>>
     <associate|auto-4|<tuple|2.2|2>>
-    <associate|auto-40|<tuple|6.3.1|?>>
-    <associate|auto-41|<tuple|6.3.1.1|?>>
-    <associate|auto-42|<tuple|6.3.1.2|?>>
-    <associate|auto-43|<tuple|6.3.2|?>>
-    <associate|auto-44|<tuple|6.3.2.1|?>>
-    <associate|auto-45|<tuple|6.3.2.2|?>>
-    <associate|auto-46|<tuple|6.3.3|?>>
-    <associate|auto-47|<tuple|6.3.3.1|?>>
-    <associate|auto-48|<tuple|6.3.3.2|?>>
-    <associate|auto-49|<tuple|7|?>>
+    <associate|auto-40|<tuple|6.3.1|18>>
+    <associate|auto-41|<tuple|6.3.1.1|18>>
+    <associate|auto-42|<tuple|6.3.1.2|18>>
+    <associate|auto-43|<tuple|6.3.2|19>>
+    <associate|auto-44|<tuple|6.3.2.1|19>>
+    <associate|auto-45|<tuple|6.3.2.2|19>>
+    <associate|auto-46|<tuple|6.3.3|19>>
+    <associate|auto-47|<tuple|6.3.3.1|19>>
+    <associate|auto-48|<tuple|6.3.3.2|19>>
+    <associate|auto-49|<tuple|7|19>>
     <associate|auto-5|<tuple|2.3|3>>
-    <associate|auto-50|<tuple|7.1|?>>
-    <associate|auto-51|<tuple|7.2|?>>
-    <associate|auto-52|<tuple|<with|mode|<quote|math>|\<bullet\>>|?>>
+    <associate|auto-50|<tuple|7.1|19>>
+    <associate|auto-51|<tuple|7.2|20>>
+    <associate|auto-52|<tuple|<with|mode|<quote|math>|\<bullet\>>|20>>
     <associate|auto-6|<tuple|2.3.1|3>>
     <associate|auto-7|<tuple|2.3.2|3>>
     <associate|auto-8|<tuple|2.3.3|3>>
@@ -1950,77 +1946,88 @@
       <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
       <no-break><pageref|auto-31><vspace|0.15fn>>
 
-      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|6<space|2spc>Partitionnement
-      dynamique> <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-32><vspace|0.5fn>
+      <with|par-left|<quote|1.5fn>|5.3<space|2spc>Partitionnement dynamique
+      <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-32>>
+
+      <with|par-left|<quote|6fn>|Découpage de base.
+      <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-33><vspace|0.15fn>>
+
+      <with|par-left|<quote|6fn>|Rafinement.
+      <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-34><vspace|0.15fn>>
+
+      Observations. <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-35><vspace|0.15fn>
 
-      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|7<space|2spc>Implémentation>
+      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|6<space|2spc>Implémentation>
       <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-33><vspace|0.5fn>
+      <no-break><pageref|auto-36><vspace|0.5fn>
 
-      <with|par-left|<quote|1.5fn>|7.1<space|2spc>Parsing et affichage de
+      <with|par-left|<quote|1.5fn>|6.1<space|2spc>Parsing et affichage de
       programmes SCADE <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-34>>
+      <no-break><pageref|auto-37>>
 
-      <with|par-left|<quote|1.5fn>|7.2<space|2spc>Interprète SCADE
+      <with|par-left|<quote|1.5fn>|6.2<space|2spc>Interprète SCADE
       <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-35>>
+      <no-break><pageref|auto-38>>
 
-      <with|par-left|<quote|1.5fn>|7.3<space|2spc>Analyse statique par
+      <with|par-left|<quote|1.5fn>|6.3<space|2spc>Analyse statique par
       interprétation abstraite <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-36>>
+      <no-break><pageref|auto-39>>
 
-      <with|par-left|<quote|3fn>|7.3.1<space|2spc>Domaine à disjonctions
+      <with|par-left|<quote|3fn>|6.3.1<space|2spc>Domaine à disjonctions
       simples <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-37>>
+      <no-break><pageref|auto-40>>
 
       <with|par-left|<quote|6fn>|Modes d'analyse
       <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-38><vspace|0.15fn>>
+      <no-break><pageref|auto-41><vspace|0.15fn>>
 
       <with|par-left|<quote|6fn>|Options de l'analyse
       <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-39><vspace|0.15fn>>
+      <no-break><pageref|auto-42><vspace|0.15fn>>
 
-      <with|par-left|<quote|3fn>|7.3.2<space|2spc>Domaine à disjonction par
+      <with|par-left|<quote|3fn>|6.3.2<space|2spc>Domaine à disjonction par
       graphe de décision <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-40>>
+      <no-break><pageref|auto-43>>
 
       <with|par-left|<quote|6fn>|Modes d'analyse
       <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-41><vspace|0.15fn>>
+      <no-break><pageref|auto-44><vspace|0.15fn>>
 
       <with|par-left|<quote|6fn>|Options de l'analyse
       <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-42><vspace|0.15fn>>
+      <no-break><pageref|auto-45><vspace|0.15fn>>
 
-      <with|par-left|<quote|3fn>|7.3.3<space|2spc>Analyse par partitionnement
+      <with|par-left|<quote|3fn>|6.3.3<space|2spc>Analyse par partitionnement
       dynamique <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-43>>
+      <no-break><pageref|auto-46>>
 
       <with|par-left|<quote|6fn>|Modes d'analyse
       <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-44><vspace|0.15fn>>
+      <no-break><pageref|auto-47><vspace|0.15fn>>
 
       <with|par-left|<quote|6fn>|Paramètres de l'analyse
       <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-45><vspace|0.15fn>>
+      <no-break><pageref|auto-48><vspace|0.15fn>>
 
-      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|8<space|2spc>Prolongements
+      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|7<space|2spc>Prolongements
       envisageables> <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-46><vspace|0.5fn>
+      <no-break><pageref|auto-49><vspace|0.5fn>
 
-      <with|par-left|<quote|1.5fn>|8.1<space|2spc>Analyse des propriétés des
+      <with|par-left|<quote|1.5fn>|7.1<space|2spc>Analyse des propriétés des
       nombres flottants <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-47>>
+      <no-break><pageref|auto-50>>
 
-      <with|par-left|<quote|1.5fn>|8.2<space|2spc>Analyse de programmes \S
+      <with|par-left|<quote|1.5fn>|7.2<space|2spc>Analyse de programmes \S
       taille réelle \T <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-48>>
+      <no-break><pageref|auto-51>>
 
-      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|9<space|2spc>Références>
+      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|Références>
       <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-49><vspace|0.5fn>
+      <no-break><pageref|auto-52><vspace|0.5fn>
     </associate>
   </collection>
 </auxiliary>
\ No newline at end of file