Easy pointer alignment bug

[lookfwd]

Hello, there's a - hope it to be - simple bug when you play with bool's and pointers. More specifically the example below fails for any padding size >= 2:

#include <assert.h>

struct TestBench {

    bool padding[2];
    unsigned monitor;

    TestBench()
        : monitor(0u)
    {
        unsigned * m1 = &monitor;
        *m1 = 1u;
    
        assert(monitor == 1u);
    }
};

int main()
{
    TestBench tb;

    return 0;
}

Problem:

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
size of program expression: 46 steps
simple slicing removed 13 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.1 with simplifier
162 variables, 0 clauses
SAT checker: instance is SATISFIABLE
Solving with MiniSAT 2.2.1 with simplifier
162 variables, 0 clauses
SAT checker inconsistent: instance is UNSATISFIABLE
Runtime decision procedure: 0.005s

** Results:
[] assertion monitor == 1u: SUCCESS
[TestBench.assertion.1] assertion monitor == 1u: FAILURE

Trace for TestBench.assertion.1:

State 14 file tmp3.cpp line 20 function main thread 0
----------------------------------------------------
  tb={ .padding={ false, false }, .monitor=0u } ({ { 0, 0 }, 00000000000000000000000000000000 })

State 16 file tmp3.cpp line 20 function main thread 0
----------------------------------------------------
  this=((struct *)NULL) (0000000000000000000000000000000000000000000000000000000000000000)

State 17 file tmp3.cpp line 20 function main thread 0
----------------------------------------------------
  this=tb@1.padding (0000001000000000000000000000000000000000000000000000000000000000)

State 18 file tmp3.cpp line 9 thread 0
----------------------------------------------------
  tb.monitor=0u (00000000000000000000000000000000)

State 19 file tmp3.cpp line 11 function TestBench thread 0
----------------------------------------------------
  m1=((const unsigned *)NULL) (0000000000000000000000000000000000000000000000000000000000000000)

State 20 file tmp3.cpp line 11 function TestBench thread 0
----------------------------------------------------
  m1=&tb@1.monitor (0000001000000000000000000000000000000000000000000000000000000010)

State 21 file tmp3.cpp line 12 function TestBench thread 0
----------------------------------------------------
  tb={ .padding={ false, false }, .monitor=0u } ({ { 0, 0 }, 00000000000000000000000000000000 })

Violated property:
  file tmp3.cpp line 14 function TestBench
  assertion monitor == 1u
  !((_Bool)(signed long int)(signed long int)!(this->monitor == 1u))


** 1 of 2 failed (2 iterations)
VERIFICATION FAILED

[thomasspriggs]

I have been unable to reproduce this with the current develop version of cbmc. Therefore I am going to close this out on the basis that it must have been fixed sometime in the 3 years since this issue was raised. Below is the output from cbmc for reference -

cbmc output

$ cbmc ./Issue534_example.cpp
CBMC version 5.25.0 (cbmc-5.25.0-dirty) 64-bit x86_64 linux
Parsing ./Issue534_example.cpp
Converting
Type-checking Issue534_example
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
Runtime Symex: 0.00112504s
size of program expression: 59 steps
simple slicing removed 0 assignments
Generated 1 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 1.6238e-05s

** Results:
./Issue534_example.cpp function TestBench
[TestBench.assertion.1] line 15 assertion monitor == 1u: SUCCESS

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

Please feel free to reopen this ticket if this issue can actually be reproduced with the current version of cbmc.