0000791: Cash in value analysis of sliced project - Frama-C Bug Tracking System

Frama-C Bug Tracking System

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

[ Issue History ] [ Print ]

ID

Project

Category

View Status

Date Submitted

Last Update

0000791

Frama-C

Plug-in > value analysis

public

2011-04-13 08:55

2014-02-12 16:54

Reporter

patrick

Assigned To

pascal

Priority

normal

Severity

crash

Reproducibility

have not tried

Status

closed

Resolution

fixed

Platform

OS

OS Version

Product Version

Frama-C GIT, precise the release id

Target Version

Fixed in Version

Frama-C Nitrogen-20111001

Summary

0000791: Cash in value analysis of sliced project

Description

Unexpected error (File "src/kernel/cilE.ml", line 268, characters 68-74: Assertion failed).

Additional Information

Revision: 12829

Command:
frama-c bug.c -slice-return send -then-on 'Slicing export' -val

file bug.c
/*@ assigns *p \from \empty;
    assigns \result ; */
int scanf (char const *, int * p);
/*@ assigns \nothing ; */
int send (int x) {
  return x;
}
void main(void) {
  int input;
  scanf("%d",&input);
  send (input);
}

Tags

No tags attached.

Relationships

related to

closed

r12793: slicing generates uncompilable code (sliced function called with too few arguments) (csmith)

Notes
(0001785) yakobowski (manager) 2011-04-14 10:31	Building parts of a new AST inside a copy visitor is really tricky to get right. The above patch ensures that varinfos will not clash between the different projects, but this is not the Right Thing To Do. No better solution for now.

Issue History
Date Modified	Username	Field	Change
2011-04-13 08:55	patrick	New Issue
2011-04-13 08:55	patrick	Status	new => assigned
2011-04-13 08:55	patrick	Assigned To	=> pascal
2011-04-13 09:25	patrick	Description Updated
2011-04-13 09:25	patrick	Additional Information Updated
2011-04-14 10:28	svn	Checkin
2011-04-14 10:31	yakobowski	Note Added: 0001785
2011-04-14 10:31	yakobowski	Status	assigned => resolved
2011-04-14 10:31	yakobowski	Fixed in Version	=> Frama-C GIT, precise the release id
2011-04-14 10:31	yakobowski	Resolution	open => fixed
2011-04-14 13:54	svn	Checkin
2011-04-14 14:33	yakobowski	Relationship added	related to 0000780
2011-10-10 14:13	signoles	Fixed in Version	Frama-C GIT, precise the release id => Frama-C Nitrogen-20111001
2011-10-10 14:14	signoles	Status	resolved => closed

Copyright © 2000 - 2017 MantisBT Team