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