Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
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.
Attached Files? file icon justcopy.ml [^] (227 bytes) 2012-10-16 12:35 [Show Content]

- Relationships

-  Notes
(0004614)

2014-02-12 16:58

Fix committed to stable/neon branch.

- 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 Checkin
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
2014-02-12 16:58 Note Added: 0004614
2014-02-12 16:58 Status closed => resolved


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker