frama-c [kernel] ошибка пользователя: недопустимый символ

Question

frama-c [kernel] ошибка пользователя: недопустимый символ

Когда я пытаюсь получить pdg кода, я получаю эту недопустимую ошибку символа без номеров строк для справки.
Кто-нибудь может подсказать, что означает эта ошибка? обратите внимание, что код компилируется и работает с g ++
Вопрос в том, как получить точный номер строки для этой ошибки.

команда выполнена:

frama-c -continue-annot-error -kernel-verbose 3  -no-annot -no-frama-c-stdlib -cpp-command " /usr/bin/g++  -iquote../../inc -std=c++11 fPIC -Wno-write-strings -Wno-narrowing  -gdwarf-3  -o test.o -c" -pdg -pdg-dot test -pdg-print test.cpp

Сообщение об ошибке :

[kernel] computing the AST
[kernel] parsing
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing /usr/local/share/frama-c/libc/__fc_builtin_for_normalization.i to Cabs
[kernel] Parsing /usr/local/share/frama-c/libc/__fc_builtin_for_normalization.i
[kernel] Converting /usr/local/share/frama-c/libc    /__fc_builtin_for_normalization.i from Cabs to CIL
[kernel] Parsing test.cpp (with preprocessing)
[kernel] Parsing /tmp/test.cppe1a338.i to Cabs
[kernel] Parsing /tmp/test.cppe1a338.i
/tmp/test.cppe1a338.i:1:[kernel] user error: Invalid symbol
[kernel] user error: stopping on file "test.cpp"that has errors.
[kernel] Frama-C aborted: invalid user input.

0

c++frama-c linux

Решение

Другие решения

Других решений пока нет …

Источник

Accepted Answer

Frama-C предназначен для анализа С код, а не C ++ код. Это два разных языка, и если вы не напишите простой C (с оговоркой, что некоторые конструкции, которые выглядят синтаксически похожими в обоих языках, фактически имеют разную семантику), Frama-C не сможет проанализировать test.cpp файл.

Кроме того, как упомянуто Энн в комментарии, -cpp-command вы дали неверно: вы спросили g++ чтобы предоставить двоичный файл, тогда как Frama-C ожидает предварительно обработанный C. На самом деле, строка ошибки упоминается в вашем журнале: /tmp/test.cppe1a338.i:1:, но это бессмысленно, так как test.cppe1a338 это бинарный файл С соответствующим -cpp-command (например, тот, который Frama-C дает вам по умолчанию), Frama-C найдет #line аннотации, которые позволят ему сообщать о любой ошибке в соответствующем месте исходного файла вместо промежуточного результата.

2