sizeof shouldn't work for forward declared structs

[danielsn]

#include <stdlib.h>
#include <assert.h>

struct foo;

int main(int argc, char **argv)
{
  struct foo* thefoo = malloc(sizeof(struct foo));
  size_t s = sizeof(struct foo);
  assert(s == 0);
}

~/temp $ cbmc cbmc-test.c
CBMC version 5.12 (cbmc-5.12-d8598f8-1008-gfab409d18) 64-bit x86_64 macos
Parsing cbmc-test.c
Converting
Type-checking cbmc-test
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
size of program expression: 72 steps
simple slicing removed 0 assignments
Generated 1 VCC(s), 0 remaining after simplification

** Results:
cbmc-test.c function main
[main.assertion.1] line 10 assertion s == 0: SUCCESS

** 0 of 1 failed (1 iterations)
VERIFICATION SUCCESSFUL

~/temp $ gcc cbmc-test.c
cbmc-test.c:8:31: error: invalid application of 'sizeof' to an incomplete type
      'struct foo'
  struct foo* thefoo = malloc(sizeof(struct foo));
                              ^     ~~~~~~~~~~~~
cbmc-test.c:4:8: note: forward declaration of 'struct foo'
struct foo;
       ^
cbmc-test.c:9:14: error: invalid application of 'sizeof' to an incomplete type
      'struct foo'
  size_t s = sizeof(struct foo);
             ^     ~~~~~~~~~~~~
cbmc-test.c:4:8: note: forward declaration of 'struct foo'
struct foo;
       ^
2 errors generated.

CBMC version:
Operating system:
Exact command line resulting in the issue:
What behaviour did you expect: I expected sizeof on an forward declared type to fail
What happened instead: CBMC decided it was 0, and gave no warning.

[danielsn]

@tautschnig

[danielsn]

Technically its Clang that complained, not gcc.

~/temp $ gcc --version
Configured with: --prefix=/Applications/Xcode.app/Contents/Developer/usr --with-gxx-include-dir=/usr/include/c++/4.2.1
Apple LLVM version 9.0.0 (clang-900.0.39.2)
Target: x86_64-apple-darwin16.7.0
Thread model: posix
InstalledDir: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin

[xbauch]

Hi @danielsn, we think the PR #5211 fixed the issue. Could you please confirm that?

[danpoe]

This is now fixed. cbmc will report a conversion error:

CBMC version 5.12 (cbmc-5.12.2-21-g63c32d9e7) 64-bit x86_64 linux
Parsing test.c
Converting
Type-checking test
file test.c line 8 function main: invalid application of 'sizeof' to an incomplete type
	'struct foo'
CONVERSION ERROR