C frontend issue with arrays that are declared without a length #5022
Assignees
Labels
Comments
romainbrenguier
added a commit
to romainbrenguier/cbmc
that referenced
this issue
Aug 15, 2019
In some cases, like the test in regression/cbmc/Global_Initialization2, the array type is incomplete and changed in the symbol table after the main function has been converted, leading to inconsistencies. This means we can get nil instead of the size in field_sensitivityt::apply, though the actual size is present in the symbol table. The issue is reported here: diffblue#5022
romainbrenguier
added a commit
to romainbrenguier/cbmc
that referenced
this issue
Aug 16, 2019
In some cases, like the test in regression/cbmc/Global_Initialization2, the array type is incomplete and changed in the symbol table after the main function has been converted, leading to inconsistencies. This means we can get nil instead of the size in field_sensitivityt::apply, though the actual size is present in the symbol table. The issue is reported here: diffblue#5022
romainbrenguier
added a commit
to romainbrenguier/cbmc
that referenced
this issue
Aug 20, 2019
In some cases, like the test in regression/cbmc/Global_Initialization2, the array type is incomplete and changed in the symbol table after the main function has been converted, leading to inconsistencies. This means we can get nil instead of the size in field_sensitivityt::apply, though the actual size is present in the symbol table. The issue is reported here: diffblue#5022
romainbrenguier
added a commit
to romainbrenguier/cbmc
that referenced
this issue
Aug 20, 2019
In some cases, like the test in regression/cbmc/Global_Initialization2, the array type is incomplete and changed in the symbol table after the main function has been converted, leading to inconsistencies. This means we can get nil instead of the size in field_sensitivityt::apply, though the actual size is present in the symbol table. The issue is reported here: diffblue#5022
romainbrenguier
added a commit
to romainbrenguier/cbmc
that referenced
this issue
Aug 21, 2019
In some cases, like the test in regression/cbmc/Global_Initialization2, the array type is incomplete and changed in the symbol table after the main function has been converted, leading to inconsistencies. This means we can get nil instead of the size in field_sensitivityt::apply, though the actual size is present in the symbol table. The issue is reported here: diffblue#5022
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
As noticed in this PR #4680 (comment)
in the example https://github.com/diffblue/cbmc/blob/develop/regression/cbmc/Global_Initialization2/main.c
the type of the array (which is declared without a length and not defined) is created with undefined length and then attached to various expressions from which the goto program is constructed. The implementation of rule 6.9.2 (https://github.com/diffblue/cbmc/blob/develop/regression/cbmc/Global_Initialization2/main.c#L15) then updates the array length of the symbol in the symbol table only, but not in the goto program. When symex takes the length from the goto program, it doesn't contain the correct length - the correct length is in the symbol table only.
CBMC version: 5.12
Operating system: ubuntu 16.04
Exact command line resulting in the issue: cbmc main.c
What behaviour did you expect: the type of the array in the goto program should be set according to rule 6.9.2
What happened instead: the type is set correctly for the array entry in the symbol table but not inside code which contains the array
The text was updated successfully, but these errors were encountered: