Plug into Apron Box domain for intervals.

7 files changed, 280 insertions, 150 deletions

diff --git a/Makefile b/Makefile
index 1faacde..07daf1d 100644
--- a/Makefile
+++ b/Makefile
@@ -34,7 +34,7 @@ all: $(BIN)
 
 $(BIN): $(SRC)
 	ocamlbuild -Is $(SRCDIRS) -cflags '-I +zarith -I +apron -I +gmp -I +str' \
-			-lflags '-I +zarith -I +apron -I +gmp -I +str str.cmxa zarith.cmxa bigarray.cmxa gmp.cmxa apron.cmxa polkaMPQ.cmxa unix.cmxa octMPQ.cmxa' \
+			-lflags '-I +zarith -I +apron -I +gmp -I +str str.cmxa zarith.cmxa bigarray.cmxa gmp.cmxa apron.cmxa polkaMPQ.cmxa unix.cmxa octMPQ.cmxa boxMPQ.cmxa' \
 		    main.native \
 			-classic-display
 	mv main.native $(BIN)
diff --git a/abstract/apron_domain.ml b/abstract/apron_domain.ml
index 58cd544..e1b3007 100644
--- a/abstract/apron_domain.ml
+++ b/abstract/apron_domain.ml
@@ -11,18 +11,16 @@ open Apron
   Mostly direct translation between the two.
 *)
 
-(* Polyhedra *)
-
-module ND_Poly : NUMERICAL_ENVIRONMENT_DOMAIN = struct
+module Common = struct
 
-    (* manager *)
-    type man = Polka.loose Polka.t
-    let manager = Polka.manager_alloc_loose ()
-
-    type itv = Interval.t
-
-    (* abstract elements *)
-    type t = man Abstract1.t
+    let v_env vars = 
+        let intv = List.map
+              (fun (s, _) -> Var.of_string s)
+              (List.filter (fun (_, n) -> not n) vars) in
+        let realv = List.map
+              (fun (s, _) -> Var.of_string s)
+              (List.filter (fun (_, n) -> n) vars) in
+        (Environment.make (Array.of_list intv) (Array.of_list realv))
 
     (* direct translation of numerical expressions into Apron tree expressions *)
     let rec texpr_of_nexpr = function
@@ -67,16 +65,107 @@ module ND_Poly : NUMERICAL_ENVIRONMENT_DOMAIN = struct
           | CONS_GE -> Tcons1.SUPEQ
         in Tcons1.make (Texpr1.of_expr env (texpr_of_nexpr eq)) op
 
+end
+
+(* Apron Boxes (intervals) *)
+
+module ND_Box : NUMERICAL_ENVIRONMENT_DOMAIN = struct
+
+    open Common
+
+    (* manager *)
+    type man = Box.t
+    let manager = Box.manager_alloc ()
+
+    type itv = Interval.t
+
+    (* abstract elements *)
+    type t = man Abstract1.t
+
     (* implementation *)
-    let v_env vars = 
-        let intv = List.map
-              (fun (s, _) -> Var.of_string s)
-              (List.filter (fun (_, n) -> not n) vars) in
-        let realv = List.map
-              (fun (s, _) -> Var.of_string s)
-              (List.filter (fun (_, n) -> n) vars) in
-        (Environment.make (Array.of_list intv) (Array.of_list realv))
+    let top vars =
+      Abstract1.top manager (v_env vars)
+    let bottom vars = Abstract1.bottom manager (v_env vars)
+    let is_bot = Abstract1.is_bottom manager
+    let is_top = Abstract1.is_top manager
+
+    let forgetvar x id =
+        let v = [| Var.of_string id |] in
+        Abstract1.forget_array manager x v false
+
+    let vars x =
+        let (ivt, fvt) = Environment.vars (Abstract1.env x) in
+        let ivl = List.map Var.to_string (Array.to_list ivt) in
+        let fvl = List.map Var.to_string (Array.to_list fvt) in
+        (List.map (fun x -> x, false) ivl) @ (List.map (fun x -> x, true) fvl)
+
+    let vbottom x =
+        Abstract1.bottom manager (Abstract1.env x)
+
+    let project x id =
+        Abstract1.bound_variable manager x (Var.of_string id)
+
+    (* Apply some formula to the environment *)
+    let apply_cl x cons =
+        let env = Abstract1.env x in
+        let tca = Array.of_list (List.map (tcons_of_cons env) cons) in
+        let ar = Tcons1.array_make env (Array.length tca) in
+        Array.iteri (Tcons1.array_set ar) tca;
+        Abstract1.meet_tcons_array manager x ar
+
+    let apply_cons x cons = apply_cl x [cons]
+
+
+    let assign x eqs =
+      let env = Abstract1.env x in
+      let vars = Array.of_list
+        (List.map (fun (id, _) -> Var.of_string id) eqs) in
+      let vals = Array.of_list
+        (List.map (fun (_, v) -> Texpr1.of_expr env (texpr_of_nexpr v)) eqs) in
+      Abstract1.assign_texpr_array manager x vars vals None
+
+    
+    (* Ensemblistic operations *)
+    let join = Abstract1.join manager
+    let meet = Abstract1.meet manager
+    let widen = Abstract1.widening manager
+
+    let subset = Abstract1.is_leq manager
+    let eq = Abstract1.is_eq manager
+
+    (* Pretty-printing *)
+    let print fmt x =
+        Abstract1.minimize manager x;
+        Format.fprintf fmt "%a@?" Abstract1.print x
+
+    let print_vars fmt x idl = 
+        let prevars = vars x in
+        let rm_vars_l = List.filter (fun (id, _) -> not (List.mem id idl)) prevars in
+        let rm_vars = Array.of_list
+          (List.map (fun (id, _) -> Var.of_string id) rm_vars_l) in
+        let xx = Abstract1.forget_array manager x rm_vars false in
+        print fmt xx
+
+    let print_itv = Interval.print
+
+end
+
+(* Polyhedra *)
+
+module ND_Poly : NUMERICAL_ENVIRONMENT_DOMAIN = struct
 
+    open Common
+
+    (* manager *)
+    type man = Polka.loose Polka.t
+    let manager = Polka.manager_alloc_loose ()
+
+    type itv = Interval.t
+
+    (* abstract elements *)
+    type t = man Abstract1.t
+
+    (* implementation *)
     let top vars =
       Abstract1.top manager (v_env vars)
     let bottom vars = Abstract1.bottom manager (v_env vars)
@@ -129,7 +218,7 @@ module ND_Poly : NUMERICAL_ENVIRONMENT_DOMAIN = struct
 
     (* Pretty-printing *)
     let print fmt x =
-        if not (Oct.manager_is_oct manager) then Abstract1.minimize manager x;
+        Abstract1.minimize manager x;
         Format.fprintf fmt "%a@?" Abstract1.print x
 
     let print_vars fmt x idl = 
@@ -149,6 +238,8 @@ end
 
 module ND_Oct : NUMERICAL_ENVIRONMENT_DOMAIN = struct
 
+    open Common
+
     (* manager *)
     type man = Oct.t
     let manager = Oct.manager_alloc()
@@ -158,59 +249,7 @@ module ND_Oct : NUMERICAL_ENVIRONMENT_DOMAIN = struct
     (* abstract elements *)
     type t = man Abstract1.t
 
-    (* direct translation of numerical expressions into Apron tree expressions *)
-    let rec texpr_of_nexpr = function
-        | NIdent id -> Texpr1.Var (Var.of_string id)
-        | NIntConst i -> Texpr1.Cst (Coeff.s_of_mpqf (Mpqf.of_int i))
-        | NRealConst r -> Texpr1.Cst (Coeff.s_of_mpqf (Mpqf.of_float r))
-        | NUnary(AST_UPLUS, e, is_real) ->
-            Texpr1.Unop(
-                Texpr1.Cast,
-                texpr_of_nexpr e,
-                (if is_real then Texpr1.Real else Texpr1.Int),
-                Texpr1.Rnd)
-        | NUnary(AST_UMINUS, e, is_real) ->
-            (* APRON bug ? Unary negate seems to not work correctly... *)
-            Texpr1.Binop(
-                Texpr1.Sub,
-                Texpr1.Cst(Coeff.s_of_mpqf (Mpqf.of_string "0")),
-                (texpr_of_nexpr e),
-                (if is_real then Texpr1.Real else Texpr1.Int),
-                Texpr1.Rnd)
-        | NBinary(op, e1, e2, is_real) ->
-            let f = match op with
-            | AST_PLUS -> Texpr1.Add
-            | AST_MINUS -> Texpr1.Sub
-            | AST_MUL -> Texpr1.Mul
-            | AST_DIV -> Texpr1.Div
-            | AST_MOD -> Texpr1.Mod
-            in
-            Texpr1.Binop(
-                  f,
-                  (texpr_of_nexpr e1),
-                  (texpr_of_nexpr e2),
-                  (if is_real then Texpr1.Real else Texpr1.Int),
-                  Texpr1.Rnd)
-    
-    (* direct translation of constraints into Apron constraints *)
-    let tcons_of_cons env (eq, op) =
-        let op = match op with
-          | CONS_EQ -> Tcons1.EQ
-          | CONS_NE -> Tcons1.DISEQ
-          | CONS_GT -> Tcons1.SUP
-          | CONS_GE -> Tcons1.SUPEQ
-        in Tcons1.make (Texpr1.of_expr env (texpr_of_nexpr eq)) op
-
     (* implementation *)
-    let v_env vars = 
-        let intv = List.map
-              (fun (s, _) -> Var.of_string s)
-              (List.filter (fun (_, n) -> not n) vars) in
-        let realv = List.map
-              (fun (s, _) -> Var.of_string s)
-              (List.filter (fun (_, n) -> n) vars) in
-        (Environment.make (Array.of_list intv) (Array.of_list realv))
-
     let top vars =
       Abstract1.top manager (v_env vars)
     let bottom vars = Abstract1.bottom manager (v_env vars)
@@ -263,7 +302,6 @@ module ND_Oct : NUMERICAL_ENVIRONMENT_DOMAIN = struct
 
     (* Pretty-printing *)
     let print fmt x =
-        if not (Oct.manager_is_oct manager) then Abstract1.minimize manager x;
         Format.fprintf fmt "%a@?" Abstract1.print x
 
     let print_vars fmt x idl = 
diff --git a/doc/readme.pdf b/doc/readme.pdf
index 4a97029..aa680ca 100644
--- a/doc/readme.pdf
+++ b/doc/readme.pdf
diff --git a/doc/readme.tm b/doc/readme.tm
index 8622a9a..f21a66c 100644
--- a/doc/readme.tm
+++ b/doc/readme.tm
@@ -823,20 +823,22 @@
   peut être caractérisée par sa fonction de concrétisation :
 
   <\eqnarray*>
-    <tformat|<table|<row|<cell|\<gamma\><rsub|\<bbb-M\>>>|<cell|:>|<cell|\<cal-D\><rsup|#>\<rightarrow\>\<cal-P\><around*|(|\<bbb-M\>|)>>>>>
+    <tformat|<table|<row|<cell|\<gamma\>>|<cell|:>|<cell|\<cal-D\><rsup|#>\<rightarrow\>\<cal-P\><around*|(|\<bbb-M\>|)>>>>>
   </eqnarray*>
 
   \ On peut aussi généralement s'appuyer sur l<math|>'existence d'une
   fonction d'abstraction :
 
   <\eqnarray*>
-    <tformat|<table|<row|<cell|\<alpha\><rsub|\<bbb-M\>>>|<cell|:>|<cell|\<cal-P\><around*|(|\<bbb-M\>|)>\<rightarrow\>\<cal-D\><rsup|#>>>>>
+    <tformat|<table|<row|<cell|\<alpha\>>|<cell|:>|<cell|\<cal-P\><around*|(|\<bbb-M\>|)>\<rightarrow\>\<cal-D\><rsup|#>>>>>
   </eqnarray*>
 
   Cette fonction fait correspondre à une partie de <math|\<bbb-M\>> sa
-  meilleure approximation dans le domaine abstrait (par exemple dans le cas
-  des polyèdres, l'abstraction d'un ensemble fini de points est leur
-  enveloppe convexe, mais un cercle n'a pas de meilleure abstraction).
+  meilleure approximation dans le domaine abstrait, lorsque celle-ci existe
+  (par exemple dans le cas des polyèdres, l'abstraction d'un ensemble fini de
+  points est leur enveloppe convexe, mais un cercle n'a pas de meilleure
+  abstraction). En pratique la fonction d'abstraction n'est pas très
+  utilisée.
 
   Dans tous les cas, on s'attend à ce que
   <math|\<forall\>x\<in\>\<cal-D\><rsup|#>,x\<sqsubseteq\>\<alpha\><around*|(|\<gamma\><around*|(|x|)>|)>>
@@ -1441,11 +1443,65 @@
     Dans ce cas, on s'arrête si <math|s<rsub|n+1>=s<rsub|n>>.
   </itemize>
 
-  <section|Partitionnement dynamique>
+  <subsection|Partitionnement dynamique>
 
-  Une autre approche à base de partitionnement dynamique a été tentée, mais
-  elle n'a pas donné de très bons résultats par manque d'une heuristique sur
-  les partitionnements à effectuer. Détails à venir.
+  Une autre approche à base de partitionnement dynamique a été tentée (cf
+  <em|Dynamic Partitionning in Analyses of Numerical Properties>), mais elle
+  n'a pas donné de très bons résultats par manque d'une heuristique sur les
+  partitionnements à effectuer.
+
+  L'idée de base consiste à se donner une liste de conditions
+  <math|d<rsub|1>,d<rsub|2>,\<ldots\>,d<rsub|n>> qui définissent <math|n>
+  parties de <math|S<rsup|#>> (en principe disjointes, mais les
+  approximations mènent parfois à des recoupenents). On étudie les parties
+  (ou <em|lieux>) <math|S<rsub|i><rsup|#>=<around*|\<llbracket\>|d<rsub|i>|\<rrbracket\>><around*|(|S<rsup|#>|)>>
+  comme un système de transitions pour lequel on calcule un point fixe par
+  itérations chaotiques.
+
+  Les conditions <math|d<rsub|i>> sont données par une heuristique qui
+  découpe à chaque rafinement un des lieux <math|S<rsub|i><rsup|#>> en
+  plusieurs sous-lieux.
+
+  <paragraph|Découpage de base.>Le découpage de base est généralement : init
+  ; non init et propriété vérifiée ; non init et propriété non vérifiée.
+
+  <paragraph|Rafinement.>On note <math|S<rsub|i><rsup|#>\<rightarrow\>S<rsup|#><rsub|j>>
+  si dans notre sur-approximation on peut être à un cycle dans
+  <math|S<rsub|i><rsup|#>> et dans le suivant dans <math|S<rsub|j><rsup|#>>.
+
+  On recherche un lieu <math|S<rsub|i><rsup|#>> et une condition <math|c>
+  apparaissant dans le programme (ou la négation d'une telle condition) tel
+  qu'il existe un état <math|S<rsub|j><rsup|#>> ayant les propriétés
+  suivantes :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|S<rsub|j><rsup|#>>|<cell|\<rightarrow\>>|<cell|S<rsub|i><rsup|#>>>|<row|<cell|S<rsub|j><rsup|#>>|<cell|\<nrightarrow\>>|<cell|<around*|\<llbracket\>|c|\<rrbracket\>>S<rsub|i><rsup|#>>>>>
+  </eqnarray*>
+
+  On peut aussi le faire dans l'autre sens :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|S<rsub|i><rsup|#>>|<cell|\<rightarrow\>>|<cell|S<rsub|j><rsup|#>>>|<row|<cell|<around*|\<llbracket\>|c|\<rrbracket\>>S<rsub|i><rsup|#>>|<cell|\<nrightarrow\>>|<cell|S<rsub|j><rsup|#>>>>>
+  </eqnarray*>
+
+  Si une telle condition est détectée, alors on peut diviser le lieu
+  <math|S<rsub|i><rsup|#>> en deux parties,
+  <math|<around*|\<llbracket\>|c|\<rrbracket\>>S<rsub|i><rsup|#>> et
+  <math|<around*|\<llbracket\>|\<neg\>c|\<rrbracket\>>S<rsub|i><rsup|#>>,
+  c'est-à-dire qu'on pose comme nouvelles définitions
+  <math|d<rsub|1>,\<ldots\>,d<rsub|i-1>,c\<wedge\>d<rsub|i>,\<neg\>c\<wedge\>d<rsub|i>,d<rsub|i+1>,\<ldots\>,d<rsub|n>>.
+  On refait ensuite un point fixe. Notre analyse est en principe plus fine,
+  donc on espère trouver des lieux inacessibles.
+
+  <subparagraph|Observations.>En pratique ça ne marche pas très bien car les
+  rafinements ne sont pas effectués dans le bon ordre. Dans le papier
+  sus-cité, une double analyse en avant et en arrière était utilisée pour
+  trouver l'intersection des valeurs accessibles depuis l'état initial et
+  co-accessibles jusqu'à un état qui provoque une erreur (ie dont la
+  définition est : la propriété est violée), mais nous n'avons pas tenté
+  d'implémenter une telle analyse, qui serait sans doute bien plus précise.
+  Remarquons que l'implémentation de <name|B.Jeannet> pour LUSTRE est
+  disponnible sur sa page web (c'est l'outil NBac).
 
   <section|Implémentation>
 
