Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001762Frama-CPlug-in > E-ACSLpublic2014-04-25 10:402018-10-04 10:12
Reportersignoles 
Assigned Tofmaurica 
PrioritynormalSeverityminorReproducibilityalways
StatusresolvedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFrama-C 18 ArgonFixed in Version 
Summary0001762: Generate out-of-scope variable when using quantified variable in a \old
Description===== a.i =====
/*@ ensures \forall integer i; 0 <= i < 10 ==> \old(t[i]) == 0; */
void f(int *t) { }

int main(void) {
  int t[10];
  int i;
  for(i = 0; i < 10; i++) t[i] = 0;
  f(t);
  return 0;
}
================

$ frama-c a.i -e-acsl -then-on e-acsl -print -ocode res.i
$ ./gcc.sh res.i
compiling res.i
res.i: In function ā€˜__e_acsl_fā€™:
res.i:84:53: error: ā€˜__e_acsl_iā€™ undeclared (first use in this function)
res.i:84:53: note: each undeclared identifier is reported only once for each fun
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2014-04-25 10:40 signoles New Issue
2014-04-25 10:40 signoles Status new => assigned
2014-04-25 10:40 signoles Assigned To => signoles
2014-04-25 10:40 signoles Status assigned => confirmed
2014-04-25 10:48 signoles Relationship added duplicate of 0001354
2014-04-25 10:48 signoles Status confirmed => closed
2014-04-25 10:48 signoles Resolution open => duplicate
2014-04-25 10:50 signoles Status closed => confirmed
2014-04-25 10:51 signoles Summary Generate out-of-scope variable when mixing quantification, \old and potential RTE => Generate out-of-scope variable when using quantified variable in a \old
2018-02-22 10:37 signoles Assigned To signoles => fmaurica
2018-02-22 10:37 signoles Status confirmed => assigned
2018-09-06 16:03 signoles Target Version => Frama-C 18 Argon
2018-10-04 10:11 signoles Relationship deleted 0001354
2018-10-04 10:12 signoles Status assigned => resolved
2018-10-04 10:12 signoles Resolution duplicate => fixed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker