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 |
|
![]() |
|||
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 |