search

Frama-C / Frama-C-snapshot

Release snapshots of the Frama-C platform for source code analysis
http://frama-c.com
169 stars 38 forks source link

frama-clang failed to install #45

Closed harshitalpha closed 3 years ago

harshitalpha commented 3 years ago

Hi all, I ran into the issue while installing frama-clang I ran ./configure and get the following output

checking for frama-c-gui... yes
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 the compiler supports GNU C++... yes
checking whether g++ accepts -g... yes
checking for g++ option to enable C++11 features... none needed
checking for camlp5o... no
configure: WARNING: camlp5o not found.
configure: WARNING: frama_clang disabled because camlp5o missing.
checking for clang... clang
checking for clang++... clang++
checking for llvm-config... no
checking for llvm-config-12... no
checking for llvm-config-11... no
checking for llvm-config-10... llvm-config-10
configure: frama_clang: no
configure: creating ./config.status
config.status: creating ./Makefile.config

I guess ./configure run with no error, then i try to run make command as the documentation said and i ran in to the following error

Generating   .Makefile.plugin.generated
Ocamlc       gen_ast
ocamlfind: /usr/lib/ocaml/ld.conf: No such file or directory
make: *** No rule to make target 'gen_ast', needed by 'intermediate_format_parser.ml'.  Stop.

Please help me to resolve this error. I have also refereed to the #10 issue but it didn't help me a lot.

vprevosto commented 3 years ago

Thanks for your report, but please note that the primary issue tracker for Frama-C now has moved to https://git.frama-c.com/pub/frama-c/issues (you can log in into git.frama-c.com with your github account). Moreover, Frama-Clang also gained its own personal repo at https://git.frama-c.com/pub/frama-clang, so that Frama-Clang-specific issues can be reported at https://git.frama-c.com/pub/frama-clang/issues.

Now, back to the issue itself: it is a bit unfortunate, but the configure scripts of Frama-C plugins will not exit with an error if the plug-in cannot be enabled (technically, this is due to the fact that most of the script is shared between internal plugins and external ones. For internal plugins, the inability to compile a single plug-in should not prevent compiling the entire platform, but admittedly if you're trying to compile a single external plug-in, you want to be warned explicitly if something goes wrong at configure stage). What is important is this line in the log:

configure: frama_clang: no

This means that frama_clang cannot be compiled on your machine. Going back in the log gives you the root cause:

configure: WARNING: camlp5o not found.
configure: WARNING: frama_clang disabled because camlp5o missing.

Frama-Clang requires camlp5 for its compilation. If you're using opam, this should only be a matter of opam install camlp5

harshitalpha commented 3 years ago

Thanks for letting me know about Frama-C personal repository. I have tried running this command opam install camlp5 but it is giving error 

[WARNING] System file /usr/bin/ocamlc, which package ocaml-system.4.08.1
          depends upon, no longer exists.
          The package will need to either be removed, or reinstalled. You may
          need to restore its system dependencies for the latter.
[ERROR] Package conflict!
  * Missing dependency:
    - ocaml-system
    unmet availability conditions, e.g. 'sys-ocaml-version = "4.13.1"'

No solution found, exiting

how can i update sys-ocaml-version to 4.13? Please let me know about this Thanks and Regards Harshit Singhal

vprevosto commented 3 years ago

The error message comes likely from the fact that the version of OCaml that is installed by your OS' package manager has changed since you've installed opam. I'd argue that the easiest way to use opam is not to depend on the version of OCaml that comes with your system and use a purely opam-managed switch, e.g. opam switch create 4.12.1. If you only use opam for compiling Frama-C and Frama-Clang, you then just need to reinstall it on the new switch: opam install frama-c camlp5. If you have other OCaml libraries and applications managed through opam, before the switch do opam switch export my-packages.export, and after the switch do opam switch import my-packages.import (don't forget to opam install camlp5 afterwards, though).

harshitalpha commented 3 years ago

Hi @vprevosto Thanks for replying, This solution work, make command is running now but now it gave following error

Generating   .Makefile.plugin.generated
Ocamlc       gen_ast
Generating   intermediate AST
Generating   META.frama-c-frama_clang
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       reorder_defs.cmi
Ocamlc       reorder_defs.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
File "convert_acsl.ml", line 596, characters 31-47:
596 | let convert_pred_tp env ?(kind=Cil_types.Assert) p =
                                     ^^^^^^^^^^^^^^^^
Error: Unbound constructor Cil_types.Assert
Hint: Did you mean AAssert?
make: *** [/home/harshit/.opam/4.13.1/share/frama-c/Makefile.generic:78: convert_acsl.cmo] Error 2

Please let me know the solution Thanks and regards Harshit Singhal

vprevosto commented 3 years ago

Which version of Frama-C have you installed, and which version of Frama-Clang are you are trying to compile? There are strong dependencies between the two.

harshitalpha commented 3 years ago

Frama-C version :- 22.0(Titanium) Frama-clang vetsion :- 0.0.11

vprevosto commented 3 years ago

These are not compatible. As mentioned on Frama-Clang's home page, you can either compile Frama-Clang 0.0.11 against Frama-C 23.x or Frama-Clang 0.0.10 against Frama-C 22.x.

harshitalpha commented 3 years ago

Hi, Sorry to bother you again, I run the make command and got this error

make[1]: Entering directory '/home/harshit/Downloads/frama-clang-0.0.10'
Linking      bin/framaCIRGen
/usr/bin/ld: cannot find -lclang-cpp
collect2: error: ld returned 1 exit status
make[1]: *** [Makefile.clang:92: bin/framaCIRGen] Error 1
make[1]: Leaving directory '/home/harshit/Downloads/frama-clang-0.0.10'
make: *** [Makefile:107: all] Error 2

I know this is not the issue with frama-c, but when i look up locate clang-cpp i found its path Please let me know the solution. Thanks and Regard Harshit Singhal

vprevosto commented 3 years ago

Could you run VERBOSEMAKE=yes make and post the logs, as well as the location of clang-cpp?

harshitalpha commented 3 years ago

Output of VERBOSEMAKE=yes make

MAKEFLAGS="" MAKEFLAGS="" make PLUGIN_DIR=. FRAMAC_SHARE=/home/harshit/.opam/4.13.1/share/frama-c -f ./Makefile.clang default
make[1]: Entering directory '/home/harshit/Downloads/frama-clang-0.0.10'
g++ -L/usr/lib/llvm-10/lib  -o bin/framaCIRGen  \
               ./Clang_utils.o ./intermediate_format.o ./ACSLComment.o ./ACSLLogicType.o ./ACSLTermOrPredicate.o ./ACSLLoopAnnotation.o ./ACSLStatementAnnotation.o ./ACSLGlobalAnnotation.o ./ACSLCodeAnnotation.o ./ACSLFunctionContract.o ./ACSLComponent.o ./ACSLLexer.o ./ACSLParser.o ./ACSLToken.o ./DescentParse.o ./RTTITable.o ./VisitTable.o ./ClangVisitor.o ./FramaCIRGen.o -lclang-cpp -lLLVM-10  -L/usr/lib/llvm-10/lib 
/usr/bin/ld: cannot find -lclang-cpp
collect2: error: ld returned 1 exit status
make[1]: *** [Makefile.clang:92: bin/framaCIRGen] Error 1
make[1]: Leaving directory '/home/harshit/Downloads/frama-clang-0.0.10'
make: *** [Makefile:107: all] Error 2

Location of clang-cpp

/usr/bin/clang-cpp-10
/usr/lib/libclang-cpp.so
/usr/lib/llvm-10/bin/clang-cpp
/usr/lib/llvm-10/lib/libclang-cpp.so.10
/usr/lib/x86_64-linux-gnu/libclang-cpp.so.10
/usr/share/doc/libclang-cpp10
/usr/share/doc/libclang-cpp10/NEWS.Debian.gz
/usr/share/doc/libclang-cpp10/changelog.Debian.gz
/usr/share/doc/libclang-cpp10/copyright
/var/lib/dpkg/info/libclang-cpp10.list
/var/lib/dpkg/info/libclang-cpp10.md5sums
/var/lib/dpkg/info/libclang-cpp10.shlibs
/var/lib/dpkg/info/libclang-cpp10.triggers
harshitalpha commented 3 years ago

Hey, Do we have any solution for the above problem?

maroneze commented 3 years ago

Hello,

I believe so far we haven't been able to replicate your problem to know what to suggest.

I tried preparing a Dockerfile for Alpine to see if I could reproduce it on a clean install, but I couldn't; the commands below compile and install Frama-Clang without errors (note that this Dockerfile is not optimal at all; more like a quick hack to get Frama-Clang to compile and install):

FROM ocaml/opam:alpine-3.13-ocaml-4.13

RUN sudo apk update
RUN sudo apk add autoconf clang llvm-dev clang-dev
RUN opam depext frama-c camlp5
RUN opam install frama-c camlp5
RUN wget https://frama-c.com/download/frama-clang-0.0.10.tar.gz
RUN tar xvf frama-clang-0.0.10.tar.gz
WORKDIR /home/opam/frama-clang-0.0.10
RUN eval $(opam env) && ./configure
RUN eval $(opam env) && make DEVELOPMENT=no -j
RUN eval $(opam env) && sudo make install

Without knowing more details about your system (distribution, version, architecture), I think it'll be hard for us to reproduce it.

harshitalpha commented 3 years ago

Hi, I have tried installing everything from scratch. Here are steps i followed. At first i have installed frama-c version 23.1 (Vanadium) Then i have downloaded frama-clang version 0.0.11 which is compatible with frama-c version. I have also installed clang-12 which is required for frama-clang version 0.0.11 by following command

sudo apt install clang-12 --install-suggests

Then i run configuration file, which gave following output

checking for frama-c-gui... yes
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 the compiler supports GNU C++... yes
checking whether g++ accepts -g... yes
checking for g++ option to enable C++11 features... none needed
checking for camlp5o... yes
checking for clang... no
checking for clang-12... clang-12
checking for clang++... no
checking for clang++-12... clang++-12
checking for llvm-config... no
checking for llvm-config-12... llvm-config-12
checking LLVM version... 12.0.0: Good
configure: frama_clang: yes
configure: creating ./config.status
config.status: creating ./Makefile.config

Then i run make command which is giving me following error

Generating   .Makefile.plugin.generated
Ocamlc       gen_ast
Generating   intermediate AST
Generating   META.frama-c-frama_clang
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       reorder_defs.cmi
Ocamlc       reorder_defs.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
Ocamlopt     intermediate_format_parser.cmx
Ocamlopt     frama_Clang_option.cmx
Ocamlopt     fclang_datatype.cmx
Ocamlopt     reorder_defs.cmx
Ocamlopt     cxx_utils.cmx
Ocamlopt     mangling.cmx
Ocamlopt     convert_env.cmx
Ocamlopt     convert_acsl.cmx
Ocamlopt     generate_spec.cmx
Ocamlopt     class.cmx
Ocamlopt     convert.cmx
Ocamlopt     convert_link.cmx
Ocamlopt     frama_Clang_register.cmx
Packing      top/Frama_Clang.cmx
Packing      top/Frama_Clang.cmxs
make[1]: Entering directory '/home/harshit/Downloads/frama-clang-0.0.11'
Compiling    Clang_utils.cpp
In file included from Clang_utils.cpp:25:
Clang_utils.h:43:10: fatal error: clang/Basic/Version.h: No such file or directory
   43 | #include "clang/Basic/Version.h"
      |          ^~~~~~~~~~~~~~~~~~~~~~~
compilation terminated.
make[1]: *** [Makefile.clang:96: Clang_utils.o] Error 1
make[1]: Leaving directory '/home/harshit/Downloads/frama-clang-0.0.11'
make: *** [Makefile:103: all] Error 2

One thing i want to mention is that clang is installed by name clang-12, that is clang is not working but clang-12 is. I have also tried creating alias with name clang which point to clang-12, but it is still giving same error.

Please let me know what i am missing Thanks and Regards Harshit Singhal

harshitalpha commented 3 years ago

Hi, Solution of above problem is to install libclang-12-dev using following command

sudo apt install libclang-12-dev --install-suggests
harshitalpha commented 3 years ago

Hi, There is same problem as before while make command

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
/usr/bin/ld: cannot find -lclang-cpp
collect2: error: ld returned 1 exit status
make[1]: *** [Makefile.clang:84: bin/framaCIRGen] Error 1
make[1]: Leaving directory '/home/harshit/Downloads/frama-clang-0.0.11'
make: *** [Makefile:103: all] Error 2
maroneze commented 3 years ago

Thanks for the update, but you still didn't tell us which system are you using: Debian? Ubuntu? From the package name I suppose it's Debian, but can you tell the version (cat /etc/debian_version), so that I can try it in a Docker to reproduce it?

harshitalpha commented 3 years ago

I am using ubuntu 20.04 LTS. I guess its debian, and output of the command cat /etc/debian_version is bullseye/sid

maroneze commented 3 years ago

Thanks. I am able to reproduce it using Docker.

I actually tried with clang-10 (the default version installed when I did sudo apt install llvm-dev libclang-dev clang -y), but I also had the "cannot find -lclang-cpp" issue in the end.

I was able to fix it by creating a symbolic link to /usr/lib/llvm-10/lib/libclang-cpp.so, from /usr/lib/llvm-10/lib/libclang-cpp.so.10 (which did exist), as follows:

sudo ln -s /usr/lib/llvm-10/lib/libclang-cpp.so.10 /usr/lib/llvm-10/lib/libclang-cpp.so

