| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0001436 | Frama-C | Plug-in > pdg | public | 2013-05-30 16:49 | 2014-03-13 15:57 | ||||
| Reporter | signoles | ||||||||
| Assigned To | yakobowski | ||||||||
| Priority | urgent | Severity | crash | Reproducibility | always | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | Frama-C Fluorine-20130501 | ||||||||
| Target Version | Fixed in Version | Frama-C Neon-20140301 | |||||||
| Summary | 0001436: 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 Information | Bug coming from Checkofv... | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
| There are no notes attached to this issue. |
| Notes |
| 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 | ||
| 2013-08-26 13:56 | yakobowski | Status | assigned => resolved |
| 2013-08-26 13:56 | yakobowski | Resolution | open => fixed |
| 2013-12-19 01:11 | yakobowski | Source_changeset_attached | => framac master 68d6f955 |
| 2014-02-12 16:53 | yakobowski | Source_changeset_attached | => framac stable/neon 68d6f955 |
| 2014-03-13 15:56 | signoles | Fixed in Version | => Frama-C Neon-20140301 |
| 2014-03-13 15:57 | signoles | Status | resolved => closed |
| Issue History |