Frama-C Bug Tracking System - Frama-C
View Issue Details
0000761Frama-CKernel > ACSL implementationpublic2011-03-22 10:592014-02-12 16:59
patrick 
virgile 
normalminorhave not tried
closedfixed 
Frama-C Carbon-20110201 
Frama-C Nitrogen-20111001 
0000761: typing rule of \old(tab) or tab[index] construct
\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.
No tags attached.
Issue History
2011-03-22 10:59patrickNew Issue
2011-03-22 10:59patrickStatusnew => assigned
2011-03-22 10:59patrickAssigned To => virgile
2011-03-22 11:49patrickNote Added: 0001627
2011-03-23 10:34svnCheckin
2011-03-23 10:53virgileStatusassigned => acknowledged
2011-03-24 16:20patrickSummarytyping rule of \at and \old construct => typing rule of \old(tab) or tab[index] construct
2011-03-24 16:20patrickDescription Updated
2011-03-24 16:27patrickNote Added: 0001630
2011-03-24 16:27patrickNote Edited: 0001630
2011-03-24 17:12svnCheckin
2011-04-20 17:19svnCheckin
2011-04-20 17:19svnStatusacknowledged => resolved
2011-04-20 17:19svnResolutionopen => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed
2014-02-12 16:59Note Added: 0004803
2014-02-12 16:59Statusclosed => resolved

Notes
(0001627)
patrick   
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   
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.