Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Related Changesets ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000791Frama-CPlug-in > Evapublic2011-04-13 08:552014-02-12 16:54
Reporterpatrick 
Assigned Topascal 
PrioritynormalSeveritycrashReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000791: Cash in value analysis of sliced project
DescriptionUnexpected error (File "src/kernel/cilE.ml", line 268, characters 68-74: Assertion failed).

Additional InformationRevision: 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);
}
TagsNo tags attached.
Attached Files

- Relationships
related to 0000780closedvirgile 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
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker