Bugs on variable initializations

[lookfwd]

Example:

#include <assert.h>

class C
{
    int x;

    C()
    : x(7) {}
};

C c1;

class D
{
    int x = 7;
};

int main()
{    
    assert(c1.x == 7); // Fails

    C c2;
    assert(c2.x == 7); // Succeeds

    D d;
    assert(d.x == 7); // C++11 Class Member Initialization Fails

    return 0;
}

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

** Results:
[main.assertion.1] assertion c1.x == 7: FAILURE
[main.assertion.2] assertion c2.x == 7: SUCCESS
[main.assertion.3] assertion d.x == 7: FAILURE

Trace for main.assertion.1:

Violated property:
  file tmp3.cpp line 22 function main
  assertion c1.x == 7
  !((_Bool)(signed long int)(signed long int)!(c1.x == 7))


Trace for main.assertion.3:

Violated property:
  file tmp3.cpp line 22 function main
  assertion c1.x == 7
  !((_Bool)(signed long int)(signed long int)!(c1.x == 7))


State 17 file tmp3.cpp line 24 function main thread 0
----------------------------------------------------
  c2={ .x=0 } ({ 00000000000000000000000000000000 })

State 19 file tmp3.cpp line 24 function main thread 0
----------------------------------------------------
  this=((class *)NULL) (0000000000000000000000000000000000000000000000000000000000000000)

State 20 file tmp3.cpp line 24 function main thread 0
----------------------------------------------------
  this=&c2@1.x (0000001000000000000000000000000000000000000000000000000000000000)

State 21 file tmp3.cpp line 8 thread 0
----------------------------------------------------
  c2.x=7 (00000000000000000000000000000111)

State 25 file tmp3.cpp line 27 function main thread 0
----------------------------------------------------
  d={ .x=8388615 } ({ 00000000100000000000000000000111 })

State 27 file tmp3.cpp line 27 function main thread 0
----------------------------------------------------
  this=((class *)NULL) (0000000000000000000000000000000000000000000000000000000000000000)

State 28 file tmp3.cpp line 27 function main thread 0
----------------------------------------------------
  this=&d@1.x (0000001100000000000000000000000000000000000000000000000000000000)

Violated property:
  file tmp3.cpp line 28 function main
  assertion d.x == 7
  !((_Bool)(signed long int)(signed long int)!(d.x == 7))


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