Frama-C Bug Tracking System - Frama-C
View Issue Details
IDProjectCategoryView StatusDate SubmittedLast Update
0001282Frama-CKernelpublic2012-10-16 12:352014-02-12 16:58
Reportersignoles 
Assigned Tovirgile 
PriorityhighSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
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.
Relationships
Attached Files? justcopy.ml (227) 2012-10-16 12:35
https://bts.frama-c.com/file_download.php?file_id=428&type=bug

Notes
(0004614)
   
2014-02-12 16:58   
Fix committed to stable/neon branch.

Issue History
Date ModifiedUsernameFieldChange
2012-10-16 12:35signolesNew Issue
2012-10-16 12:35signolesStatusnew => assigned
2012-10-16 12:35signolesAssigned To => virgile
2012-10-16 12:35signolesFile Added: justcopy.ml
2012-10-18 11:16svn
2012-10-18 11:16svnStatusassigned => resolved
2012-10-18 11:16svnResolutionopen => fixed
2013-04-19 11:05signolesFixed in Version => Frama-C Fluorine
2013-04-19 11:05signolesStatusresolved => closed
2013-12-19 01:11Source_changeset_attached => framac master 820dbb03
2014-02-12 16:53Source_changeset_attached => framac stable/neon 820dbb03
2014-02-12 16:58Note Added: 0004614
2014-02-12 16:58Statusclosed => resolved