Closed
Description
This is - I hope - a simple bug. Here's how to reproduce it:
struct Status
{
bool foo = 0; // If this is not bool, it's ok
char bar = 0; // If you remove this it's ok
};
struct Box
{
Status status[4]; // If this isn't 4, it's ok
};
class Container
{
Box boxes[3]; // If this is <3 it's ok
public:
void setStatus(const Status & status) // If this isn't pass by ref it's ok
{
bool foo = status.foo;
}
};
int main()
{
Container c;
c.setStatus(c.boxes[1].status[0]);
return 0;
}
It gives:
CBMC version 5.6 64-bit x86_64 macos
Parsing tmp3.cpp
Converting
Type-checking tmp3
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
Assertion failed: (el_size%8==0), function simplify_byte_extract, file simplify_expr.cpp, line 2033.
Abort trap: 6
Metadata
Metadata
Assignees
Labels
No labels