Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000834Frama-CPlug-in > jessiepublic2011-05-24 15:202011-05-24 15:20
Reporterproux 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in Version 
Summary0000834: Computation of regions for axioms in axiomatics
DescriptionWhen 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 =
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2011-05-24 15:20 proux New Issue
2011-05-24 15:20 proux Status new => assigned
2011-05-24 15:20 proux Assigned To => cmarche


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker