使用 Frama-C 分析预编译的 C++ 文件

问题描述

我正在尝试使用 Frama-C 分析一些预编译的 C++ 文件 (.ii)。我知道它有很多限制，但我的问题与我认为与 clang 编译器有关的编译错误有关。我正在使用 Frama-21.0 和 clang-0.0.9。

我正在使用在 this issue 中找到的示例，但包括 vector 库，因为我需要其他文件。

#include <exception>
#include <vector>

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

所以我可以使用 Clang-9 和这些命令编译和预编译文件：

clang++ -std=c++17 -stdlib=libc++ data/example.cpp -o example

clang++ -std=c++17 -stdlib=libc++ data/example.cpp -E > data/example.ii

但是，当我尝试使用 frama-c 分析文件时，使用以下命令：

frama-c data/example.ii -cxx-c++stdlib-path /usr/local/clang_9.0.0/include/c++/v1 -deps > logFiles/example.log

我明白了：

[kernel] Parsing data/example.ii (external front-end)
[kernel] User Error: Failed to parse C++ file. See Clang messages for more information
[kernel] User Error: stopping on file "data/example.ii" that has errors.
[kernel] Frama-C aborted: invalid user input.

Clang 消息是这样的：

/home/data/example.ii:411:41: error: use of undeclared identifier '__int128_t'
template <> struct __libcpp_is_integral<__int128_t> : public true_type {};
                                        ^
/home/data/example.ii:412:41: error: use of undeclared identifier '__uint128_t'
template <> struct __libcpp_is_integral<__uint128_t> : public true_type {};
                                        ^
/home/data/example.ii:1329:17: error: use of undeclared identifier '__int128_t'
    __type_list<__int128_t,^
/home/data/example.ii:1335:5: error: expected a type
    > > > > > __signed_types;
    ^
/home/data/example.ii:1335:7: error: expected a type
    > > > > > __signed_types;
      ^
/home/data/example.ii:1335:9: error: expected a type
    > > > > > __signed_types;
        ^
/home/data/example.ii:1335:11: error: expected a type
    > > > > > __signed_types;
          ^
/home/data/example.ii:1335:13: error: expected a type
    > > > > > __signed_types;
            ^
/home/data/example.ii:1344:17: error: use of undeclared identifier '__uint128_t'
    __type_list<__uint128_t,^
/home/data/example.ii:1350:5: error: expected a type
    > > > > > __unsigned_types;
    ^
/home/data/example.ii:1350:7: error: expected a type
    > > > > > __unsigned_types;
      ^
/home/data/example.ii:1350:9: error: expected a type
    > > > > > __unsigned_types;
        ^
/home/data/example.ii:1350:11: error: expected a type
    > > > > > __unsigned_types;
          ^
/home/data/example.ii:1350:13: error: expected a type
    > > > > > __unsigned_types;
            ^
/home/data/example.ii:1352:74: error: type 'int' cannot be used prior to '::' because it has no members
template <class _TypeList,size_t _Size,bool = _Size <= sizeof(typename _TypeList::_Head)> struct __find_first;
                                                                         ^
/home/data/example.ii:1421:22: note: in instantiation of default argument for '__find_first<int,sizeof(_Tp)>' required here
    typedef typename __find_first<__signed_types,sizeof(_Tp)>::type type;
                     ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
/home/data/example.ii:1421:65: error: expected a qualified name after 'typename'
    typedef typename __find_first<__signed_types,sizeof(_Tp)>::type type;
                                                                ^

有什么建议吗？？ 提前致谢

解决方法

暂无找到可以解决该程序问题的有效方法，小编努力寻找整理中！

如果你已经找到好的解决方法，欢迎将解决方案带上本链接一起发送给小编。

小编邮箱:dio#foxmail.com (将#修改为@）