Не удается проверить с помощью CBMC в программах на Ubuntu c ++ — специализация шаблона компилятора type_traits.h с неверным количеством аргументов

Question

Не удается проверить с помощью CBMC в программах на Ubuntu c ++ — специализация шаблона компилятора type_traits.h с неверным количеством аргументов

Я пытаюсь использовать CBMC Ограниченная проверка моделей в Ubuntu для программ на C и C ++.
Я скачал компиляторы gcc (4.9 v) и g ++ (4.9 v) и установил CBMC через терминал.

Я могу проверить программы на C, и никаких проблем не возникает, используя следующую процедуру:

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

1

c++cbmc g++model-checking ubuntu

Решение

Другие решения

Других решений пока нет …

Источник

Accepted Answer

По-видимому, в настоящее время CBMC имеет ограниченную поддержку шаблоны и не охватывает все их потенциальное использование.

Пока ситуация не изменится, вы можете:

откат к дистрибутиву c ++, который не имеет такого использования шаблона в файле /usr/include/c++/4.9/ext/type_traits.h (У 4.8 тоже есть, так что старше)

Удалить #include<iostream> и полагаться на стандарт С printf() функция:

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

Оба эти предложения были предложены ВОТ.

1