0000549: Typing problem into the logic about C variable of an array type. - Frama-C Bug Tracking System

2021-03-03 03:18 CET

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

ID

Project

Category

View Status

Date Submitted

Last Update

0000549

Frama-C

Kernel > ACSL implementation

public

2010-07-28 15:14

2014-02-12 16:55

Reporter

patrick

Assigned To

virgile

Priority

high

Severity

major

Reproducibility

have not tried

Status

closed

Resolution

fixed

Product Version

Target Version

Fixed in Version

Frama-C Carbon-20101201-beta1

Summary

0000549: Typing problem into the logic about C variable of an array type.

Description

Some 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 Information

int 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
     }
}

Tags

No tags attached.

Attached Files

Relationships

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 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) 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.

Notes

Date Modified	Username	Field	Change
Issue History
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