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
0000549Frama-CKernel > ACSL implementationpublic2010-07-28 15:142014-02-12 16:55
Reporterpatrick 
Assigned Tovirgile 
PriorityhighSeveritymajorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in VersionFrama-C Carbon-20101201-beta1 
Summary0000549: Typing problem into the logic about C variable of an array type.
DescriptionSome times, the inferred type is T* instead of T[]. In the given exemple, the current version of Frama-C (Revision: 9458) both arguments of == operator used into the assert clause have type int* instead of int[10]
Additional Informationint t1[10], t2[10] ; int main () { int i ; for (i=0 ; i < 10 ; i++) t1[i] = 0 ; t2[i] = 0 ; } if (t1 == t2) { /* C tests the address of the first elements, * so the then-branch is dead. */ //@ assert false; } else { /* ACSL tests the contents of the arrays, * here they are the same. */ //@ assert (t1==t2) ; // even with the previous C } }
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0001029)
patrick (developer)
2010-08-02 13:55

 About the same topic, the command frama-c -print ex.c gives : [kernel] user error: Error during annotations analysis: return type of logic function t5 is int * but int * was expected file ex.c: typedef int T10[10] ; T10 t ; //@logic int * t5 = t+1; The logic function should be accepted!
(0001086)
patrick (developer)
2010-08-24 11:24
edited on: 2010-08-24 11:26

 About the same topic, the command frama-c -print ex.c gives: extern int tab[] ; /*@ logic int * a1= tab+0; */ /*@ logic int * a2= tab; */ /*@ logic int * a3= tab; */ /*@ logic int * a4= tab; */ /*@ logic int * b1= \let x = tab+0; x; */ /*@ logic int * b2= \let x = tab; x; */ /*@ logic int * b3= \let x = tab; x; */ file ex.c: //@ logic int * a1 = tab + 0; //@ logic int * a2 = &tab[0]; //@ logic int * a3 = &*tab ; //@ logic int * a4 = tab ; //@ logic int * b1 = \let x = tab + 0; x ; //@ logic int * b2 = \let x = &tab[0]; x ; //@ logic int * b3 = \let x = &*tab ; x ; // logic int * b4 = \let x = tab ; x ; Notice logical function b4 is not accepted but it is the way how b2 and b3 are pretty printed ! I don't know if b4 should be accepted or else if there is a pretty printer problem.
(0001089)
virgile (developer)
2010-08-24 13:28

 b4 should not be accepted (neither should a4 by the way). The fact that b2 and b3 are normalized as such is a bug, but unlikely to reside in the pretty-printer. More probably in the normalization.
(0001091)
patrick (developer)
2010-08-24 15:52

 since a4 should be rejected, the fact that a2 and a3 are normalized as such is also a bug.

- Issue History
Date Modified Username Field Change
2010-07-28 15:14 patrick New Issue
2010-07-28 15:14 patrick Status new => assigned
2010-07-28 15:14 patrick Assigned To => virgile
2010-07-28 15:19 patrick Priority normal => high
2010-07-28 15:19 patrick Severity minor => major
2010-07-28 15:19 patrick Description Updated
2010-07-30 11:28 patrick Note Added: 0001022
2010-08-02 10:46 patrick Note Deleted: 0001022
2010-08-02 13:55 patrick Note Added: 0001029
2010-08-24 11:24 patrick Note Added: 0001086
2010-08-24 11:26 patrick Note Edited: 0001086
2010-08-24 13:28 virgile Note Added: 0001089
2010-08-24 15:52 patrick Note Added: 0001091
2010-08-27 11:39 svn Checkin
2010-08-27 11:39 svn Status assigned => resolved
2010-08-27 11:39 svn Resolution open => fixed
2010-12-10 15:45 signoles Fixed in Version => Frama-C Carbon-20101201-beta1
2010-12-17 19:36 signoles Status resolved => closed

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker