frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2023-03-12T22:26:44Zhttps://git.frama-c.com/pub/frama-c/-/issues/2642Installing Frama-C with opam fails2023-03-12T22:26:44ZHugo GimbertInstalling Frama-C with opam failsHello,
several students of mine were struggling today to install frama-c on their Ubuntu.
Can someone provide some feedback on the following error.
Example on Ubuntu 20.04, standard installation.
```
sudo apt-get remove opam
rm -fr ~...Hello,
several students of mine were struggling today to install frama-c on their Ubuntu.
Can someone provide some feedback on the following error.
Example on Ubuntu 20.04, standard installation.
```
sudo apt-get remove opam
rm -fr ~/.opam
sudo apt-get install opam
opam init
eval $(opam env)
opam install frama-c
```
leads to the following error
```
#=== ERROR while compiling alt-ergo-lib.2.4.2 =================================#
# context 2.0.5 | linux/x86_64 | ocaml-system.4.08.1 | https://opam.ocaml.org#0cd336b3
# path ~/.opam/default/.opam-switch/build/alt-ergo-lib.2.4.2
# command ~/.opam/opam-init/hooks/sandbox.sh build dune build -p alt-ergo-lib -j 1
# exit-code 1
# env-file ~/.opam/log/alt-ergo-lib-66410-e6f851.env
# output-file ~/.opam/log/alt-ergo-lib-66410-e6f851.out
### output ###
# 639 | [@ocaml.ppwarning "TODO: detect when there are no changes "]
# [...]
# Warning 22: TODO: detect when there are no changes
# (cd _build/default && /usr/bin/ocamlc.opt -w -40 -bin-annot -g -bin-annot -I src/lib/.AltErgoLib.objs/byte -I /home/yussef/.opam/default/lib/ocplib-simplex -I /home/yussef/.opam/default/lib/seq -I /home/yussef/.opam/default/lib/stdlib-shims -I /home/yussef/.opam/default/lib/zarith -no-alias-deps -open AltErgoLib -o src/lib/.AltErgoLib.objs/byte/altErgoLib__Parsed.cmi -c -intf src/lib/structur[...]
# File "src/lib/structures/parsed.mli", line 32, characters 17-24:
# 32 | | ConstReal of Num.num
# ^^^^^^^
# Error: Unbound module Num
# (cd _build/default && /usr/bin/ocamlc.opt -w -40 -bin-annot -g -bin-annot -I src/lib/.AltErgoLib.objs/byte -I /home/yussef/.opam/default/lib/ocplib-simplex -I /home/yussef/.opam/default/lib/seq -I /home/yussef/.opam/default/lib/stdlib-shims -I /home/yussef/.opam/default/lib/zarith -no-alias-deps -open AltErgoLib -o src/lib/.AltErgoLib.objs/byte/altErgoLib__Typed.cmi -c -intf src/lib/structure[...]
# File "src/lib/structures/typed.mli", line 58, characters 13-20:
# 58 | | Treal of Num.num (** Real constant. *)
# ^^^^^^^
# Error: Unbound module Num
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
┌─ The following actions failed
│ λ build alt-ergo-lib 2.4.2
└─
```Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2560[Plug-in wp] 96-bits floats2021-10-06T07:52:08Zarun-babu[Plug-in wp] 96-bits floatsFeature request, as I get:
```
[kernel] Parsing file.c (with preprocessing)
[kernel] Plug-in wp aborted: unimplemented feature.
You may send a feature request at https://git.frama-c.com/pub/frama-c/issues with:
'[Plug-in wp] 96-bits...Feature request, as I get:
```
[kernel] Parsing file.c (with preprocessing)
[kernel] Plug-in wp aborted: unimplemented feature.
You may send a feature request at https://git.frama-c.com/pub/frama-c/issues with:
'[Plug-in wp] 96-bits floats'.
```
I am not sure what this means though!https://git.frama-c.com/pub/frama-c/-/issues/2552Errors when trying to analyze programs including MSVC headers2021-05-18T07:08:10Zmarce9Errors when trying to analyze programs including MSVC headersHi,
We are trying to slice the simple program tst3.cpp (included [tst3.cpp](/uploads/0d081c0cc1fd06079866f667b066e4ff/tst3.cpp)).
The execution command is:
_frama-c tst3.cpp -slice-calls g -slicing-level 1 -slicing-keep-annotations -then...Hi,
We are trying to slice the simple program tst3.cpp (included [tst3.cpp](/uploads/0d081c0cc1fd06079866f667b066e4ff/tst3.cpp)).
The execution command is:
_frama-c tst3.cpp -slice-calls g -slicing-level 1 -slicing-keep-annotations -then-on 'Slicing export' -print -ocode output.cpp_
The slicing succeeds and the output is:
![tst3_no_includes_execution_success](/uploads/769b95a3290e6510fb69486ca4030401/tst3_no_includes_execution_success.PNG)
However, when adding 2 includes <stdio.h> & <string.h> the slicing fails with the following output:
![tst3_with_includes_execution_failure](/uploads/6797417f8fe26d2a127995cff63f6782/tst3_with_includes_execution_failure.PNG)
Moreover, we keep facing failures when trying to slice simple programs with the MinGW's GCC compiler and headers. For example, for tried execution the following command:
**_frama-c -cpp-command 'x86_64-w64-mingw32-gcc -C -E -I /usr/x86_64-w64-mingw32/include' -cpp-frama-c-compliant tst3.cpp -slice-calls g -slicing-level 1 -slicing-keep-annotations -then-on 'Slicing export' -print -ocode output.cpp_**
The errors range from "invalid user input" on header files, to incompatible arch mode (32, 64 bit).
Hope to receive help with the right way of executing things, including the right commands with the right parameters, how to use MinGW in order to slice visual-C++ code (MSVC), etc.