@@ -1463,13 +1519,20 @@
     logique ; quelques simplifications sur les formules logiques
     (<verbatim|abstract/formula.ml>, <verbatim|abstract/transform.ml>).
 
-    <item>domaine numérique non-relationnel basé sur les intervalles ;
-    domaine relationnel basé sur la bibliothèque externe Apron
-    (<verbatim|abstract/num_domain.ml>, <verbatim|abstract/nonrelational.ml>,
-    <verbatim|abstract/apron_domain.ml>, ...)
+    <item>trois domaines numériques basés sur Apron : intervalles, polyèdres
+    et octogones (<verbatim|abstract/apron_domain.ml>)
+
+    <item>vestige d'une implémentation \S maison \T d'un domaine
+    non-relationnel à base d'intervalles (<verbatim|abstract/num_domain.ml>,
+    <verbatim|abstract/nonrelational.ml>,
+    <verbatim|abstract/value_domain.ml>, <verbatim|abstract/intervals_domain.ml>)
 
-    <item>deux domaines abstraits et analyseur statique correspondant
-    (<verbatim|abstract/abs_interp.ml>, <verbatim|abstract/abs_interp_edd.ml>)
+    <item>deux domaines abstraits à disjonctions et procédures d'analyse
+    statique correspondantes (<verbatim|abstract/abs_interp.ml>,
+    <verbatim|abstract/abs_interp_edd.ml>)
+
+    <item>procédure d'analyse par partitionnement dynamique
+    (<verbatim|abstract/abs_interp_dynpart.ml>)
   </itemize>
 
   En nous basant sur les options de la ligne de commande, nous allons
@@ -1518,8 +1581,10 @@
     en s'appuyant sur le domaine non-relationnel à base d'intervalles pour la
     partie numérique
 
-    <item><verbatim|--ai-rel> : de même mais utilise le domaine abstrait
-    relationnel basé sur Apron (polyèdres) pour la partie numérique
+    <item><verbatim|--ai-poly> : de même mais utilise le domaine abstrait
+    relationnel basé sur les polyèdres d'Apron pour la partie numérique
+
+    <item><verbatim|--ai-oct> : de même mais utilise les octogones
   </itemize>
 
   <paragraph|Options de l'analyse>
@@ -1534,10 +1599,17 @@
     <item><verbatim|--ai-vvci> : affiche encore plus de détails
 
     <item><verbatim|--ai-wd \<less\>n\<gtr\>> : définit un délai pour les
-    opérations de widening (par défaut 5)
+    opérations de widening (par défaut 5). Ce délai est utilisé à deux
+    endroits différents de l'analyse : pour le point fixe local de chaque
+    itération chaotique, et pour le point fixe global des itérations.
 
     <item><verbatim|--disj \<less\>vars\<gtr\>> : variables à utiliser comme
-    variables de disjonction (par défaut : aucune)
+    variables de disjonction (par défaut : aucune). Donner comme argument
+    <verbatim|all> permet d'utiliser toutes les variables énumérées pour les
+    disjonctions. Donner comme argument <strong|<verbatim|last>> permet
+    d'utilsier toutes les variables énumérées qui sont utilisées dans une
+    mémoire. On peut aussi utiliser la syntaxe <verbatim|last+v1,v2,v3> pour
+    rajouter des variables aux variables mémoire.
 
     <item><verbatim|--no-time \<less\>scopes\<gtr\>> : donne un certain
     nombre de scopes pour lesquels ne pas introduire de variable
@@ -1568,8 +1640,10 @@
     utilisant le domaine à base d'EDD et en utilisant les intervalles comme
     domaine de valeurs numériques
 
-    <item><verbatim|--ai-rel-edd> : de même mais utilise le domaine abstrait
-    relationnel basé sur Apron (polyèdres) pour la partie numérique
+    <item><verbatim|--ai-poly-edd> : de même mais utilise le domaine abstrait
+    relationnel basé sur les polyèdres d'Apron pour la partie numérique
+
+    <item><verbatim|--ai-oct-edd> : de même mais utilise les octogones
   </itemize>
 
   <paragraph|Options de l'analyse>
@@ -1590,10 +1664,7 @@
 
   <subsubsection|Analyse par partitionnement dynamique>
 
-  Une troisième forme d'analyse, basée sur un partitionnement dynamique de
-  <math|S<rsup|#>> a été tentée. Celle-ci n'a pas donné de très bons
-  résultats, mais nous indiquons néanmoins son existence ici.
-  L'implémentation existe dans <verbatim|abstract/abs_interp_dynpart.ml>.
+  Cette analyse est implémentée dans <verbatim|abstract/abs_interp_dynpart.ml>.
 
   <paragraph|Modes d'analyse>
 
@@ -1606,7 +1677,7 @@
     utilise des graphes de décision pour représenter les conditions sur les
     énumérées et les intervalles pour la partie numérique
 
-    <item><verbatim|--ai-s-rel-dp>
+    <item><verbatim|--ai-s-rel-dp> : utilise les polyèdres d'Apron
 
     <item><verbatim|--ai-edd-rel-dp>
   </itemize>
@@ -1670,7 +1741,7 @@
     ...) que l'on exécuterait comme pré-processing sur le programme.
   </itemize>
 
-  <section|Références>
+  <section*|Références>
 
   <\itemize>
     <item><name|N.Halbwachs>, <em|About synchronous programming and abstract
@@ -1723,26 +1794,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|6|16>>
-    <associate|auto-33|<tuple|7|?>>
-    <associate|auto-34|<tuple|7.1|?>>
-    <associate|auto-35|<tuple|7.2|?>>
-    <associate|auto-36|<tuple|7.3|?>>
-    <associate|auto-37|<tuple|7.3.1|?>>
-    <associate|auto-38|<tuple|7.3.1.1|?>>
-    <associate|auto-39|<tuple|7.3.1.2|?>>
+    <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-4|<tuple|2.2|2>>
-    <associate|auto-40|<tuple|7.3.2|?>>
-    <associate|auto-41|<tuple|7.3.2.1|?>>
-    <associate|auto-42|<tuple|7.3.2.2|?>>
-    <associate|auto-43|<tuple|7.3.3|?>>
-    <associate|auto-44|<tuple|7.3.3.1|?>>
-    <associate|auto-45|<tuple|7.3.3.2|?>>
-    <associate|auto-46|<tuple|8|?>>
-    <associate|auto-47|<tuple|8.1|?>>
-    <associate|auto-48|<tuple|8.2|?>>
-    <associate|auto-49|<tuple|9|?>>
+    <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-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-6|<tuple|2.3.1|3>>
     <associate|auto-7|<tuple|2.3.2|3>>
     <associate|auto-8|<tuple|2.3.3|3>>
@@ -1876,61 +1950,77 @@
       <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>Implémentation>
-      <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <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>|6.1<space|2spc>Parsing et affichage de
+      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|7<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>
+
+      <with|par-left|<quote|1.5fn>|7.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-33>>
+      <no-break><pageref|auto-34>>
 
-      <with|par-left|<quote|1.5fn>|6.2<space|2spc>Interprète SCADE
+      <with|par-left|<quote|1.5fn>|7.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-34>>
+      <no-break><pageref|auto-35>>
 
-      <with|par-left|<quote|1.5fn>|6.3<space|2spc>Analyse statique par
+      <with|par-left|<quote|1.5fn>|7.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-35>>
+      <no-break><pageref|auto-36>>
 
-      <with|par-left|<quote|3fn>|6.3.1<space|2spc>Domaine à disjonctions
+      <with|par-left|<quote|3fn>|7.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-36>>
+      <no-break><pageref|auto-37>>
 
       <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-37><vspace|0.15fn>>
+      <no-break><pageref|auto-38><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-38><vspace|0.15fn>>
+      <no-break><pageref|auto-39><vspace|0.15fn>>
 
-      <with|par-left|<quote|3fn>|6.3.2<space|2spc>Domaine à disjonction par
+      <with|par-left|<quote|3fn>|7.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-39>>
+      <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-40><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-41><vspace|0.15fn>>
+      <no-break><pageref|auto-42><vspace|0.15fn>>
 
-      <with|par-left|<quote|3fn>|6.3.3<space|2spc>Analyse par partitionnement
+      <with|par-left|<quote|3fn>|7.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-42>>
+      <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-43><vspace|0.15fn>>
+      <no-break><pageref|auto-44><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-44><vspace|0.15fn>>
+      <no-break><pageref|auto-45><vspace|0.15fn>>
+
+      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|8<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>
+
+      <with|par-left|<quote|1.5fn>|8.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>>
+
+      <with|par-left|<quote|1.5fn>|8.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>>
 
-      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|Bibliographie>
+      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|9<space|2spc>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-45><vspace|0.5fn>
+      <no-break><pageref|auto-49><vspace|0.5fn>
     </associate>
   </collection>
 </auxiliary>
\ No newline at end of file
diff --git a/main.ml b/main.ml
index 08ec36a..c283328 100644
--- a/main.ml
+++ b/main.ml
@@ -13,24 +13,26 @@ open Abs_interp_dynpart
 
 module Interpret = Interpret.I
 
-module ItvND = Nonrelational.ND(Intervals_domain.VD)
+module ItvND = Apron_domain.ND_Box   (* Nonrelational.ND(Intervals_domain.VD) *)
+module PolyND = Apron_domain.ND_Poly
+module OctND = Apron_domain.ND_Oct
 
 module AI_Itv = Abs_interp.I(Enum_domain.MultiValuation)(ItvND)
-module AI_Poly = Abs_interp.I(Enum_domain.MultiValuation)(Apron_domain.ND_Poly)
-module AI_Oct = Abs_interp.I(Enum_domain.MultiValuation)(Apron_domain.ND_Oct)
+module AI_Poly = Abs_interp.I(Enum_domain.MultiValuation)(PolyND)
+module AI_Oct = Abs_interp.I(Enum_domain.MultiValuation)(OctND)
 
 module AI_Itv_EDD = Abs_interp_edd.I(ItvND)
-module AI_Poly_EDD = Abs_interp_edd.I(Apron_domain.ND_Poly)
-module AI_Oct_EDD = Abs_interp_edd.I(Apron_domain.ND_Oct)
+module AI_Poly_EDD = Abs_interp_edd.I(PolyND)
+module AI_Oct_EDD = Abs_interp_edd.I(OctND)
 
 module AI_S_Itv_DP = Abs_interp_dynpart.I
       (Enum_domain.MultiValuation)(ItvND)
 module AI_S_Rel_DP = Abs_interp_dynpart.I
-      (Enum_domain.MultiValuation)(Apron_domain.ND_Poly)
+      (Enum_domain.MultiValuation)(PolyND)
 module AI_EDD_Itv_DP = Abs_interp_dynpart.I
       (Enum_domain_edd.EDD)(ItvND)
 module AI_EDD_Rel_DP = Abs_interp_dynpart.I
-      (Enum_domain_edd.EDD)(Apron_domain.ND_Poly)
+      (Enum_domain_edd.EDD)(PolyND)
 
 (* command line options *)
 let times = ref false
diff --git a/tests/source/updown.scade b/tests/source/updown.scade
index c736dd8..4bfa5e3 100644
--- a/tests/source/updown.scade
+++ b/tests/source/updown.scade
@@ -1,4 +1,4 @@
-const bound: int = 7;
+const bound: int = 10;
 
 node updown() returns(probe x: int)
 var last_x: int;
diff --git a/tests/source/updown2.scade b/tests/source/updown2.scade
index 72d5bed..29069e5 100644
--- a/tests/source/updown2.scade
+++ b/tests/source/updown2.scade
@@ -1,4 +1,4 @@
-const bound: int = 7;
+const bound: int = 10;
 
 node updown2() returns(probe x, probe y, probe z: int)
 var last_x, last_y: int;