View Issue Details [ Jump to Notes ] [ Related Changesets ] | [ Issue History ] [ Print ] |
ID | Project | Category | View Status | Date Submitted | Last Update |
0001044 | Frama-C | Plug-in > Eva | public | 2011-12-10 23:39 | 2014-03-13 15:57 |
|
Reporter | pascal | |
Assigned To | yakobowski | |
Priority | normal | Severity | feature | Reproducibility | always |
Status | closed | Resolution | fixed | |
Platform | | OS | | OS Version | |
Product Version | | |
Target Version | | Fixed in Version | Frama-C Neon-20140301 | |
|
Summary | 0001044: Smarter access to array of struct of array |
Description | Smarter access to array of struct of array |
Tags | No tags attached. |
|
Attached Files | test1.c [^] (455 bytes) 2011-12-11 00:06 [Show Content] [Hide Content]
typedef struct {
int i;
short s;
short pad;
int* p;} T_STR1;
#define CTE1 3
#define CTE2 4
typedef struct {
int i;
short s;
short pad;
T_STR1 ts[CTE2];
} T_STR2;
T_STR2 tab[CTE1];
/*@
@ requires 0<=index1<CTE1;
@ requires 0<=index2<CTE2;
@*/
int f1(int index1, int index2, short ref)
{
short local;
if (ref == tab[index1].ts[index2].s)
{
local = tab[index1].ts[index2].s;
return 0;
}
return -1;
}
|
|