Can't verify with CBMC in Ubuntu c++ programs - compiler type_traits.h template specialization with wrong number of arguments
<p>I am trying to use the <a href="http://www.cprover.org/cbmc/" rel="nofollow">CBMC</a> Bounded Model Checker in Ubuntu for both C and C++ programs.
I have downloaded gcc (4.9 v) and g++ (4.9 v) compilers and I installed the CBMC through terminal.</p>

<hr>

<p>I am able to verify C programs and no problems arise using the below procedure:</p>

<p>Α .c file with name <code>file2.c</code>:</p>

<pre><code>int array[10];
int sum(){
unsigned i,sum;
sum=0;
for(i=0;i&lt;10;i++)
sum+=array[i];
}
</code></pre>

<p>In terminal type:</p>

<pre><code>cbmc file2.c --function sum
</code></pre>

<p>Output:</p>

<pre><code>file file2.c: Parsing
Converting
Type-checking file2
Generating GOTO Program
Adding CPROVER library
Function Pointer Removal
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
Unwinding loop c::sum.0 iteration 1 file file2.c line 5 function sum thread 0
Unwinding loop c::sum.0 iteration 2 file file2.c line 5 function sum thread 0
Unwinding loop c::sum.0 iteration 3 file file2.c line 5 function sum thread 0
Unwinding loop c::sum.0 iteration 4 file file2.c line 5 function sum thread 0
Unwinding loop c::sum.0 iteration 5 file file2.c line 5 function sum thread 0
Unwinding loop c::sum.0 iteration 6 file file2.c line 5 function sum thread 0
Unwinding loop c::sum.0 iteration 7 file file2.c line 5 function sum thread 0
Unwinding loop c::sum.0 iteration 8 file file2.c line 5 function sum thread 0
Unwinding loop c::sum.0 iteration 9 file file2.c line 5 function sum thread 0
Unwinding loop c::sum.0 iteration 10 file file2.c line 5 function sum thread 0
size of program expression: 71 steps
simple slicing removed 0 assignments
Generated 0 VCC(s), 0 remaining after simplification
VERIFICATION SUCCESSFUL
</code></pre>

<hr>

<p>When I try to execute the following .cpp file I get an error.</p>

<p><code>sum_num.cpp</code> file:</p>

<pre><code>// This program adds two numbers and prints their sum.
#include &lt;iostream&gt;

int main()
{
  int a;
  int b;
  int sum;

  sum = a + b;

  std::cout&lt;&lt;"The sum of "&lt;&lt;a&lt;&lt;" and "&lt;&lt;b&lt;&lt;" is "&lt;&lt;sum&lt;&lt;"\n";

  return 0;
}
</code></pre>

<p>Type in terminal:</p>

<pre><code>cbmc sum_num.cpp --function main
</code></pre>

<p>Output - Error:</p>

<pre><code>file sum_num.cpp: Parsing
Converting
Type-checking sum_num
file /usr/include/c++/4.9/ext/type_traits.h line 172: template specialization with wrong number of arguments
CONVERSION ERROR
</code></pre>