2021-03-03 03:18 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000549Frama-CKernel > ACSL implementationpublic2014-02-12 16:55
Reporterpatrick 
Assigned Tovirgile 
PriorityhighSeveritymajorReproducibilityhave not tried
StatusclosedResolutionfixed 
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
+Relationships

-Notes

~0001029

patrick (developer)

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)

Last edited: 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)

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)

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

-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-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
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
2013-12-19 01:12 Source_changeset_attached => framac master b5e35dc5
2014-02-12 16:55 Source_changeset_attached => framac stable/neon b5e35dc5
+Issue History