我正在尝试使用 CBMC Ubuntu 中用于 C 和 C++ 程序的有界模型检查器。 我已经下载了 gcc (4.9 v) 和 g++ (4.9 v) 编译器,并通过终端安装了 CBMC。
我能够验证 C 程序并且使用以下过程没有出现问题:
名为 file2.c
的 .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
最佳答案
显然,目前 cbmc 对模板 的支持有限,并未涵盖它们的所有潜在用途。
在情况发生变化之前,您可以:
回滚到文件中没有此类模板用法的 c++ 发行版
/usr/include/c++/4.9/ext/type_traits.h
(4.8也有,所以比较老)删除
#include<iostream>
并依赖标准 Cprintf()
功能:#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; }
这两个建议都被提出了HERE .
关于c++ - 无法在 Ubuntu c++ 程序中使用 CBMC 进行验证 - 参数数量错误的编译器 type_traits.h 模板特化,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/36196567/