diff options
| -rw-r--r-- | abstract/abs_interp_dynpart.ml | 77 | ||||
| -rw-r--r-- | doc/readme.pdf | bin | 263955 -> 263736 bytes | |||
| -rw-r--r-- | doc/readme.tm | 119 |
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 Binary files differindex 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 |