Can't verify with CBMC in Ubuntu c++ programs - compiler type_traits.h template specialization with wrong number of arguments

Question

I am trying to use the CBMC 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.

---

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

Α .c file with name file2.c:

int array[10];
int sum(){
unsigned i,sum;
sum=0;
for(i=0;i<10;i++)
sum+=array[i];
}

In terminal type:

cbmc file2.c --function sum

Output:

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

---

When I try to execute the following .cpp file I get an error.

sum_num.cpp file:

// This program adds two numbers and prints their sum.
#include <iostream>

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

  sum = a + b;

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

  return 0;
}

Type in terminal:

cbmc sum_num.cpp --function main

Output - Error:

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

Answer 1

Apparently, at the time being cbmc has limited support for templates and does not cover all of their potential uses.

Until the situation changes, you can either:

1. roll-back to a c++ distribution which does not have such template usage in the file /usr/include/c++/4.9/ext/type_traits.h (4.8 does have it too, so an older one)

2. remove #include<iostream> and rely on the standard C printf() function:

   #include<stdio.h>
   
   int main()
   {
       int a;
       int b;
       int sum;
   
       sum = a + b;
   
       printf("The sum of %d and %d is %d\n", a, b, sum);
   
       return 0;
   }
   

Both of these suggestions have been proposed HERE.