2

I'm trying to analyze some pre-compiled C++ files (.ii) using Frama-C. I know it has many limitations, but my problem has to do with compilation errors which I think are related to the clang compiler. I'm using Frama-21.0 and clang-0.0.9.

I'm using the example I found in this issue but including the vector library, because I needed for my other files.

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

So I am able to compile and pre-compile the file using Clang-9 with these command:

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

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

But then, when I try to analyze the files with frama-c, with this command:

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

I get this:

[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.

And the Clang messages are like this:

/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;
                                                                ^

Any suggestions?? Thanks in advance

José Luis
  • 21
  • 2
  • Ask on [this Frama-C list](https://groupes.renater.fr/sympa/subscribe/frama-c-discuss). I think that Frama-C is more for C programs than for C++ ones. You might get information about experimental C++ support using [Frama-Clang](https://frama-c.com/fc-plugins/frama-clang.html) – Basile Starynkevitch Jan 14 '21 at 10:06
  • I suspect that the problem lies in the fact that you're mixing your system C++ library with Frama-C's standard C headers. Adding option `-cxx-cstdlib /usr/include` (or another appropriate path) might let clang properly typecheck the code. However, I doubt that you will be able to get much further than that (in particular Frama-C does not support 128-bit integers, so that e.g. `__int128_t` might be a little bit problematic, even before we speak about complex C++ constructions) – Virgile Jan 14 '21 at 14:11
  • I've tried with both "-cxx-cstdlib-path /usr/include/ -cxx-c++stdlib-path /usr/include/" and now the message error is the following: `Unknown kind of comment at /usr/lib/gcc/x86_64-linux-gnu/9/../../../../include/c++/9/new:114:114:15`. I don't know if it can be considered as progress... Anyway, is there and example on C++ code with std libraries that can be easily analyzed with Frama-Clang? – José Luis Jan 14 '21 at 15:24

0 Answers0