Ошибки при использовании плагина Frama-Clang

Учитывая, что плагин https://frama-c.com/frama-clang.html рассматривается на «ранних этапах» разработки, возможно, мне пока не повезло. Но интересно, если кто-то еще столкнулся с такой проблемой:

navarre@navarre-t400:~/code/c$ frama-c max.cpp
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing max.cpp (external front-end)
: CommandLine Error: Option 'asm-macro-max-nesting-depth' registered more than once!
LLVM ERROR: inconsistency in registered CommandLine options
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
[kernel] user error: stopping on file "max.cpp" that has errors.
[kernel] Frama-C aborted: invalid user input.

Для записи содержимое max.cpp выглядит следующим образом:

int s(int i) {
return i;
}

Любая помощь будет оценена. Даже просто указав мне на таинственные «Clang messages», которые вывод ошибок предлагает мне увидеть!

РЕДАКТИРОВАТЬ: я, вероятно, должен добавить, что я на Ubuntu и у меня было достаточно времени, чтобы сборка заработала, по-видимому, из-за конфликта в clang 3.9 в репозиториях Ubuntu против PPA. В конце концов я получил плагин для сборки, и теперь я застрял здесь.

EDIT2: мне удалось отредактировать исходный код frama_Clang_register.ml, чтобы увидеть выполняемую команду. Вот этот:

framaCIRGen  -target i386-unknown-linux-gnu -D__FC_MACHDEP_X86_32 -std=c++11 -nostdinc -I /home/navarre/.opam/system/share/frama-c/frama-clang/libc++ -I /home/navarre/.opam/system/share/frama-c/libc -I /home/navarre/.opam/system/share/frama-c --stop-annot-error

И вот теперь возникает вопрос: «что не так с« framaCIRGen ». Сначала я заметил, что получаю оскорбительную ошибку, даже если я просто запускаю framaCIRGen и ничего больше. Интересно.

И затем я замечаю, что оскорбительная вещь (asm-macro-max-nesting-глубина) не присутствует в исходном файле для framaCIRGen, но является в скомпилированном бинарнике!

Это также не в выходных данных cpp, так что, должно быть, он получил через связанную библиотеку?

navarre@navarre-t400:~/Downloads/frama-clang-0.0.3$ cpp -std=c++11 ./FramaCIRGen.cpp -I/usr/lib/llvm-4.0/include   -D_GNU_SOURCE -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -g -fPIC -D__STDC_CONSTANT_MACROS -D__STDC_LIMIT_MACROS | grep asm-macro-max-nesting-depth | wc
0       0       0

РЕДАКТИРОВАТЬ:

Вот вывод из ./configure:

checking for frama-c-gui... no
checking for Makefile.config.in... yes
frama_clang... yes
checking for g++... g++
checking whether the C++ compiler works... yes
checking for C++ compiler default output file name... a.out
checking for suffix of executables...
checking whether we are cross compiling... no
checking for suffix of object files... o
checking whether we are using the GNU C++ compiler... yes
checking whether g++ accepts -g... yes
checking for camlp4o... yes
checking for clang... no
checking for clang-3.8... no
checking for clang-3.9... no
checking for clang-4.0... clang-4.0
checking for clang++... no
checking for clang++-3.8... no
checking for clang++-3.9... no
checking for clang++-4.0... clang++-4.0
checking for llvm-config... no
checking for llvm-config-3.8... no
checking for llvm-config-3.9... no
checking for llvm-config-4.0... llvm-config-4.0
checking LLVM version... 4.0.1: Good
configure: frama_clang: yes
configure: creating ./config.status
config.status: creating ./Makefile.config

А вот и вывод команды make (с переменной окружения VERBOSEMAKE = yes).

Generating   .Makefile.plugin.generated
Generating   intermediate AST
Generating   top/Frama_Clang.mli
Ocamldep     ./.depend
Ocamlc       intermediate_format.cmi
Ocamlc       intermediate_format_parser.cmi
Ocamlc       intermediate_format_parser.cmo
Ocamlc       frama_Clang_option.cmi
Ocamlc       frama_Clang_option.cmo
Ocamlc       fclang_datatype.cmi
Ocamlc       fclang_datatype.cmo
Ocamlc       cxx_utils.cmi
Ocamlc       cxx_utils.cmo
Ocamlc       mangling.cmi
Ocamlc       mangling.cmo
Ocamlc       convert_env.cmi
Ocamlc       convert_env.cmo
Ocamlc       convert_acsl.cmi
Ocamlc       convert_acsl.cmo
Ocamlc       generate_spec.cmi
Ocamlc       generate_spec.cmo
Ocamlc       class.cmi
Ocamlc       class.cmo
Ocamlc       convert.cmi
Ocamlc       convert.cmo
Ocamlc       convert_link.cmi
Ocamlc       convert_link.cmo
Ocamlc       frama_Clang_register.cmi
Ocamlc       frama_Clang_register.cmo
Ocamlc       Frama_Clang.cmi
Generating   top/Frama_Clang.cmi
Packing      top/Frama_Clang.cmo
findlib: [WARNING] Interface Frama_Clang.cmi occurs in several directories: /home/navarre/.opam/system/lib/frama-c/plugins, .
Ocamlopt     intermediate_format_parser.cmx
findlib: [WARNING] Interface Frama_Clang.cmi occurs in several directories: /home/navarre/.opam/system/lib/frama-c/plugins, .
Ocamlopt     frama_Clang_option.cmx
findlib: [WARNING] Interface Frama_Clang.cmi occurs in several directories: /home/navarre/.opam/system/lib/frama-c/plugins, .
Ocamlopt     fclang_datatype.cmx
findlib: [WARNING] Interface Frama_Clang.cmi occurs in several directories: /home/navarre/.opam/system/lib/frama-c/plugins, .
Ocamlopt     cxx_utils.cmx
findlib: [WARNING] Interface Frama_Clang.cmi occurs in several directories: /home/navarre/.opam/system/lib/frama-c/plugins, .
Ocamlopt     mangling.cmx
findlib: [WARNING] Interface Frama_Clang.cmi occurs in several directories: /home/navarre/.opam/system/lib/frama-c/plugins, .
Ocamlopt     convert_env.cmx
findlib: [WARNING] Interface Frama_Clang.cmi occurs in several directories: /home/navarre/.opam/system/lib/frama-c/plugins, .
Ocamlopt     convert_acsl.cmx
findlib: [WARNING] Interface Frama_Clang.cmi occurs in several directories: /home/navarre/.opam/system/lib/frama-c/plugins, .
Ocamlopt     generate_spec.cmx
findlib: [WARNING] Interface Frama_Clang.cmi occurs in several directories: /home/navarre/.opam/system/lib/frama-c/plugins, .
Ocamlopt     class.cmx
findlib: [WARNING] Interface Frama_Clang.cmi occurs in several directories: /home/navarre/.opam/system/lib/frama-c/plugins, .
Ocamlopt     convert.cmx
findlib: [WARNING] Interface Frama_Clang.cmi occurs in several directories: /home/navarre/.opam/system/lib/frama-c/plugins, .
Ocamlopt     convert_link.cmx
findlib: [WARNING] Interface Frama_Clang.cmi occurs in several directories: /home/navarre/.opam/system/lib/frama-c/plugins, .
Ocamlopt     frama_Clang_register.cmx
findlib: [WARNING] Interface Frama_Clang.cmi occurs in several directories: /home/navarre/.opam/system/lib/frama-c/plugins, .
Packing      top/Frama_Clang.cmx
findlib: [WARNING] Interface Frama_Clang.cmi occurs in several directories: /home/navarre/.opam/system/lib/frama-c/plugins, .
Packing      top/Frama_Clang.cmxs
findlib: [WARNING] Interface Frama_Clang.cmi occurs in several directories: /home/navarre/.opam/system/lib/frama-c/plugins, .
make[1]: Entering directory `/home/navarre/Downloads/frama-clang-0.0.3'
Compiling    Clang_utils.cpp
Compiling    intermediate_format.c
Compiling    ACSLComment.cpp
Compiling    ACSLLogicType.cpp
Compiling    ACSLTermOrPredicate.cpp
Compiling    ACSLLoopAnnotation.cpp
Compiling    ACSLStatementAnnotation.cpp
Compiling    ACSLGlobalAnnotation.cpp
Compiling    ACSLCodeAnnotation.cpp
Compiling    ACSLFunctionContract.cpp
Compiling    ACSLComponent.cpp
Compiling    ACSLLexer.cpp
Compiling    ACSLParser.cpp
Compiling    ACSLToken.cpp
Compiling    DescentParse.cpp
Compiling    RTTITable.cpp
Compiling    VisitTable.cpp
Compiling    ClangVisitor.cpp
Compiling    FramaCIRGen.cpp
Linking      bin/framaCIRGen
make[1]: Leaving directory `/home/navarre/Downloads/frama-clang-0.0.3'

И вот флаг отладки, предложенный в комментариях:

navarre@navarre-t400:~/code/c$ frama-c max.cpp -fclang-msg-key clang
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing max.cpp (external front-end)
[fclang:clang] Clang command is framaCIRGen  -target i386-unknown-linux-gnu -D__FC_MACHDEP_X86_32 -std=c++11 -nostdinc -I /home/navarre/.opam/system/share/frama-c/frama-clang/libc++ -I /home/navarre/.opam/system/share/frama-c/libc -I /home/navarre/.opam/system/share/frama-c --stop-annot-error -v  max.cpp -o /tmp/clang_ast8f7187ast
: CommandLine Error: Option 'asm-macro-max-nesting-depth' registered more than once!
LLVM ERROR: inconsistency in registered CommandLine options
framaCIRGen  -target i386-unknown-linux-gnu -D__FC_MACHDEP_X86_32 -std=c++11 -nostdinc -I /home/navarre/.opam/system/share/frama-c/frama-clang/libc++ -I /home/navarre/.opam/system/share/frama-c/libc -I /home/navarre/.opam/system/share/frama-c --stop-annot-error -v  max.cpp -o /tmp/clang_ast8f7187ast[kernel] user error: Failed to parse C++ file. See Clang messages for more information
[kernel] user error: stopping on file "max.cpp" that has errors.
[kernel] Frama-C aborted: invalid user input.
[extlib] Debug: not removing file /tmp/clang_ast8f7187ast