Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001436Frama-CPlug-in > pdgpublic2013-05-30 16:492014-03-13 15:57
Reportersignoles 
Assigned Toyakobowski 
PriorityurgentSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Fluorine-20130501 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001436: Stack overflow when computing a PDG
Description==== test.c ==== void __VERIFIER_assert(int cond) { if (!(cond)) { ERROR: goto ERROR; } return; } #define a (2) int main(unsigned int loop1, unsigned int m1) { int sn=0; unsigned int x=0; while(1){ sn = sn + a; x++; __VERIFIER_assert(sn==x*a || sn == 0); } } ========== $ frama-c -pdg test.c [pdg] computing for function __VERIFIER_assert [pdg] done for function __VERIFIER_assert [pdg] computing for function main [kernel] Current source was: sum03_safe.c:5 The full backtrace is: Called from file "set.ml", line 216, characters 18-33 Called from file "list.ml", line 195, characters 17-20 Called from file "src/kernel/stmts_graph.ml", line 418, characters 6-65 Called from file "src/pdg/ctrlDpds.ml", line 217, characters 35-59 Called from file "list.ml", line 86, characters 24-34 Called from file "src/pdg/ctrlDpds.ml", line 237, characters 29-39 Called from file "src/pdg/ctrlDpds.ml", line 257, characters 22-31 Called from file "src/pdg/ctrlDpds.ml", line 261, characters 11-21 Called from file "src/pdg/ctrlDpds.ml", line 261, characters 11-21 Called from file "src/pdg/ctrlDpds.ml", line 261, characters 11-21
Additional InformationBug coming from Checkofv...
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2013-05-30 16:49 signoles New Issue
2013-05-30 16:49 signoles Status new => assigned
2013-05-30 16:49 signoles Assigned To => yakobowski
2013-08-26 13:55 svn Checkin
2013-08-26 13:56 yakobowski Status assigned => resolved
2013-08-26 13:56 yakobowski Resolution open => fixed
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker