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

Analyzing a simple C++ program with Frama-C

本文关键字：简单 一个 C++ 程序 Frama-C 使用      更新时间：2023-10-16

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

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时，我在输出中收到警告和错误：

$ 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 是从版本 20170501+Phosphorus+dfsg-2 的 debian-test 仓库安装的）

首先，我想指出Frama-Clang页面上的警告：

Frama-Clang目前处于开发的早期阶段。众所周知，它是不完整的，并且没有任何无错误保证。

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

也就是说，正如评论中提到的，问题是 Frama-Clang 中的 STL 支持很少（特别是，当涉及到模板时，看起来无辜的iostream并不是最容易处理的代码段）。

使用frama-c -cxx-nostdinc refs.cc可能会有更好的运气，它将使用系统的标准库而不是Frama-Clang附带的库：这至少可以让clang对代码进行类型检查。然而，绝对不能保证Frama-Clang本身能够理解这个库提供的所有结构。

相关文章：