时间戳

首页 > 解决方案 > 如何使用 Frama-Clang 解析 C++ 程序

c++ - 如何使用 Frama-Clang 解析 C++ 程序

问题描述

我已经安装了 Frama-c 的插件 Frama-Clang 来解析 C++ 程序。但是，我不知道如何正确使用它。我用一个非常简单的 c++ 程序尝试了它，但失败了。这是test.cpp的代码：

#include <iostream>
using namespace std;
int main()
{
    cout << "Hello, world!" << endl;
    return 0;
}

我使用命令 frama-c test.cpp 并得到以下错误：

[kernel] Parsing test.cpp (external front-end)
In file included from test.cpp:1:
In file included from /home/server3/.opam/system/share/frama-c/frama-clang/libc++/iostream:29:
/home/server3/.opam/system/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> {
                                       ^
test.cpp:5:10: note: in instantiation of template class 'std::basic_ostream<char, std::char_traits<char> >' requested here
    cout << "Hello, world!" << endl;
         ^
/home/server3/.opam/system/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 "test.cpp" that has errors.
[kernel] Frama-C aborted: invalid user input.

有人可以告诉我如何成功解析它吗？

标签： c++frama-c

解决方案

您的用法是正确的：只需给它一个.cpp文件，它就会尝试解析它。

但是，由于 STL 的大小和复杂性，使用 Hello World<iostream>并不是最好的示例：您的程序在预处理后包含 18k 到 28k 行（取决于我使用的是g++还是clang）。

如 Frama-Clang 网页所示，

Frama-Clang 目前处于开发的早期阶段。众所周知，它是不完整的 (...)

处理 STL 确实是支持 C++ 的主要困难之一，目前正在开发中。

如果您尝试使用非 STL 文件，您应该会得到更好的结果。支持 STL 的一部分，但没有完整的列表来说明哪些类是哪些类是不支持的（因为这是不断发展的）。

例如，下面的玩具示例使用std::exception、模板和类，只需运行frama-c test.cpp.

#include <exception>

class empty_stack: public std::exception {
  virtual const char* what() const throw() {
    return "stack is empty!";
  }
};

class full_stack: public std::exception {
  virtual const char* what() const throw() {
    return "stack is full!";
  }
};

template <class T>
class Stack {
private:
  T elems[10];
  unsigned index;
public:
  Stack() {
    index = 0;
  }
  void push(T const&);
  T pop();
  T top() const;
  bool empty() const {
    return index == 0;
  }
};

template <class T>
void Stack<T>::push (T const& elem) {
  if (index >= 10) throw new full_stack();
  elems[index++] = elem;
}

template <class T>
T Stack<T>::pop () {
  if (index == 0) throw new empty_stack;
  return elems[--index];
}

template <class T>
T Stack<T>::top () const {
  if (index == 0) throw new empty_stack;
  return elems[index-1];
}

int main() {
  try {
    Stack<int> intStack;
    intStack.push(7);
    intStack.push(42);
    return intStack.pop();
  } catch (char* ex) {
    return -1;
  }
}

推荐阅读