Я установил плагин Frama-Clang из Frama-c для разбора программ на 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
файл, и он попытается разобрать его.
Тем не менее, Hello World, используя <iostream>
Это не лучший пример из-за размера и сложности STL: ваша программа после предварительной обработки содержит от 18 до 28 тыс. строк (в зависимости от того, использую ли я g++
или же clang
).
Как указано на веб-странице Frama-Clang,
Frama-Clang в настоящее время находится на ранней стадии разработки. Известно, что оно неполное (…)
Обработка STL действительно является одной из основных трудностей в поддержке C ++ и в настоящее время находится в стадии разработки.
Если вы попытаетесь использовать файл, отличный от STL, у вас будут лучшие результаты. Часть STL поддерживается, но нет исчерпывающего списка, какие классы есть, а какие нет (так как это постоянно развивается).
Например, пример игрушки ниже, который использует std::exception
, шаблоны и классы, успешно анализируется Frama-Clang (несмотря на несколько предупреждений), просто запустив 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;
}
}
Других решений пока нет …