用Frama-C分析一个简单的C ++程序 [英] Analyzing a simple C++ program with Frama-C

查看:173
本文介绍了用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目前处于开发的早期阶段.已知它不完整,并且没有任何错误修复保证.

Frama-Clang is currently in an early stage of development. It is known to be incomplete and comes without any bug-freeness guarantee.

因此,如果您还不熟悉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 ++程序的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!

查看全文
登录 关闭
扫码关注1秒登录
发送“验证码”获取 | 15天全站免登陆