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 |
|
![]() |
|
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! |
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. |
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. |
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. |
![]() |
|||
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 |