用Frama-C分析一个简单的C ++程序

问题描述

我从一个很棒的教程开始学习C ++，该教程位于 https://learnxinyminutes.com/docs/c++/，并希望在Frama-C中分析一个显示引用的最简单示例:

I started learning C++ from a great tutorial available at https://learnxinyminutes.com/docs/c++/ and would like to analyze in Frama-C a simplest example that shows references:

using namespace std;
#include <iostream>
#include <string>

int main() {
    string foo = "I am foo";
    string bar = "I am bar";

    string& fooRef = foo; // This creates a reference to foo.
    fooRef += ". Hi!"; // Modifies foo through the reference
    cout << fooRef; // Prints "I am foo. Hi!"

    // Doesn't reassign "fooRef". This is the same as "foo = bar", and
    //   foo == "I am bar"
    // after this line.
    cout << &fooRef << endl; //Prints the address of foo
    fooRef = bar;
    cout << &fooRef << endl; //Still prints the address of foo
    cout << fooRef;  // Prints "I am bar"

    //The address of fooRef remains the same, i.e. it is still referring to foo.
    return 0;
}

我编译并安装了名为"Frama-Clang"的Frama-C C ++插件.现在，当我运行frama-c时，输出中将显示警告和错误:

I compiled and installed Frama-C C++ plug-in called "Frama-Clang".Now when I run frama-c I get warnings and errors in the output:

$ frama-c refs.cc
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing refs.cc (external front-end)
refs.cc:13:17: warning: using directive refers to implicitly-defined namespace 'std'
using namespace std;
                ^
In file included from refs.cc:14:
In file included from /usr/share/frama-c/frama-clang/libc++/iostream:29:
/usr/share/frama-c/frama-clang/libc++/ostream:31:40: error: implicit instantiation of undefined template 'std::basic_ios<char, std::char_traits<char> >'
  class basic_ostream : virtual public basic_ios<charT,traits> {
                                       ^
refs.cc:23:7: note: in instantiation of template class 'std::basic_ostream<char, std::char_traits<char> >' requested here
        cout << fooRef; // Prints "I am foo. Hi!"
             ^
/usr/share/frama-c/frama-clang/libc++/iosfwd:37:68: note: template is declared here
  template <class charT, class traits = char_traits<charT> > class basic_ios;
                                                                   ^
code generation aborted due to one compilation error
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
[kernel] user error: stopping on file "refs.cc" that has errors.
[kernel] Frama-C aborted: invalid user input.

怎么了?

(Frama-C是从debian-testing存储库中安装的，版本为20170501 + phosphorus + dfsg-2)

(Frama-C is installed from a debian-testing repository in version 20170501+phosphorus+dfsg-2)

推荐答案

首先，我想指出 Frama-Clang页面:

因此，如果您还不熟悉C ++，我建议您立即开始使用Frama-Clang可能是一项巨大的努力.

Thus, if you're not already familiar with C++, I'd kindly suggest that starting right away with Frama-Clang might be a pretty big effort.

也就是说，正如评论中提到的那样，问题是Frama-Clang对STL的支持是最小的(特别是，看上去无辜的 iostream 并非最简单的代码段)处理模板).

That said, the issue is, as mentioned in the comments, that STL support in Frama-Clang is minimal (in particular, the innocent-looking iostream is not exactly the easiest piece of code to handle when it comes to templates).

使用 frama-c -cxx-nostdinc refs.cc 可能会带来更好的运气，它将使用系统的标准库，而不是Frama-Clang随附的标准库: clang 对您的代码进行类型检查.但是，绝对不能保证Frama-Clang本身就能理解该库提供的所有构造.

You might have better luck by using frama-c -cxx-nostdinc refs.cc, which will use your system's standard library instead of the one shipped with Frama-Clang: this will at least let clang type-check your code. There is however absolutely no guarantee that Frama-Clang itself will be able to understand all the constructions provided by this library.

这篇关于用Frama-C分析一个简单的C ++程序的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！