However, this is not the right solution: the proper fix is to install package libclang-cpp10-dev (or, in your case, libclang-cpp12-dev), which does seem to provide the required file. I found it out using apt-file find libclang-cpp.so. Of course, there is no libclang-cpp-dev package, which would make sense considering the naming of the other packages; for some reason, this specific package only has numbered version names, so you have to manually find the right one and install it.

The profusion of different packages and dependencies (which varies with each Linux distribution) makes it very hard to provide the full list of dependencies and check all of them during configure. We'll see if we can perform extra checks for future users.

maroneze commented 3 years ago

Just in case, here's the (hackish, unoptimized) Dockerfile I used to test, and which allowed getting Frama-Clang installed:

FROM ocaml/opam:ubuntu-20.04-ocaml-4.13

RUN sudo apt update
RUN sudo apt install autoconf -y
RUN opam depext frama-c camlp5
RUN opam install --deps-only frama-c
RUN opam install why3.1.4.0 camlp5
RUN git clone https://git.frama-c.com/pub/frama-c.git
WORKDIR /home/opam/frama-c
RUN autoconf
RUN eval $(opam env) && ./configure
RUN eval $(opam env) && make DEVELOPMENT=no -j
RUN sudo make install
WORKDIR /home/opam
RUN sudo apt install wget
RUN wget https://frama-c.com/download/frama-clang-0.0.11.tar.gz
RUN tar xvf frama-clang-0.0.11.tar.gz
WORKDIR /home/opam/frama-clang-0.0.11
RUN sudo apt install llvm-dev libclang-dev libclang-cpp10-dev clang -y
RUN eval $(opam env) && ./configure
RUN eval $(opam env) && make DEVELOPMENT=no -j
RUN eval $(opam env) && sudo make install
harshitalpha commented 3 years ago

Thanks you, It worked. I am using libclang-cpp-12. Thanks for helping me a lot.

harshitalpha commented 3 years ago

Hi, Since frama-clang is installed, i tried to test it with following command 

frama-c -cpp-extra-args="-Iinc" -wp testing.cpp

and the testing.cpp file is fairly simple file.

#include<bits/stdc++.h>
using namespace std;
int main(){
    cout<<"Hello World"<<endl;
    return 0;
}

but it is giving me error

[kernel] Parsing testing.cpp (external front-end)
In file included from /home/harshit/Desktop/testing.cpp:1:
In file included from /usr/lib/gcc/x86_64-linux-gnu/9/../../../../include/x86_64-linux-gnu/c++/9/bits/stdc++.h:35:
In file included from /usr/lib/gcc/x86_64-linux-gnu/9/../../../../include/c++/9/cctype:41:
In file included from /usr/lib/gcc/x86_64-linux-gnu/9/../../../../include/x86_64-linux-gnu/c++/9/bits/c++config.h:524:
/usr/lib/gcc/x86_64-linux-gnu/9/../../../../include/x86_64-linux-gnu/c++/9/bits/os_defines.h:44:5: error: function-like macro '__GLIBC_PREREQ' is not defined
#if __GLIBC_PREREQ(2,15) && defined(_GNU_SOURCE)
    ^
In file included from /home/harshit/Desktop/testing.cpp:1:
In file included from /usr/lib/gcc/x86_64-linux-gnu/9/../../../../include/x86_64-linux-gnu/c++/9/bits/stdc++.h:41:
/usr/lib/gcc/x86_64-linux-gnu/9/../../../../include/c++/9/cmath:45:15: fatal error: 'math.h' file not found
#include_next <math.h>
              ^~~~~~~~
code generation aborted due to compilation errors
[kernel] User Error: Failed to parse C++ file. See Clang messages for more information
[kernel] User Error: stopping on file "testing.cpp" that has errors.
[kernel] Frama-C aborted: invalid user input.

It is giving invalid user input. Do i have to give the file in different format It also says not found math.h, but it compiled successfully. Do i have to link any header?

Thanks and Regards Harshit Singhal

maroneze commented 3 years ago

The new problem you are having is related to parsing C++ files with Frama-Clang, not with its installation. There are limitations concerning the C++ standard library, as well as command-line options which could help address it (some options are mentioned in Frama-Clang's README.md), such as:

-cxx-c++stdlib-path <path>: specifies where to look for standard C++ library headers (default is the path to Frama-Clang headers, which are very incomplete)

I think it's better to deal with it in an issue in the new Frama-Clang Gitlab repository, at https://git.frama-c.com/pub/frama-clang/-/issues/1. I created a new issue for this parsing problem, and copied your code and error message. You can use your Github account to log into our public Gitlab repository and follow the issue there.

harshitalpha commented 3 years ago

Thank you sir for helping me, I will followup this parsing issue at Frama-Clang Gitlab repository.