Skip to content

CBMC error if variable of type struct with flexible array member is forward declared and initialized #6787

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.

Sign up for GitHub

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

Jump to bottom
Closed
andreast271 opened this issue Apr 7, 2022 · 1 comment · Fixed by #6788
Closed

CBMC error if variable of type struct with flexible array member is forward declared and initialized #6787

andreast271 opened this issue Apr 7, 2022 · 1 comment · Fixed by #6788
Labels
pending merge

Comments

@andreast271
Copy link
Contributor

CBMC version: cbmc-5.54.0-13-gf3e4096300
Operating system: Linux x86_64
Exact command line resulting in the issue: cbmc fam.c
What behaviour did you expect: termination with message VERIFICATION SUCCESSFUL and exit status 0
What happened instead: termination with message CONVERSION ERROR and exit status 6

The error occurs in the following scenario:

  1. There is a struct St with a flexible array member
  2. A global variable with type St is both forward declared and initialized

The test case fam.c.txt is attached.
The output is in file cbmc.log.

The problem was introduced by the following commit:
commit b16c7d7
Author: Michael Tautschnig [email protected]
Date: Fri Feb 11 13:17:17 2022 +0000

Reverting commit b16c7d7 on top of commit f3e4096 fixes the error, but I did not check if it causes other problems.
@tautschnig tautschnig self-assigned this Apr 7, 2022
tautschnig added a commit to tautschnig/cbmc that referenced this issue Apr 7, 2022
@tautschnig
Flexible array members: make type checking aware and fix bounds checking
da0c44a 
Type checking must be ready to handle type changes between declaration
and definition, which b16c7d7 introduced. Also, bounds checking must
not use `size_of_expr` with these as 24eba85 rightly introduced a
distinction between "sizeof" and the actual object size as mandated by
the C standard.

Fixes: diffblue#6787
@tautschnig tautschnig mentioned this issue Apr 7, 2022
Merged
4 tasks
@tautschnig
Copy link
Collaborator

Thank you for the detailed report and the test case! #6788 now fixes the problem (without having to revert b16c7d7).

@tautschnig tautschnig removed their assignment Apr 7, 2022
tautschnig added a commit to tautschnig/cbmc that referenced this issue Apr 9, 2022
@tautschnig
Flexible array members: make type checking aware and fix bounds checking
3f9754b 
Type checking must be ready to handle type changes between declaration
and definition, which b16c7d7 introduced. Also, bounds checking must
not use `size_of_expr` with these as 24eba85 rightly introduced a
distinction between "sizeof" and the actual object size as mandated by
the C standard.

Fixes: diffblue#6787
tautschnig added a commit to tautschnig/cbmc that referenced this issue Apr 20, 2022
@tautschnig
Flexible array members: make type checking aware and fix bounds checking
22bd66f 
Type checking must be ready to handle type changes between declaration
and definition, which b16c7d7 introduced. Also, bounds checking must
not use `size_of_expr` with these as 24eba85 rightly introduced a
distinction between "sizeof" and the actual object size as mandated by
the C standard.

Fixes: diffblue#6787
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
pending merge
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Flexible array members: make type checking aware and fix bounds checking tautschnig/cbmc
2 participants
@tautschnig @andreast271