summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-07-24 10:18:30 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-07-24 10:18:30 +0200
commit6742003891028d566edf23dc7092c34f6d40255f (patch)
tree9768a5fadaf1668726bcc055197fc3ae944d05fe
parent2073dd00710add906cc94099cd4bfb7aa3a2f85e (diff)
downloadscade-analyzer-6742003891028d566edf23dc7092c34f6d40255f.tar.gz
scade-analyzer-6742003891028d566edf23dc7092c34f6d40255f.zip
Plug into Apron Box domain for intervals.
-rw-r--r--Makefile2
-rw-r--r--abstract/apron_domain.ml184
-rw-r--r--doc/readme.pdfbin236320 -> 263955 bytes
-rw-r--r--doc/readme.tm224
-rw-r--r--main.ml16
-rw-r--r--tests/source/updown.scade2
-rw-r--r--tests/source/updown2.scade2
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
Binary files differ
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;