replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

fix for designated initializers 

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@1707 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
This commit is contained in:
kroening 2012-09-18 11:00:43 +00:00
parent 0ca1ab4dd8
commit ca4f7e5992
2 changed files with 13 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
regression/cbmc/Array_Initialization3/main.c
View File

@ -10,6 +10,10 @@ int array2[]={ [1]=10, [2]=20, [3]=30, [10]=100 };
extern int array3[8];
int array3[]={ 1, 2, 3, 4, 5, 6, 7, 8 };
int array4[2] = { [1] 42 };
int array5[2][2] = { { 42, 42 }, {[1] 42 } };
int array6[2][2] = { [1] {[1] 42 } };
int main(void)
{
assert(array1[0][1] ==2);

19
src/ansi-c/parser.y
View File

@ -1774,7 +1774,6 @@ initializer_opt:
initializer:
constant_expression /* was: assignment_expression */
| designated_initializer
| '{' initializer_list_opt '}'
{
$$=$1;
@ -1790,7 +1789,7 @@ initializer:
;
initializer_list:
initializer
designated_initializer
{
$$=$1;
exprt tmp;
@ -1798,7 +1797,7 @@ initializer_list:
stack($$).clear();
stack($$).move_to_operands(tmp);
}
| initializer_list ',' initializer
| initializer_list ',' designated_initializer
{
$$=$1;
mto($$, $3);
@ -1815,9 +1814,9 @@ initializer_list_opt:
}
;
/* GCC extension: designated initializer */
designated_initializer:
designated_initializer_designator '=' initializer
initializer
| designator '=' initializer
{
$$=$2;
stack($$).id(ID_designated_initializer);
@ -1825,7 +1824,7 @@ designated_initializer:
mto($$, $3);
}
/* the following two are obsolete GCC extensions */
| designated_initializer_designator constant_expression
| designator initializer
{
init($$, ID_designated_initializer);
stack($$).add(ID_designator).swap(stack($1));
@ -1845,7 +1844,7 @@ designated_initializer:
}
;
designated_initializer_designator:
designator:
'.' member_name
{
init($$);
@ -1868,14 +1867,14 @@ designated_initializer_designator:
mto($1, $2);
mto($$, $1);
}
| designated_initializer_designator '[' comma_expression ']'
| designator '[' comma_expression ']'
{
$$=$1;
stack($2).id(ID_index);
mto($2, $3);
mto($$, $2);
}
| designated_initializer_designator '[' comma_expression TOK_ELLIPSIS comma_expression ']'
| designator '[' comma_expression TOK_ELLIPSIS comma_expression ']'
{
// TODO
$$=$1;
@ -1883,7 +1882,7 @@ designated_initializer_designator:
mto($2, $3);
mto($$, $2);
}
| designated_initializer_designator '.' member_name
| designator '.' member_name
{
$$=$1;
stack($2).id(ID_member);