| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0001445 | Frama-C | Plug-in > slicing | public | 2013-06-13 10:12 | 2014-03-13 15:57 | ||||
| Reporter | signoles | ||||||||
| Assigned To | patrick | ||||||||
| Priority | high | Severity | crash | Reproducibility | always | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | |||||||||
| Target Version | Frama-C Fluorine-20130501 | Fixed in Version | Frama-C Neon-20140301 | ||||||
| Summary | 0001445: Crash when selecting the calls to an unterminating functions | ||||||||
| Description | $ less bug.i int x = 0; int main() { while(1) x=0; return 0; } $ frama-c.byte -slice-calls main bug.i [slicing] slicing requests in progress... [value] Analyzing a complete application starting at main [value] Computing initial state [value] Initial state computed [value] Values of globals at initialization x ? {0} bug.i:4:[value] entering loop for the first time [value] Recording results for main [value] done for function main [slicing] making slicing project 'Slicing'... [slicing] interpreting slicing requests from the command line... [pdg] computing for function main bug.i:6:[pdg] warning: no final state. Probably unreachable... [pdg] done for function main [kernel] Current source was: bug.i:5 The full backtrace is: Raised at file "src/slicing/register.ml", line 150, characters 23-35 Called from file "src/slicing/slicingCmds.ml", line 200, characters 25-96 | ||||||||
| 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-06-13 10:12 | signoles | New Issue | |
| 2013-06-13 10:12 | signoles | Status | new => assigned |
| 2013-06-13 10:12 | signoles | Assigned To | => patrick |
| 2013-06-13 11:04 | svn | ||
| 2013-06-14 08:44 | svn | ||
| 2013-06-18 09:49 | signoles | Status | assigned => resolved |
| 2013-06-18 09:49 | signoles | Resolution | open => fixed |
| 2013-12-19 01:11 | patrick | Source_changeset_attached | => framac master a9686756 |
| 2013-12-19 01:11 | patrick | Source_changeset_attached | => framac master b64880cb |
| 2014-02-12 16:53 | patrick | Source_changeset_attached | => framac stable/neon a9686756 |
| 2014-02-12 16:53 | patrick | Source_changeset_attached | => framac stable/neon b64880cb |
| 2014-03-13 15:56 | signoles | Fixed in Version | => Frama-C Neon-20140301 |
| 2014-03-13 15:57 | signoles | Status | resolved => closed |
| Issue History |