Computation of regions for axioms in axiomatics

ID0000834: This issue was created automatically from Mantis Issue 834. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0000834	Frama-C	Plug-in > jessie	public	2011-05-24	2011-05-24

Reporter	proux	Assigned To	cmarche	Resolution	open
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Carbon-20110201	Target Version	-	Fixed in Version	-

Description :

When using Jessie (from Why-2.29) on following code, it answers "Unable to complete region analysis, aborting. Consider using #pragma SeparationPolicy(none)":

/*@ axiomatic a { @ logic integer f(integer x); @ logic integer g{L}(int *x); @ axiom g0: \forall int x; g(x) == 0; @ } @/

Indeed, in jc_separation.ml, when computing regions for any logic functions it just after trigers computation of regions for all axioms in the same axiomatic hence trigerring typing of axiom g0 just after logic function f while function g appearing in it is still "unknown".

The function compute_regions in jc_main.ml first computes regions for all logic functions the for axioms and a comment says "Preserve order between following calls". It indeed seems that preserving this order fix the problem with following patch except if I happen to miss something:

diff -ru why-2.29/jc/jc_separation.ml why-2.29.patched/jc/jc_separation.ml --- why-2.29/jc/jc_separation.ml 2011-03-02 08:27:41.000000000 +0000 +++ why-2.29.patched/jc/jc_separation.ml 2011-05-24 12:01:11.000000000 +0000 @@ -275,16 +275,6 @@ (* fold_location ) ( (fold_unit (term rresult)) (fold_unit ignore) (fold_unit ignore) () loc *)

-let axiomatic_decl d =

• match d with
• | Jc_typing.ABaxiom(,,_,a) -> assertion dummy_region a

-let axiomatic a =

• try
• let l = Hashtbl.find Jc_typing.axiomatics_table a in
• List.iter axiomatic_decl l.Jc_typing.axiomatics_decls
• with Not_found -> assert false

let logic_function f = let (f, ta) = Hashtbl.find Jc_typing.logic_functions_table f.jc_logic_info_tag @@ -301,8 +291,7 @@ | JCReads r -> List.iter (location rresult) r | JCInductive l -> List.iter (fun (,,a) -> assertion rresult a) l

• end;
• Option_misc.iter axiomatic f.jc_logic_info_axiomatic

• end

let generalize_logic_function f = let param_regions =