Frama-C Bug Tracking System - Frama-C | |||||
View Issue Details | |||||
ID | Project | Category | View Status | Date Submitted | Last Update |
0001282 | Frama-C | Kernel | public | 2012-10-16 12:35 | 2014-02-12 16:58 |
Reporter | signoles | ||||
---|---|---|---|---|---|
Assigned To | virgile | ||||
Priority | high | Severity | crash | Reproducibility | always |
Status | closed | Resolution | fixed | ||
Platform | OS | OS Version | |||
Product Version | Frama-C Oxygen-20120901 | ||||
Target Version | Fixed in Version | Frama-C Fluorine-20130401 | |||
Summary | 0001282: [Visitor] Cil.JustCopy does not work on functions with contracts | ||||
Description | Consider 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> | ||||
Tags | No tags attached. | ||||
Relationships | |||||
Attached Files | ![]() https://bts.frama-c.com/file_download.php?file_id=428&type=bug |
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 |