2

C と C++ の両方のプログラムに対して、Ubuntu でCBMC Bounded Model Checkerを使用しようとしています。gcc (4.9 v) および g++ (4.9 v) コンパイラをダウンロードし、端末から 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
4

1 に答える 1

1

明らかに、現時点ではcbmcはテンプレートのサポートを制限しており、潜在的な用途をすべてカバーしているとは言えません。

状況が変わるまで、次のいずれかを実行できます。

  1. ファイルにそのようなテンプレートの使用法がない C++ ディストリビューションにロールバックします/usr/include/c++/4.9/ext/type_traits.h(4.8 にもあるため、古いものです)。

  2. 削除して、標準の C関数#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;
}

これらの提案はどちらもここで提案されています。

于 2016-04-05T11:08:12.290 に答える