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 - 2019 MantisBT Team
Powered by Mantis Bugtracker