frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-05-18T07:08:10Zhttps://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.https://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/2633Issue while installing Frama-c 25.0.02023-05-15T09:02:22ZOussamaH92Issue while installing Frama-c 25.0.0Hello everyone,
I'm a French student wanting to start using Frama-C.
When I was installing it following the step in Frama-C's website I get this error message after using
`opam install frama-c`
I was stuck with this error : `[ERROR]...Hello everyone,
I'm a French student wanting to start using Frama-C.
When I was installing it following the step in Frama-C's website I get this error message after using
`opam install frama-c`
I was stuck with this error : `[ERROR] The compilation of frama-c.25.0 failed at "make -j7".`
`
Error: Unbound module Cil_typesFile "src/plugins/aorai/promelaoutput.ml", line 26, characters 5-14:
26 | open Cil_types
^^^^^^^^^
Error: Unbound module Cil_types`
I've updated my GNU make version just before the install process with the command `brew install homebrew/core/make`
I hope someone can explain me how to get rid of this problem.
Thankshttps://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/2575[WP] Soundness issue when handling a pointer on a structure containing an array.2021-10-06T07:07:23ZAlexCid[WP] Soundness issue when handling a pointer on a structure containing an array.<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
Save the following code into a file called "error.c":
```C
#include <__fc_builtin.h>
struct slice {
int len;
char *buf;
};
int main() {
char b[4] = {0};
struct slice s = {.len = Frama_C_int_interval(2, 100000), .buf=b};
struct slice *p = &s;
//@ assert \valid_read(p->buf + (0..(p->len-1)));
return (int)p->buf[p->len-1];
}
```
Then analyse this code using the WP plugin with the command
`frama-c error.c -eva -wp -wp-rte -wp-prover alt-ergo`
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
### Expected behaviour
The assertion `//@ assert \valid_read(p->buf + (0..(p->len-1)));` does obviously not hold and should be rejected by WP.
<!--
Please explain here what is the expected behaviour.
-->
### Actual behaviour
The manually added assertion, as well as the RTE assertion generated by wp-rte, are proved by alt-ergo. Using a different prover (z3, cvc4) yields the same result.
<!--
Please explain here what is the actual (faulty) behaviour.
-->
### Contextual information
- Frama-C installation mode: docker
- Frama-C version: 23.1
- Plug-in used: Eva, WP
- OS name: Ubuntu
- OS version: 20.04
### Additional information (optional)
Handling a pointer on a structure containing the array is required to trigger the bug - a simple structure containing the array won't trigger it.
This bug can also be triggered in a slightly more complex setting, where the array access is done in a second function and the `assert` clause is replaced by an equivalent `requires` clause in the preconditions of that second function.
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->Allan BlanchardAllan Blanchard