diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | abstract/apron_domain.ml | 184 | ||||
| -rw-r--r-- | doc/readme.pdf | bin | 236320 -> 263955 bytes | |||
| -rw-r--r-- | doc/readme.tm | 224 | ||||
| -rw-r--r-- | main.ml | 16 | ||||
| -rw-r--r-- | tests/source/updown.scade | 2 | ||||
| -rw-r--r-- | tests/source/updown2.scade | 2 |
7 files changed, 280 insertions, 150 deletions
@@ -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 Binary files differindex 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 @@ -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; |