4

I have installed the plugin Frama-Clang of Frama-c to parse C++ programs. However, I don't know how to correctly use it. I tried it with a very simple c++ program but failed. Here is the code of test.cpp:

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

I used the command frama-c test.cpp and got the following error:

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

Can someone tell me how to successfully parse it?

2
  • Any luck with this? I've been trying to do the same. I tried to give it include paths directly like this frama-c -cpp-extra-args="-I /usr/include/c++/7.2.0 -I /usr/include/x86_64-linux-gnu/c++/7.2.0 -I /usr/include/c++/7.2.0/backward -I /usr/local/include -I /usr/local/lib/clang/6.0.1/include -I /usr/include/x86_64-linux-gnu -I /usr/include" -cxx-c++stdlib-path="/usr/include/c++/7.2.0" hello.cpp but it core dumps with no useful information.
    – intheweeds
    Aug 1, 2018 at 16:53
  • 1
    @intheweeds no, it seems that frama-clang doesn't support the usage of STL.
    – M.J
    Aug 2, 2018 at 9:01

1 Answer 1

4

Your usage is correct: simply give it a .cpp file and it will try to parse it.

However, Hello World using <iostream> is not the best example due to the size and complexity of the STL: your program, after preprocessing, contains between 18k and 28k lines (depending on whether I use g++ or clang).

As indicated in the Frama-Clang webpage,

Frama-Clang is currently in an early stage of development. It is known to be incomplete (...)

Handling the STL is indeed one of the major difficulties in supporting C++, and currently under development.

If you try with a non-STL file, you should have better results. Part of the STL is supported, but there is no comprehensive list of which classes are and which aren't (as this is continually evolving).

For instance, the toy example below, which uses std::exception, templates and classes, is successfully parsed by Frama-Clang (despite a few warnings), simply by running 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;
  }
}

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.