0001445: Crash when selecting the calls to an unterminating functions

View Issue Details [ Jump to Notes ] [ Related Changesets ]

[ Issue History ] [ Print ]

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

Platform

OS Version

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

Notes
There are no notes attached to this issue.

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	Checkin
2013-06-14 08:44	svn	Checkin
2013-06-18 09:49	signoles	Status	assigned => resolved
2013-06-18 09:49	signoles	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