Frama-C Bug Tracking System - Frama-C
View Issue Details
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
<skip value's trace>
[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
<skip the rest of the backrace>
Additional InformationBug coming from Checkofv...
TagsNo tags attached.
Relationships
Attached Files

There are no notes attached to this issue.

Issue History
Date ModifiedUsernameFieldChange
2013-05-30 16:49signolesNew Issue
2013-05-30 16:49signolesStatusnew => assigned
2013-05-30 16:49signolesAssigned To => yakobowski
2013-08-26 13:55svn
2013-08-26 13:56yakobowskiStatusassigned => resolved
2013-08-26 13:56yakobowskiResolutionopen => fixed
2013-12-19 01:11yakobowskiSource_changeset_attached => framac master 68d6f955
2014-02-12 16:53yakobowskiSource_changeset_attached => framac stable/neon 68d6f955
2014-03-13 15:56signolesFixed in Version => Frama-C Neon-20140301
2014-03-13 15:57signolesStatusresolved => closed