2021-02-24 19:06 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001282Frama-CKernelpublic2012-10-16 12:352014-02-12 16:58
Reportersignoles 
Assigned Tovirgile 
PriorityhighSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Oxygen-20120901 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0001282: [Visitor] Cil.JustCopy does not work on functions with contracts
DescriptionConsider the attached script justcopy.ml which just implements a copy visitor with an invokation to Cil.JustCopy for vglob_aux.

$ touch justcopy.i
$ frama-c -load-script justcopy.ml justcopy.i -check
/usr/local/share/frama-c/libc/__fc_builtin_for_normalization.i:30:[kernel] failure: [AST Integrity Check] AST of justcopy
                  logic variable dest(365) is not declared
<skip the backtrace>
TagsNo tags attached.
Attached Files
  • ? file icon justcopy.ml (227 bytes) 2012-10-16 12:35 - 
    let main () =
  Ast.compute ();
  let o prj = object
    inherit Visitor.frama_c_copy prj
    method vglob_aux _g = Cil.JustCopy
  end
  in
  ignore (File.create_project_from_visitor "justcopy" o)

let () = Db.Main.extend main
    ? file icon justcopy.ml (227 bytes) 2012-10-16 12:35 +

-Relationships
+Relationships

-Notes

~0004614

2014-02-12 16:58

 Fix committed to stable/neon branch.
+Notes

-Issue History
Date Modified Username Field Change
2012-10-16 12:35 signoles New Issue
2012-10-16 12:35 signoles Status new => assigned
2012-10-16 12:35 signoles Assigned To => virgile
2012-10-16 12:35 signoles File Added: justcopy.ml
2012-10-18 11:16 svn
2012-10-18 11:16 svn Status assigned => resolved
2012-10-18 11:16 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 820dbb03
2014-02-12 16:53 Source_changeset_attached => framac stable/neon 820dbb03
2014-02-12 16:58 Note Added: 0004614
2014-02-12 16:58 Status closed => resolved
+Issue History