无法在Ubuntu c++程序中使用CBMC进行验证-编译器type_traits.h模板专门化且参数数错误

Question

我试图在Ubuntu中为C和C++程序使用CBMC有界模型检查器。我下载了gcc (4.9V)和g++ (4.9V)编译器，并通过终端安装了CBMC。

我能够验证C程序，使用以下过程不会出现任何问题：

名为.c file2.c的ΑΑ文件

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

终端类型：

cbmc file2.c --function sum

输出：

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

当我尝试执行以下.cpp文件时，会得到一个错误。

sum_num.cpp文件：

// 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;
}

输入终端：

cbmc sum_num.cpp --function main

输出-错误：

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

显然，在的时候，cbmc对模板的支持有限，并且没有涵盖它们的所有潜在用途。

在情况发生变化之前，您可以：

1. 回滚到c++发行版，该发行版在文件/usr/include/c++/4.9/ext/type_traits.h中没有这样的模板用法(4.8也有，所以是旧的)。
2. 删除#include<iostream>并依赖标准的C printf()函数： #include int (){ int a；int b；int sum；sum =a+ b；printf(“%d和%d的和为%d\n"，a，b，sum)；返回0；}

这两项建议都是这里提出的。