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.

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

最佳答案

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

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

如 Frama-Clang 网页所示，



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

如果您尝试使用非 STL 文件，您应该会获得更好的结果。部分 STL 受支持，但没有关于哪些类是哪些类的完整列表(因为它在不断发展)。

例如，下面的玩具示例使用 std::exception 、模板和类，只需运行 frama-c test.cpp 即可通过 Frama-Clang 成功解析(尽管有一些警告)。

#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;
  }
}

关于c++ - 如何使用 Frama-Clang 解析 C++ 程序，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/51586499/