2021-03-03 03:20 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001284Frama-CKernelpublic2014-02-12 16:58
Reportersignoles 
Assigned Tovirgile 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Oxygen-20120901 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0001284: Copy visitor builds an inconsistent AST on clause 'frees'
DescriptionRun the uploaded script on the following file:

=== frees.i ===
/*@ frees x; */
void f(int *x);
===============

$ frama-c -check -load-script frees.ml frees.i
frees.i:1:[kernel] failure: [AST Integrity Check] AST of frees
                  logic variable x(741) is not shared between definition and use
<skip backtrace>
TagsNo tags attached.
Attached Files
  • ? file icon frees.ml (127 bytes) 2012-10-19 10:47 -
    let main () =
      ignore
        (File.create_project_from_visitor "frees" (new Visitor.frama_c_copy))
    
    let () = Db.Main.extend main
    
    ? file icon frees.ml (127 bytes) 2012-10-19 10:47 +

-Relationships
+Relationships

-Notes

~0004613

Fix committed to stable/neon branch.
+Notes

-Issue History
Date Modified Username Field Change
2012-10-19 10:47 signoles New Issue
2012-10-19 10:47 signoles Status new => assigned
2012-10-19 10:47 signoles Assigned To => virgile
2012-10-19 10:47 signoles File Added: frees.ml
2012-10-19 13:00 virgile Status assigned => acknowledged
2012-10-22 12:27 svn
2012-10-22 12:27 svn Status acknowledged => resolved
2012-10-22 12:27 svn Resolution open => fixed
2013-04-19 11:05 signoles Fixed in Version => Frama-C Fluorine
2013-04-19 11:05 signoles Status resolved => closed
2013-12-19 01:11 Source_changeset_attached => framac master a9dee319
2014-02-12 16:53 Source_changeset_attached => framac stable/neon a9dee319
2014-02-12 16:58 Note Added: 0004613
2014-02-12 16:58 Status closed => resolved
+Issue History