Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000761Frama-CKernel > ACSL implementationpublic2011-03-22 10:592014-02-12 16:59
Reporterpatrick 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000761: typing rule of \old(tab) or tab[index] construct
Description\old(t)[0] is interpreted as \old((int*)t)[0] when t is a C variable declared as follow:
int t[10];

That raises a problem when using such constructs combined with \let constructs.
It is mainly accepted that
  \old(\let x = t ; x)
is equivalent to
  \let x = \old(t) ; x
That propagation rule implies the type of t should be the same than the type of \old(t).

That isn't the case with the current ACSL implementation:
  \old(\let x = t ; x) has type int[10] and
  \let x = \old(t) ; x has type int*
The issue is more significant on theses expressions
  \old(\let x = t ; x)[0] and
  (\let x = \old(t) ; x)[0].

So, is the problem with a typing rule or with the propagation rule.
  
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0001627)
patrick (developer)
2011-03-22 11:49

There is an example

tab.c:
extern int tab [] ;
/*@ ensures \old(tab)[0] > 0 ;
    ensures \old(\let x = tab ; x)[0] > 0 ;
    ensures (\let x = \old(tab) ; x)[0] > 0;
*/
int main(void);

>frama-c -print tab.c
/* Generated by Frama-C */
extern int tab[] ;
/*@ ensures \old((int *)tab)[0] > 0;
    ensures (\let tmp = \old(\let x = tab; x); tmp[0]) > 0;
    ensures (\let tmp = \let x = \old(tab); x; tmp[0]) > 0;
  
*/
extern int main(void) ;
(0001630)
patrick (developer)
2011-03-24 16:27
edited on: 2011-03-24 16:27

There is another problem with the typing rule of \old(x)[i] :

tab_bis.c:
struct st { int t[10]; } S;
int i,j ;
//@ ensures S.t[i] == s.t[j] ;
void main (struct st s) ;

>frama-c -print tab_bis.c
...
/*@ ensures S.t[i] == \old(s.t[j]); */
extern void main(struct st s ) ;


It should be:
/*@ ensures S.t[i] == \old(s.t[\at(j,Here)]); */
extern void main(struct st s ) ;

(0004803)

2014-02-12 16:59

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2011-03-22 10:59 patrick New Issue
2011-03-22 10:59 patrick Status new => assigned
2011-03-22 10:59 patrick Assigned To => virgile
2011-03-22 11:49 patrick Note Added: 0001627
2011-03-23 10:34 svn Checkin
2011-03-23 10:53 virgile Status assigned => acknowledged
2011-03-24 16:20 patrick Summary typing rule of \at and \old construct => typing rule of \old(tab) or tab[index] construct
2011-03-24 16:20 patrick Description Updated
2011-03-24 16:27 patrick Note Added: 0001630
2011-03-24 16:27 patrick Note Edited: 0001630
2011-03-24 17:12 svn Checkin
2011-04-20 17:19 svn Checkin
2011-04-20 17:19 svn Status acknowledged => resolved
2011-04-20 17:19 svn Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
2014-02-12 16:59 Note Added: 0004803
2014-02-12 16:59 Status closed => resolved


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker