Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

ansi-c/Array_Declarator* regression tests: front end is too permissive #132

Open
tautschnig opened this issue Jun 20, 2016 · 0 comments
Open

Comments

@tautschnig
Copy link
Collaborator

These are marked KNOWNBUG at the moment, because goto-cc accepts what gcc wouldn't:

Array_Declarator2/main.c:5:18: error: variable length array must be bound in function definition
void fooStar(int x[*])
                 ^
1 error generated.
$ gcc Array_Declarator3/main.c
Array_Declarator3/main.c:7:11: error: type qualifier used in array declarator outside of function prototype
  int bar0[restrict] = {0};
          ^
1 error generated.
$ gcc Array_Declarator4/main.c
Array_Declarator4/main.c:7:11: error: 'static' used in array declarator outside of function prototype
  int bar1[static 1U] = {1};
          ^
1 error generated.
$ gcc Array_Declarator5/main.c
Array_Declarator5/main.c:7:11: error: type qualifier used in array declarator outside of function prototype
  int bar2[restrict 2U] = {1, 2};
          ^
1 error generated.
$ gcc Array_Declarator6/main.c
Array_Declarator6/main.c:7:11: error: 'static' used in array declarator outside of function prototype
  int bar3[restrict static 3U] = {1, 2, 3};
          ^
1 error generated.
$ gcc Array_Declarator7/main.c
Array_Declarator7/main.c:7:11: error: 'static' used in array declarator outside of function prototype
  int bar4[static restrict 4U] = {1, 2, 3, 4};
          ^
1 error generated.

It may be debatable whether the C front end really needs to produce errors here, it safely ignores these extra qualifiers anyway.

Best,
Michael

smowton pushed a commit to smowton/cbmc that referenced this issue May 9, 2018
…r_PR

SEC-19: Introducing irept_instrumenter.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants