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