frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2022-03-25T05:14:24Zhttps://git.frama-c.com/pub/frama-c/-/issues/2606How to downgrade Frama-C2022-03-25T05:14:24ZJaeD-ShinHow to downgrade Frama-Cmy frama-c and E-ACSL's version is 24.0+dev,
but E-ACSL's version in manual is 23.i.
so I want to downgrade frama-c and E-ACSL.
How to downgrade Frama-C and E-ACSL?my frama-c and E-ACSL's version is 24.0+dev,
but E-ACSL's version in manual is 23.i.
so I want to downgrade frama-c and E-ACSL.
How to downgrade Frama-C and E-ACSL?https://git.frama-c.com/pub/frama-c/-/issues/2605Segmentation fault of e-acsl(feat.E-acsl user manual)2022-05-12T12:25:23ZJaeD-ShinSegmentation fault of e-acsl(feat.E-acsl user manual)I followed the user's manual, but the following result does not come out and 'Segmentation fault (core dumped)' occurs.
I don't know what is the problem.
(URL: https://frama-c.com/fc-plugins/e-acsl.html)
* **expected result**
![expecte...I followed the user's manual, but the following result does not come out and 'Segmentation fault (core dumped)' occurs.
I don't know what is the problem.
(URL: https://frama-c.com/fc-plugins/e-acsl.html)
* **expected result**
![expected_result](/uploads/ebc7591b516b32a3631380e8abdfaaaa/expected_result.png)
* **my result**
```
jaeyoung@jaeyoung-VirtualBox:~/Documents$ e-acsl-gcc.sh -c -omonitored_first.i first.i
+ /home/jaeyoung/.opam/default/bin/frama-c -remove-unused-specified-functions -machdep gcc_x86_64 '-cpp-extra-args= -std=c99 -D_DEFAULT_SOURCE -D__NO_CTYPE -D__FC_MACHDEP_X86_64 ' -no-frama-c-stdlib first.i -e-acsl -e-acsl-share=/home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl -then-last -print -ocode monitored_first.i
[kernel] Parsing first.i (no preprocessing)
[e-acsl] beginning translation.
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] /usr/include/x86_64-linux-gnu/bits/thread-shared-types.h:92: Warning:
unnamed fields are a C11 extension (use -c11 to avoid this warning)
[e-acsl] translation done in project "e-acsl".
+ gcc -std=c99 -m64 -g -O2 -fno-builtin -fno-merge-constants -Wall -Wno-long-long -Wno-attributes -Wno-nonnull -Wno-undef -Wno-unused -Wno-unused-function -Wno-unused-result -Wno-unused-value -Wno-unused-function -Wno-unused-variable -Wno-unused-but-set-variable -Wno-implicit-function-declaration -Wno-empty-body first.i -o a.out
+ gcc -DE_ACSL_SEGMENT_MMODEL -std=c99 -m64 -g -O2 -fno-builtin -fno-merge-constants -Wall -Wno-long-long -Wno-attributes -Wno-nonnull -Wno-undef -Wno-unused -Wno-unused-function -Wno-unused-result -Wno-unused-value -Wno-unused-function -Wno-unused-variable -Wno-unused-but-set-variable -Wno-implicit-function-declaration -Wno-empty-body -I/home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl -o a.out.e-acsl monitored_first.i /home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl/e_acsl_rtl.c /home/jaeyoung/.opam/default/bin/../lib/frama-c/e-acsl/libeacsl-dlmalloc.a -lgmp -lm
jaeyoung@jaeyoung-VirtualBox:~/Documents$ ls
a.out first.i monitored_first.c monitored_first.o pow.i
a.out.e-acsl format-string.c monitored_first.i no_main.i
jaeyoung@jaeyoung-VirtualBox:~/Documents$ ./a.out.e-acsl
Segmentation fault (core dumped)
```
**I checked it through gdb, can you tell me how to solve it?**
```
jaeyoung@jaeyoung-VirtualBox:~/Documents$ gdb -q ./a.out.e-acsl
Reading symbols from ./a.out.e-acsl...
(gdb) run
Starting program: /home/jaeyoung/Documents/a.out.e-acsl
Program received signal SIGSEGV, Segmentation fault.
0x000055555555bf0a in shadow_alloca (ptr=ptr@entry=0x7ffff7ddb6a0 <_IO_2_1_stdout_>,
size=size@entry=216)
at /home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c:302
302 sec_shadow[j++] = size;
(gdb) info locals
i = 0
j = 1
k = 0
boundary = 216
prim_shadow = <optimized out>
prim_shadow_alt = 0x0
sec_shadow = 0x0
i = <optimized out>
j = 0
k = 0
(gdb)
```Julien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/2604e-acsl-gcc.sh segmentation fault2022-05-12T12:25:35ZJaeD-Shine-acsl-gcc.sh segmentation faultWhenever option --validate-format-strings of e-acsl-gcc.sh is set, E-ACSL detects format-string vulnerabilities in printf-like function. Below is an example which incorrectly tries to print a string through a %d format.
File printf.c
``...Whenever option --validate-format-strings of e-acsl-gcc.sh is set, E-ACSL detects format-string vulnerabilities in printf-like function. Below is an example which incorrectly tries to print a string through a %d format.
File printf.c
```
#include <stdio.h>
int main(void) {
printf ("is %d really an int?", "foo");
return 0;
}
```
```
jaeyoung@jaeyoung-VirtualBox:~/Downloads/frama$ e-acsl-gcc.sh -Oprintf -c --validate-format-strings print.c
+ /home/jaeyoung/.opam/default/bin/frama-c -remove-unused-specified-functions -variadic-no-translation -machdep gcc_x86_64 '-cpp-extra-args= -std=c99 -D_DEFAULT_SOURCE -D__NO_CTYPE -D__FC_MACHDEP_X86_64 ' -no-frama-c-stdlib print.c -e-acsl -e-acsl-validate-format-strings -e-acsl-share=/home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl -then-last -print -ocode a.out.frama.c
[kernel] Parsing print.c (with preprocessing)
[e-acsl] beginning translation.
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] /usr/include/x86_64-linux-gnu/bits/thread-shared-types.h:92: Warning:
unnamed fields are a C11 extension (use -c11 to avoid this warning)
[e-acsl] translation done in project "e-acsl".
+ gcc -std=c99 -m64 -g -O2 -fno-builtin -fno-merge-constants -Wall -Wno-long-long -Wno-attributes -Wno-nonnull -Wno-undef -Wno-unused -Wno-unused-function -Wno-unused-result -Wno-unused-value -Wno-unused-function -Wno-unused-variable -Wno-unused-but-set-variable -Wno-implicit-function-declaration -Wno-empty-body print.c -o printf
+ gcc -DE_ACSL_SEGMENT_MMODEL -DE_ACSL_VALIDATE_FORMAT_STRINGS -std=c99 -m64 -g -O2 -fno-builtin -fno-merge-constants -Wall -Wno-long-long -Wno-attributes -Wno-nonnull -Wno-undef -Wno-unused -Wno-unused-function -Wno-unused-result -Wno-unused-value -Wno-unused-function -Wno-unused-variable -Wno-unused-but-set-variable -Wno-implicit-function-declaration -Wno-empty-body -I/home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl -o printf.e-acsl a.out.frama.c /home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl/e_acsl_rtl.c /home/jaeyoung/.opam/default/bin/../lib/frama-c/e-acsl/libeacsl-dlmalloc.a -lgmp -lm
jaeyoung@jaeyoung-VirtualBox:~/Downloads/frama$ ./printf.e-acsl
Segmentation fault (core dumped)
```
The error in the printf.c file cannot be detected because a 'segmentation fault' has occurred.
The result of running gdb of ./printf.e-acsl is as follows.
```
(gdb) run
Starting program: /home/jaeyoung/Downloads/frama/printf.e-acsl
Program received signal SIGSEGV, Segmentation fault.
0x000055555555c1fa in shadow_alloca (
ptr=ptr@entry=0x7ffff7ddb6a0 <_IO_2_1_stdout_>, size=size@entry=216)
at /home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c:302
302 sec_shadow[j++] = size;
(gdb) bt
#0 0x000055555555c1fa in shadow_alloca (
ptr=ptr@entry=0x7ffff7ddb6a0 <_IO_2_1_stdout_>, size=size@entry=216)
at /home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c:302
#1 0x000055555555e9bf in register_safe_locations (
thread_only=thread_only@entry=0)
at /home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c:720
#2 0x000055555555ea88 in do_eacsl_memory_init (argc_ref=<optimized out>,
argv_ref=<optimized out>, ptr_size=<optimized out>)
at /home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c:324
#3 0x000055555555ebd9 in __e_acsl_memory_init (argc_ref=<optimized out>,
argv_ref=<optimized out>, ptr_size=<optimized out>)
at /home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c:331
#4 0x0000555555557856 in main () at a.out.frama.c:243
```Julien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/2603package 'why3' error2022-03-17T08:14:27ZJaeD-Shinpackage 'why3' errormy ubuntu version is Ubuntu 20.04.3 LTS opam version is 4.08.1
After run 'frama-c -e-acsl first.i', happening package 'why3' error..
Package why3 is already installed and current version of why3 is 1.4.0.
```
jaeyoung@jaeyoung-VirtualB...my ubuntu version is Ubuntu 20.04.3 LTS opam version is 4.08.1
After run 'frama-c -e-acsl first.i', happening package 'why3' error..
Package why3 is already installed and current version of why3 is 1.4.0.
```
jaeyoung@jaeyoung-VirtualBox:~/frama-c$ frama-c -e-acsl first.i
[kernel] User Error: [findlib] package 'why3' not found (required by `frama-c-wp')
[kernel] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.
```https://git.frama-c.com/pub/frama-c/-/issues/2602[findlib] package 'why3' not found2022-03-17T10:25:58ZJaeD-Shin[findlib] package 'why3' not foundMy ubuntu version is Ubuntu 20.04.3 LTS opam version is 4.08.1
After run 'frama-c -kernel-help', happening package 'why3' error.. Package why3 is already installed and current version of why3 is 1.4.0.
```
jaeyoung@jaeyoung-VirtualBox:...My ubuntu version is Ubuntu 20.04.3 LTS opam version is 4.08.1
After run 'frama-c -kernel-help', happening package 'why3' error.. Package why3 is already installed and current version of why3 is 1.4.0.
```
jaeyoung@jaeyoung-VirtualBox:~/Downloads/examples$ frama-c -kernel-help
[kernel] User Error: [findlib] package 'why3' not found (required by `frama-c-wp')
[kernel] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.
```
And Can you recommend a tutorial?https://git.frama-c.com/pub/frama-c/-/issues/2601[WP] [RTE] Unable to verify valid memory access in array using bitwise-ANDed ...2022-05-30T12:20:54ZCostava[WP] [RTE] Unable to verify valid memory access in array using bitwise-ANDed index when array is function parameter<!--
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
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
With Alt-Ergo 2.4.1 installed:
`frama-c -wp -wp-rte poc.c` / `frama-c-gui -wp -wp-rte poc.c`
using [poc.c](/uploads/62e84944634b546da975b2397c7c4e4d/poc.c) :
```c
/*@
requires \valid_read(arr + (0 .. 3));
assigns \nothing;
*/
int foo(const int arr[const static 4]) {
const unsigned int h = 7 & 0b11;
//@ assert 0 <= h < 4;
const int hvalue = arr[h];
const unsigned int i = 7 % 4;
//@ assert 0 <= i < 4;
const int ivalue = arr[i];
/*@
loop invariant 0 <= s <= 8;
loop assigns s;
loop variant 8 - s;
*/
for (unsigned int s = 0; s < 8; s += 1) {
const unsigned int j = s & 0b11;
//@ assert 0 <= j < 4;
const int jvalue = arr[j];
const unsigned int k = s % 4;
//@ assert 0 <= k < 4;
const int kvalue = arr[k];
}
return 0;
}
/*@
assigns \nothing;
*/
int main(void) {
const int arr[4] = {0, 1, 2, 3};
const unsigned int h = 7 & 0b11;
//@ assert 0 <= h < 4;
const int hvalue = arr[h];
const unsigned int i = 7 % 4;
//@ assert 0 <= i < 4;
const int ivalue = arr[i];
/*@
loop invariant 0 <= s <= 8;
loop assigns s;
loop variant 8 - s;
*/
for (unsigned int s = 0; s < 8; s += 1) {
const unsigned int j = s & 0b11;
//@ assert 0 <= j < 4;
const int jvalue = arr[j];
const unsigned int k = s % 4;
//@ assert 0 <= k < 4;
const int kvalue = arr[k];
}
foo(arr);
return 0;
}
```
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
All goals proved.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
```sh
$ frama-c -wp -wp-rte poc.c
[kernel] Parsing poc.c (with preprocessing)
[rte] annotating function foo
[rte] annotating function main
[wp] 34 goals scheduled
[wp] [Alt-Ergo 2.4.1] Goal typed_foo_assert_rte_mem_access_3 : Timeout (Qed:9ms) (10s)
[wp] Proved goals: 33 / 34
Qed: 23 (2ms-5ms-14ms)
Alt-Ergo 2.4.1: 10 (7ms-17ms-30ms) (556) (interrupted: 1)
```
33/34 goals proved.
The verification of `/*@ assert rte: mem_access: \valid_read(arr + j); */` for code `const int jvalue = arr[j];` in function `foo` is not successful.
From a naive perspective, the `arr[j]` accesses in main and foo are equivalent, so the assert in foo should be verifiable if the assert in main is.
(I am aware that a different assert is generated in main: `/*@ assert rte: index_bound: j < 4; */`)
Also, the `//@ assert 0 <= j < 4;` immediately before the access can be verified, both in main and foo, so it seems the rte assert should be able to be verified also.
### Contextual information
- Frama-C installation mode: opam
- Frama-C version: 24.0 (Chromium)
- Plug-in used: WP, RTE
- OS name: Manjaro Linux
- OS version: Qonos 21.2.4
### Additional information (optional)
<!--
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.
-->
The poc.c is a simplified proof of concept, but I did hit this situation when working on a real program.
To be explicit about the provers involved:
```sh
$ why3 config detect
Found prover Alt-Ergo version 2.4.1, OK.
1 prover(s) added
Save config to /home/user/.why3.conf
```
I was uncertain whether to submit this here or at the [alt-ergo issues](https://github.com/OCamlPro/alt-ergo/issues).
Apologies if this is the wrong place. Let me know if I should post there instead.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2599Problem with dependencies: Alt-Ergo set to 1.012022-05-11T06:28:08ZJaeD-ShinProblem with dependencies: Alt-Ergo set to 1.01my ubuntu version is Ubuntu 20.04.3 LTS
opam version is 4.08.1
After run 'opam install frama-c error', happening this issue.
```
[ERROR] The compilation of alt-ergo failed at
"/home/jaeyoung/.opam/opam-init/hooks/sandbox.sh ...my ubuntu version is Ubuntu 20.04.3 LTS
opam version is 4.08.1
After run 'opam install frama-c error', happening this issue.
```
[ERROR] The compilation of alt-ergo failed at
"/home/jaeyoung/.opam/opam-init/hooks/sandbox.sh build make".
∗ installed why3.1.4.1
#=== ERROR while compiling alt-ergo.1.01 ======================================#
# context 2.0.5 | linux/x86_64 | ocaml-system.4.08.1 | https://opam.ocaml.org#257f9ce1
# path ~/.opam/default/.opam-switch/build/alt-ergo.1.01
# command ~/.opam/opam-init/hooks/sandbox.sh build make
# exit-code 2
# env-file ~/.opam/log/alt-ergo-23270-89b24d.env
# output-file ~/.opam/log/alt-ergo-23270-89b24d.out
### output ###
# [...]
# ocamlopt.opt -c -annot -inline 100 -I /home/jaeyoung/.opam/default/lib/zarith -I /home/jaeyoung/.opam/default/lib/lablgtk2 -I +threads -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/myUnix.ml
# ocamlc.opt -c -annot -g -I /home/jaeyoung/.opam/default/lib/zarith -I /home/jaeyoung/.opam/default/lib/lablgtk2 -I +threads -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/util.mli
# ocamlopt.opt -c -annot -inline 100 -I /home/jaeyoung/.opam/default/lib/zarith -I /home/jaeyoung/.opam/default/lib/lablgtk2 -I +threads -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/util.ml
# ocamlc.opt -c -annot -g -I /home/jaeyoung/.opam/default/lib/zarith -I /home/jaeyoung/.opam/default/lib/lablgtk2 -I +threads -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/lists.mli
# ocamlopt.opt -c -annot -inline 100 -I /home/jaeyoung/.opam/default/lib/zarith -I /home/jaeyoung/.opam/default/lib/lablgtk2 -I +threads -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/lists.ml
# ocamlc.opt -c -annot -g -I /home/jaeyoung/.opam/default/lib/zarith -I /home/jaeyoung/.opam/default/lib/lablgtk2 -I +threads -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/numbersInterface.mli
# ocamlc.opt -c -annot -g -I /home/jaeyoung/.opam/default/lib/zarith -I /home/jaeyoung/.opam/default/lib/lablgtk2 -I +threads -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/numsNumbers.mli
# File "src/util/numsNumbers.mli", line 24, characters 47-62:
# 24 | module Z : NumbersInterface.ZSig with type t = Big_int.big_int
# ^^^^^^^^^^^^^^^
# Error: Unbound module Big_int
# make: *** [Makefile.users:220: src/util/numsNumbers.cmi] Error 2
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
┌─ The following actions failed
│ λ build alt-ergo 1.01
└─
┌─ The following changes have been performed (the rest was aborted)
│ ∗ install conf-autoconf 0.1
│ ∗ install conf-gmp 4
│ ∗ install conf-gnomecanvas 2
│ ∗ install conf-graphviz 0.1
│ ∗ install conf-gtk2 1
│ ∗ install conf-gtksourceview 2
│ ∗ install lablgtk 2.18.12
│ ∗ install ocamlgraph_gtk 2.0.0
│ ∗ install why3 1.4.1
│ ∗ install zarith 1.12
└─
# Run eval $(opam env) to update the current shell environment
The former state can be restored with:
opam switch import
"/home/jaeyoung/.opam/default/.opam-switch/backup/state-20220315135530.export"
```
I'm not sure how to handle the bottom part.https://git.frama-c.com/pub/frama-c/-/issues/2598install error2022-03-15T15:38:51ZJaeD-Shininstall erroraftter run 'opam depext frama-c', happening this issue.![issue](/uploads/6d494a24e40d9434b6d96c30b946e193/issue.png)
solution please :(aftter run 'opam depext frama-c', happening this issue.![issue](/uploads/6d494a24e40d9434b6d96c30b946e193/issue.png)
solution please :(https://git.frama-c.com/pub/frama-c/-/issues/2595Crash with Unexpected error (Cil.Not_representable).2022-07-11T15:36:34ZKarine EMCrash with Unexpected error (Cil.Not_representable).<!--
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
<!--
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
<!--
Please explain here what is the expected behaviour.
-->
Not to crush but return a proper error or warning regarding the issue in the input program.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
Crashed Frama-c
```
[kernel] Parsing fuzzer-file-2359.c (with preprocessing)
[kernel] Current source was: fuzzer-file-2359.c:1
The full backtrace is:
Raised at Cil.intKindForValue in file "src/kernel_services/ast_queries/cil.ml", line 3096, characters 7-30
Called from Cabs2cil.doSpecList in file "src/kernel_internals/typing/cabs2cil.ml", line 4796, characters 24-57
Called from Cabs2cil.doOnlyTypedef in file "src/kernel_internals/typing/cabs2cil.ml", line 9768, characters 28-53
Called from Cabs2cil.doDecl in file "src/kernel_internals/typing/cabs2cil.ml", line 9181, characters 34-68
Called from Cabs2cil.convFile.doOneGlobal in file "src/kernel_internals/typing/cabs2cil.ml", line 10455, characters 12-35
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Cabs2cil.convFile in file "src/kernel_internals/typing/cabs2cil.ml", line 10459, characters 2-25
Called from Frontc.parse.(fun) in file "src/kernel_internals/typing/frontc.ml", line 82, characters 14-36
Called from File.parse_cabs in file "src/kernel_services/ast_queries/file.ml", line 617, characters 25-44
Called from File.to_cil_cabs in file "src/kernel_services/ast_queries/file.ml", line 637, characters 14-38
Called from File.files_to_cabs_cil.(fun) in file "src/kernel_services/ast_queries/file.ml", line 700, characters 46-72
Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34
Called from File.files_to_cabs_cil in file "src/kernel_services/ast_queries/file.ml", line 700, characters 17-89
Called from File.prepare_from_c_files in file "src/kernel_services/ast_queries/file.ml", line 1792, characters 24-60
Called from File.init_from_cmdline in file "src/kernel_services/ast_queries/file.ml", line 1869, characters 4-27
Called from Ast.force_compute in file "src/kernel_services/ast_data/ast.ml", line 110, characters 2-28
Called from Ast.compute in file "src/kernel_services/ast_data/ast.ml", line 118, characters 53-71
Called from Boot.play_analysis in file "src/kernel_internals/runtime/boot.ml", line 29, characters 6-20
Called from Cmdline.play_in_toplevel_one_shot in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 846, characters 2-9
Called from Cmdline.play_in_toplevel in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 876, characters 18-64
Called from Cmdline.catch_toplevel_run in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 235, characters 4-8
Unexpected error (Cil.Not_representable).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 24.0 (Chromium).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: *Frama-C version* 24.0 (Chromium)
- Plug-in used: none
- OS name: Ubuntu
- OS version: 18
### Additional information (optional)
<!--
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.
-->
This is the (reduced) program:
```
enum { a = 11423207941596596085, b = -51 };
int main (void) {
return 0;
}
```
got the crash when running frama-c with no other plugins
```
frama-c fuzzer-file-2359.c
```Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2594Unsafe uses of Obj in Unmarshal2022-05-30T08:20:54ZVincent LavironUnsafe uses of Obj in UnmarshalA few pieces of code in the `Unmarshal` module are too obviously unsafe for the Flambda 2 compiler's taste, and results in the compiler deliberately inserting a segfault.
The `Sys.opaque_identity` function can be used to tell the compile...A few pieces of code in the `Unmarshal` module are too obviously unsafe for the Flambda 2 compiler's taste, and results in the compiler deliberately inserting a segfault.
The `Sys.opaque_identity` function can be used to tell the compiler not to make any assumptions on the underlying value, and is available since OCaml 4.03, so I'd like to see it used here to allow testing Frama C with Flambda 2.
The three places that are affected are:
- The code for initialising `arch_bigendian`. This can be fixed by inserting a call to `Sys.opaque_identity`.
- The code for initialising `arch_float_endianness`. This can be fixed by inserting a call to `Sys.opaque_identity`.
- The code for computing the `null` value. I assume that the code was intended to compute a null pointer, but it was reading the wrong field anyway so this was instead a pointer to a C-allocated struct (which, it seems, works as well). I'd like to replace it with `Obj.repr (Sys.opaque_identity (ref 0))`, which should work too (it gives you a unique static pointer) and has the advantage of not manipulating naked pointers.
I could propose a patch if you'd like (or even open a merge request, if your GitLab instance accepts merge requests from external contributors)25 (Manganese)François BobotFrançois Bobothttps://git.frama-c.com/pub/frama-c/-/issues/2593Build failure if only the eva plugin is selected: -rectypes is required2022-07-11T15:44:07Zfx-cartonBuild failure if only the eva plugin is selected: -rectypes is required### Steps to reproduce the issue
- untar the frama-c-24.0 sources
- configure with: --disable-landmarks --with-no-plugin --enable-gui --enable-callgraph --enable-server --enable-eva
- make
### Expected behaviour
Compilation succeeds
#...### Steps to reproduce the issue
- untar the frama-c-24.0 sources
- configure with: --disable-landmarks --with-no-plugin --enable-gui --enable-callgraph --enable-server --enable-eva
- make
### Expected behaviour
Compilation succeeds
### Actual behaviour
Compilation fails with the following message:
```
Ocamlc src/plugins/value/domains/multidim_domain.cmo
File "src/plugins/value/domains/multidim_domain.ml", line 1:
Error: Invalid import of Abstract_memory, which uses recursive types.
The compilation flag -rectypes is required
make: *** [share/Makefile.generic:78: src/plugins/value/domains/multidim_domain.cmo] Error 2
```
### Contextual information
- Frama-C installation mode: from source
- Frama-C version: 24.0
- Plug-in used: Eva (and dependencies)
- OS name: Linux
- OS version: Gentoo linux
### Additional information (optional)
- With no configure options, it builds fine.
- I've tried to debug the issue, and I think this is caused by having "-rectypes" added to BFLAGS for the rule compiling src/kernel_services/abstract_interp/abstract_memory.mli; which seems to be added as a side effect of the following line in the Makefile:
```
src/kernel_services/abstract_interp/abstract_memory.cmo: BFLAGS += -rectypes
```
For some reason, the dependency tree happens to change between the two configurations (default ./configure and ./configure with the aforementioned options), and in the latter case, the .cmi is a dependency of the .cmo, and thus inherits the local variables including BFLAGS.
- If I run `make src/kernel_services/abstract_interp/abstract_memory.cmi` and then `make`, it builds fine, because in the first make invocation the .cmo is not in the dependency tree, so -rectypes won't be added.Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2592Crash when size of field is zero with Unexpected error (Invalid_argument("Z.s...2022-07-11T15:45:22ZKarine EMCrash when size of field is zero with Unexpected error (Invalid_argument("Z.shift_left: count argument must be positive")).<!--
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
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
```
frama-c -eva 5523daed847ab69918007c2c696bec546984c2d8.c
```
will get the crash:
```
Unexpected error (Invalid_argument("Z.shift_left: count argument must be positive")).
```
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
Return a user error for line 3.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
With this code and eva:
```
struct __attribute__((packed)) S
{
int s : (0);
};
void main () {
struct S e[] = {0};
}
```
we get this crash:
```
[kernel] Parsing 5523daed847ab69918007c2c696bec546984c2d8.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
[kernel] Current source was: 5523daed847ab69918007c2c696bec546984c2d8.c:6
The full backtrace is:
Raised by primitive operation at file "z.ml", line 180, characters 4-20
Called from file "src/libraries/stdlib/integer.ml" (inlined), line 30, characters 2-22
Called from file "src/kernel_services/abstract_interp/int_val.ml", line 549, characters 14-45
Called from file "src/kernel_services/abstract_interp/int_val.ml", line 566, characters 10-63
Called from file "src/kernel_services/abstract_interp/ival.ml", line 525, characters 24-65
Called from file "src/plugins/value_types/cvalue.ml", line 427, characters 23-57
Called from file "src/plugins/value/engine/evaluation.ml", line 700, characters 18-50
Called from file "src/plugins/value/engine/evaluation.ml", line 747, characters 10-57
Called from file "src/plugins/value/engine/evaluation.ml", line 917, characters 14-39
Called from file "src/plugins/value/eval.ml", line 48, characters 29-32
Called from file "src/plugins/value/engine/evaluation.ml", line 845, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 810, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 1118, characters 6-36
Called from file "src/plugins/value/engine/evaluation.ml" (inlined), line 1166, characters 4-67
Called from file "src/plugins/value/engine/evaluation.ml", line 1527, characters 23-77
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 164, characters 14-59
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 184, characters 4-54
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 258, characters 10-55
Called from file "src/plugins/value/engine/initialization.ml", line 131, characters 10-48
Called from file "list.ml", line 121, characters 24-34
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/initialization.ml", line 304, characters 8-95
Called from file "src/plugins/value/engine/iterator.ml", line 234, characters 33-36
Called from file "src/plugins/value/partitioning/partition.ml", line 649, characters 29-42
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/iterator.ml", line 436, characters 15-74
Called from file "src/plugins/value/engine/iterator.ml", line 501, characters 18-35
Called from file "list.ml", line 92, characters 20-23
Called from file "src/plugins/value/engine/iterator.ml", line 503, characters 18-60
Called from file "src/plugins/value/engine/iterator.ml", line 550, characters 13-31
Called from file "list.ml", line 110, characters 12-15
Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 547, characters 4-31
Called from file "src/plugins/value/engine/iterator.ml", line 609, characters 6-22
Called from file "src/plugins/value/engine/iterator.ml", line 776, characters 20-39
Called from file "src/plugins/value/utils/value_util.ml", line 114, characters 6-10
Called from file "src/plugins/value/engine/compute_functions.ml", line 206, characters 8-45
Called from file "src/plugins/value/engine/compute_functions.ml", line 344, characters 8-63
Called from file "src/plugins/value/utils/value_util.ml", line 114, characters 6-10
Called from file "src/plugins/value/engine/analysis.ml", line 181, characters 2-49
Called from file "src/libraries/project/state_builder.ml", line 998, characters 9-13
Re-raised at file "src/libraries/project/state_builder.ml", line 1006, characters 9-18
Called from file "src/plugins/value/register.ml", line 39, characters 46-66
Called from file "queue.ml", line 121, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 846, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 876, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 235, characters 4-8
Unexpected error (Invalid_argument("Z.shift_left: count argument must be positive")).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 24.0 (Chromium).
```
Without Eva, we don't get the crash, but we also got no warning, which we should get for line 3.
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: *Frama-C version* 24.0 (Chromium)
- Plug-in used: Eva
- OS name: Ubuntu
- OS version: 18
### Additional information (optional)
<!--
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.
-->
Might be related to bug https://git.frama-c.com/pub/frama-c/-/issues/2556Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2591Error when install frama-c with opam2022-09-28T12:52:59ZryancaicseError when install frama-c with opamWhen I use `opam install frama-c` I got the below errors. What should I do? Thanks!
```
rando@ubuntu:~$ opam install frama-c
The following actions will be performed:
∗ install conf-gtk2 1 [required by lablgtk]
∗ insta...When I use `opam install frama-c` I got the below errors. What should I do? Thanks!
```
rando@ubuntu:~$ opam install frama-c
The following actions will be performed:
∗ install conf-gtk2 1 [required by lablgtk]
∗ install conf-gtksourceview 2 [required by frama-c]
∗ install conf-gnomecanvas 2 [required by frama-c]
∗ install lablgtk 2.18.11 [required by frama-c]
∗ install ocamlgraph_gtk 2.0.0 [required by frama-c]
∗ install frama-c 24.0
The Frama-C/Wp now uses Why-3 for all provers (Cf.
deprecated -wp-prover native:alt-ergo)
===== ∗ 6 =====
Do you want to continue? [Y/n] y
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><>
⬇ retrieved frama-c.24.0 (cached)
⬇ retrieved lablgtk.2.18.11 (cached)
⬇ retrieved ocamlgraph_gtk.2.0.0 (cached)
[ERROR] The compilation of conf-gnomecanvas.2 failed at "pkg-config
libgnomecanvas-2.0".
[ERROR] The compilation of conf-gtk2.1 failed at "pkg-config --exists
gtk+-2.0".
[ERROR] The compilation of conf-gtksourceview.2 failed at "pkg-config
--short-errors --print-errors gtksourceview-2.0".
#=== ERROR while compiling conf-gtksourceview.2 =====================#
# context 2.1.2 | linux/x86_64 | ocaml-option-flambda.1 ocaml-variants.4.12.0+options | https://opam.ocaml.org/#3aeec9a7
# path ~/.opam/4.12.0+flambda/.opam-switch/build/conf-gtksourceview.2
# command ~/.opam/opam-init/hooks/sandbox.sh build pkg-config --short-errors --print-errors gtksourceview-2.0
# exit-code 1
# env-file ~/.opam/log/conf-gtksourceview-53359-4fbae4.env
# output-file ~/.opam/log/conf-gtksourceview-53359-4fbae4.out
### output ###
# No package 'gtksourceview-2.0' found
#=== ERROR while compiling conf-gtk2.1 ==============================#
# context 2.1.2 | linux/x86_64 | ocaml-option-flambda.1 ocaml-variants.4.12.0+options | https://opam.ocaml.org/#3aeec9a7
# path ~/.opam/4.12.0+flambda/.opam-switch/build/conf-gtk2.1
# command ~/.opam/opam-init/hooks/sandbox.sh build pkg-config --exists gtk+-2.0
# exit-code 1
# env-file ~/.opam/log/conf-gtk2-53359-73ec4e.env
# output-file ~/.opam/log/conf-gtk2-53359-73ec4e.out
#=== ERROR while compiling conf-gnomecanvas.2 =======================#
# context 2.1.2 | linux/x86_64 | ocaml-option-flambda.1 ocaml-variants.4.12.0+options | https://opam.ocaml.org/#3aeec9a7
# path ~/.opam/4.12.0+flambda/.opam-switch/build/conf-gnomecanvas.2
# command ~/.opam/opam-init/hooks/sandbox.sh build pkg-config libgnomecanvas-2.0
# exit-code 1
# env-file ~/.opam/log/conf-gnomecanvas-53359-4e35be.env
# output-file ~/.opam/log/conf-gnomecanvas-53359-4e35be.out
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><>
┌─ The following actions failed
│ λ build conf-gnomecanvas 2
│ λ build conf-gtk2 1
│ λ build conf-gtksourceview 2
└─
╶─ No changes have been performed
```Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2590Frama-c crash with Unexpected error (Invalid_argument("Array.make"))2022-02-09T07:14:30ZKarine EMFrama-c crash with Unexpected error (Invalid_argument("Array.make"))<!--
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
`frama-c 8ff8d2fc802d04c6a8b50094288d03e291d2c9bf.c`
<!--
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
<!--
Please explain here what is the expected behaviour.
-->
Not to crash
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
Crash with Unexpected error (Invalid_argument("Array.make")), for this (reduced) program:
```
int a[] = {[72057594037927936] 0};
void main() {}
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: *Frama-C version* 24.0 (Chromium)
- Plug-in used: none
- OS name: Ubuntu
- OS version: 18
### Additional information (optional)
<!--
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.
-->
The trace of the error:
```
frama-c 8ff8d2fc802d04c6a8b50094288d03e291d2c9bf.c
[kernel] Parsing 8ff8d2fc802d04c6a8b50094288d03e291d2c9bf.c (with preprocessing)
[kernel] Current source was: 8ff8d2fc802d04c6a8b50094288d03e291d2c9bf.c:1
The full backtrace is:
Raised by primitive operation at file "src/kernel_internals/typing/cabs2cil.ml", line 3393, characters 21-62
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 8353, characters 19-72
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 8379, characters 8-85
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 8076, characters 4-112
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 8639, characters 27-73
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 9137, characters 18-76
Called from file "list.ml", line 121, characters 24-34
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 9154, characters 14-53
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 10455, characters 12-35
Called from file "list.ml", line 110, characters 12-15
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 10459, characters 2-25
Called from file "src/kernel_internals/typing/frontc.ml", line 82, characters 14-36
Called from file "src/kernel_services/ast_queries/file.ml", line 617, characters 25-44
Called from file "src/kernel_services/ast_queries/file.ml", line 637, characters 14-38
Called from file "src/kernel_services/ast_queries/file.ml", line 700, characters 46-72
Called from file "list.ml", line 121, characters 24-34
Called from file "src/kernel_services/ast_queries/file.ml", line 700, characters 17-89
Called from file "src/kernel_services/ast_queries/file.ml", line 1792, characters 24-60
Called from file "src/kernel_services/ast_queries/file.ml", line 1869, characters 4-27
Called from file "src/kernel_services/ast_data/ast.ml", line 110, characters 2-28
Called from file "src/kernel_services/ast_data/ast.ml", line 118, characters 53-71
Called from file "src/kernel_internals/runtime/boot.ml", line 29, characters 6-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 846, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 876, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 235, characters 4-8
Unexpected error (Invalid_argument("Array.make")).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 24.0 (Chromium).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
```Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2589[WP] Failure to verify range information after bitwise and on signed integers2022-01-11T07:16:49ZGuerricChupin[WP] Failure to verify range information after bitwise and on signed integersIn the function below, WP fails to verify the assertion (which I believe is true after exhaustively testing it):
```c
/*@ assigns \nothing;
@*/
int8_t foo(int8_t n) {
int8_t m = n & 0xF;
/*@ assert 0 <= m < 16; */
return ...In the function below, WP fails to verify the assertion (which I believe is true after exhaustively testing it):
```c
/*@ assigns \nothing;
@*/
int8_t foo(int8_t n) {
int8_t m = n & 0xF;
/*@ assert 0 <= m < 16; */
return m;
}
```
It does so with all signed integer types, but doesn't with unsigned integer types. Performing the `&` on an unsigned integer type and casting the result to a signed integer doesn't work either. For instance, in the function below, the first assertion is verified but not the second:
```c
int8_t bar(int8_t n) {
uint8_t m = n & 0xF;
/*@ assert 0 <= m < 16; */
int8_t p = m;
/*@ assert 0 <= p < 16; */
return p;
}
```
Test file: [test.c](/uploads/2751b8e74f9f0f37840a32cbff4965ce/test.c)
I used this command to run Frama-C:
```bash
frama-c -wp -wp-rte test.c -wp-prover why3:alt-ergo -wp-prover why3:cvc4 -wp-prover why3:Z3
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 24.0
- Plug-in used: WP, RTE
- OS name: Fedora
- OS version: 35
- Solvers: Alt-Ergo 2.4.1, CVC4 1.8, Z3 4.8.11
### Additional information (optional)
<!--
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.
-->https://git.frama-c.com/pub/frama-c/-/issues/2588Frama-c crashes with "src/kernel_services/abstract_interp/ival.ml", line 444,...2022-01-24T09:36:26ZKarine EMFrama-c crashes with "src/kernel_services/abstract_interp/ival.ml", line 444, characters 31-37: Assertion failed<!--
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
```
frama-c -eva fuzzer-file-49652.c
```
<!--
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
Not to crash
<!--
Please explain here what is the expected behaviour.
-->
### Actual behaviour
Frama-c 24.0 crashed with "src/kernel_services/abstract_interp/ival.ml", line 444, characters 31-37: Assertion failed
I reduced the original program to this:
```
#include <stdarg.h>
long a;
void b(va_list ap) {
a = va_arg(ap, double);
a += va_arg(ap, long);
}
void c(int d, ...) {
va_list ap;
va_start(ap, d);
b(ap);
}
void main() { c(0, 8.1, 7.1); }
```
<!--
Please explain here what is the actual (faulty) behaviour.
-->
The crash's trace is:
```
[kernel] Parsing fuzzer-file-49652.c (with preprocessing)
[kernel:parser:decimal-float] fuzzer-file-49652.c:12: Warning:
Floating-point constant 7.1 is not represented exactly. Will use 0x1.c666666666666p2.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
a ∈ {0}
[eva:alarm] fuzzer-file-49652.c:5: Warning:
signed overflow. assert a + tmp ≤ 9223372036854775807;
(tmp from vararg)
[kernel] Current source was: fuzzer-file-49652.c:5
The full backtrace is:
Raised at file "src/kernel_services/abstract_interp/ival.ml", line 444, characters 31-43
Called from file "src/libraries/utils/hptmap.ml", line 934, characters 18-24
Called from file "src/kernel_services/abstract_interp/map_lattice.ml", line 428, characters 24-39
Called from file "src/plugins/value_types/cvalue.ml", line 557, characters 10-64
Called from file "src/plugins/value/legacy/eval_terms.ml", line 1357, characters 17-46
Called from file "src/plugins/value/legacy/eval_terms.ml" (inlined), line 2680, characters 25-57
Called from file "src/plugins/value/legacy/eval_terms.ml", line 2690, characters 22-36
Called from file "src/plugins/value/legacy/eval_terms.ml", line 2736, characters 11-29
Called from file "src/plugins/inout/operational_inputs.ml", line 383, characters 19-67
Called from file "list.ml", line 110, characters 12-15
Called from file "src/plugins/inout/operational_inputs.ml", line 485, characters 6-28
Called from file "src/kernel_services/analysis/dataflows.ml", line 514, characters 12-42
Called from file "src/kernel_services/analysis/dataflows.ml", line 522, characters 19-30
Called from file "src/kernel_services/analysis/dataflows.ml", line 523, characters 5-14
Called from file "src/kernel_services/analysis/dataflows.ml" (inlined), line 582, characters 10-48
Called from file "src/kernel_services/analysis/dataflows.ml" (inlined), line 582, characters 10-57
Called from file "src/kernel_services/analysis/dataflows.ml", line 582, characters 10-60
Called from file "src/plugins/inout/operational_inputs.ml" (inlined), line 702, characters 6-37
Called from file "src/plugins/inout/operational_inputs.ml", line 702, characters 6-48
Called from file "src/plugins/inout/operational_inputs.ml", line 716, characters 14-78
Called from file "queue.ml", line 121, characters 6-15
Called from file "src/plugins/value/engine/iterator.ml", line 731, characters 8-214
Called from file "src/plugins/value/engine/iterator.ml", line 780, characters 6-31
Called from file "src/plugins/value/utils/value_util.ml", line 114, characters 6-10
Called from file "src/plugins/value/engine/compute_functions.ml", line 206, characters 8-45
Called from file "src/plugins/value/engine/compute_functions.ml", line 228, characters 26-36
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 326, characters 10-53
Called from file "src/plugins/value/utils/value_util.ml", line 114, characters 6-10
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 463, characters 22-70
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 767, characters 14-73
Called from file "src/kernel_services/abstract_interp/bottom.ml", line 36, characters 25-30
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 762, characters 12-489
Called from file "list.ml", line 121, characters 24-34
Called from file "src/kernel_services/abstract_interp/bottom.ml", line 36, characters 25-30
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 749, characters 6-1023
Called from file "src/plugins/value/engine/iterator.ml", line 278, characters 6-47
Called from file "src/plugins/value/partitioning/partition.ml", line 649, characters 29-42
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/iterator.ml", line 436, characters 15-74
Called from file "src/plugins/value/engine/iterator.ml", line 501, characters 18-35
Called from file "list.ml", line 92, characters 20-23
Called from file "src/plugins/value/engine/iterator.ml", line 503, characters 18-60
Called from file "src/plugins/value/engine/iterator.ml", line 550, characters 13-31
Called from file "list.ml", line 110, characters 12-15
Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 547, characters 4-31
Called from file "src/plugins/value/engine/iterator.ml", line 609, characters 6-22
Called from file "src/plugins/value/engine/iterator.ml", line 776, characters 20-39
Called from file "src/plugins/value/utils/value_util.ml", line 114, characters 6-10
Called from file "src/plugins/value/engine/compute_functions.ml", line 206, characters 8-45
Called from file "src/plugins/value/engine/compute_functions.ml", line 228, characters 26-36
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 326, characters 10-53
Called from file "src/plugins/value/utils/value_util.ml", line 114, characters 6-10
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 463, characters 22-70
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 767, characters 14-73
Called from file "src/kernel_services/abstract_interp/bottom.ml", line 36, characters 25-30
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 762, characters 12-489
Called from file "list.ml", line 121, characters 24-34
Called from file "src/kernel_services/abstract_interp/bottom.ml", line 36, characters 25-30
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 749, characters 6-1023
Called from file "src/plugins/value/engine/iterator.ml", line 278, characters 6-47
Called from file "src/plugins/value/partitioning/partition.ml", line 649, characters 29-42
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/iterator.ml", line 436, characters 15-74
Called from file "src/plugins/value/engine/iterator.ml", line 501, characters 18-35
Called from file "list.ml", line 92, characters 20-23
Called from file "src/plugins/value/engine/iterator.ml", line 503, characters 18-60
Called from file "src/plugins/value/engine/iterator.ml", line 550, characters 13-31
Called from file "list.ml", line 110, characters 12-15
Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 547, characters 4-31
Called from file "src/plugins/value/engine/iterator.ml", line 609, characters 6-22
Called from file "src/plugins/value/engine/iterator.ml", line 776, characters 20-39
Called from file "src/plugins/value/utils/value_util.ml", line 114, characters 6-10
Called from file "src/plugins/value/engine/compute_functions.ml", line 206, characters 8-45
Called from file "src/plugins/value/engine/compute_functions.ml", line 344, characters 8-63
Called from file "src/plugins/value/utils/value_util.ml", line 114, characters 6-10
Called from file "src/plugins/value/engine/analysis.ml", line 181, characters 2-49
Called from file "src/libraries/project/state_builder.ml", line 998, characters 9-13
Re-raised at file "src/libraries/project/state_builder.ml", line 1006, characters 9-18
Called from file "src/plugins/value/register.ml", line 39, characters 46-66
Called from file "queue.ml", line 121, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 846, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 876, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 235, characters 4-8
Unexpected error (File "src/kernel_services/abstract_interp/ival.ml", line 444, characters 31-37: Assertion failed).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 24.0 (Chromium).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 24.0 (Chromium)
- Plug-in used: eva
- OS name: Ubuntu
- OS version: 18.04
### Additional information (optional)
<!--
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.
-->David BühlerDavid Bühlerhttps://git.frama-c.com/pub/frama-c/-/issues/2587Crash on Startup of frama-c-gui on WSL2022-01-18T09:06:14ZmoemodeCrash on Startup of frama-c-gui on WSL### Steps to reproduce the issue
Install frama-c on Windows 11 WSL according to install instructions. Then launch frama-c-gui
### Expected behaviour
frama-c-gui opens the gui
### Actual behaviour
![frama_err](/uploads/88a88cea9d4899...### Steps to reproduce the issue
Install frama-c on Windows 11 WSL according to install instructions. Then launch frama-c-gui
### Expected behaviour
frama-c-gui opens the gui
### Actual behaviour
![frama_err](/uploads/88a88cea9d4899909f2ee7ef74c73099/frama_err.png)
[frama_c_journal.ml](/uploads/a75256b6f842241a1e7ffb7ab0919b00/frama_c_journal.ml)
### Contextual information
- Frama-C installation mode: Opam as described on [Website](https://frama-c.com/html/get-frama-c.html)
- Frama-C version: 24.0 (Chromium)
- OS name: Windows
- OS version: 11Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2586** (frama-c-gui:11256): CRITICAL **2021-12-14T13:30:19Zankit247** (frama-c-gui:11256): CRITICAL **<!--
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
$ frama-c-gui foo.c Gdk-Message: 00:28:20.600: Unable to load arrow from the cursor theme ** (frama-c-gui:11388): CRITICAL **: 00:28:32.491: GSourceFunc: callback raised an exception
<!--
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
Getting error opening GUI for Frama-c
<!--
-->
### Actual behaviour
Should open the GUI
<!--
-->
### Contextual information
- Frama-C installation mode: **Opam**
- Frama-C version: **24.0**
- Plug-in used: **eva**
- OS name: Windows 11 (UBUNTU as WSLg)
- OS version: ubuntu 20.04 LTS
### Additional information (optional)
Usig command **frama-c -eva -main SumHadCoefficients foo.c**, not getting any error, also analysis result is getting dumped on terminal. But using gui gives error
![framac_gui_error_eva](/uploads/79eef02f4cce41c37a7ea764844fbe78/framac_gui_error_eva.png)
While running command frama-c-gui foo.c gives followin error
![framac_gui_error](/uploads/18d90850585b150c1ce9c3992a069e8c/framac_gui_error.png)
<!--
-->Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2585Unexpected error (Stack overflow) with large array sizes and expressions2022-09-15T15:56:24Zarindam-8Unexpected error (Stack overflow) with large array sizes and expressions
### Steps to reproduce the issue
[fc-bug.c](/uploads/a314f79930f93d2f2a1cea3080b7b043/fc-bug.c)Run the following command:
```
frama-c -eva -eva-slevel 100 -eva-plevel 256 -eva-precision 5 -eva-warn-undefined-pointer-comparison pointe...
### Steps to reproduce the issue
[fc-bug.c](/uploads/a314f79930f93d2f2a1cea3080b7b043/fc-bug.c)Run the following command:
```
frama-c -eva -eva-slevel 100 -eva-plevel 256 -eva-precision 5 -eva-warn-undefined-pointer-comparison pointer -eva-no-alloc-returns-null -warn-signed-overflow -eva-no-show-progress -machdep x86_64 fuzzer-file-102106.c
```
### Expected behaviour
Frama-C when run on the test program with the given command should exit gracefully instead of resulting in an "Unexpected
stackoverflow error"
### Actual behaviour
When Frama-C is run on the program with the given command parameters it results in a Frama-C crash. with the following trace (abbreviated)
```
[kernel] Parsing _rmv_fuzzer-file-102106.c (with preprocessing)
[eva] Option -eva-precision 5 detected, automatic configuration of the analysis:
option -eva-min-loop-unroll set to 0 (default value).
option -eva-auto-loop-unroll set to 128.
option -eva-widening-delay set to 3 (default value).
option -eva-partition-history set to 0 (default value).
option -eva-slevel already set to 100.
option -eva-ilevel set to 48.
option -eva-plevel already set to 256 (not modified).
option -eva-subdivide-non-linear set to 100.
option -eva-remove-redundant-alarms set to true (default value).
option -eva-domains set to 'cvalue,equality,gauges,octagon,symbolic-locations'.
option -eva-split-return set to 'auto'.
option -eva-equality-through-calls set to 'formals' (default value).
option -eva-octagon-through-calls set to false (default value).
[eva] Splitting return states on:
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
b.f2 ∈ {0}
.f3 ∈ {65006}
.[bits 65047 to 65055] ∈ {0}
.f5 ∈ {65005}
.[bits 130059 to 130063] ∈ {0}
.f6 ∈ {-536}
g.f2 ∈ {65008}
.f3 ∈ {65000}
.[bits 65047 to 65055] ∈ {0}
.f5 ∈ {65005}
.[bits 130059 to 130063] ∈ {0}
.f6 ∈ {-536}
d ∈ {0}
l ∈ {0}
a ∈ {0}
c ∈ {0}
h ∈ {65008}
e[0] ∈ {-20}
[1..65236] ∈ {0}
f ∈ {{ &d }}
i[0] ∈ {-533}
[1..65004] ∈ {0}
j ∈ {0}
k ∈ {{ &c }}
[kernel] Current source was: _rmv_fuzzer-file-102106.c:20
The full backtrace is:
Raised by primitive operation at file "src/blocks.ml", line 691, characters 11-59
Called from file "src/blocks.ml", line 703, characters 17-53
Called from file "src/libraries/utils/wto.ml", line 168, characters 18-36
Called from file "src/libraries/utils/wto.ml", line 170, characters 34-66
...
Unexpected error (Stack overflow).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 22.0 (Titanium).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 22.0 (Titanium)
- Plug-in used: eva
- OS name: Ubuntu
- OS version: Bionic 18.04
### Additional information (optional)
The crash seems inconsistent and appears sporadically. It seg-faults on some occasions while on others it crashes like mentioned above. With such expression length issues the crash seems legitimate.David BühlerDavid Bühlerhttps://git.frama-c.com/pub/frama-c/-/issues/2584[WP] Correction of loop-based copy function not prooved if using 32-bit integ...2021-11-23T08:12:16ZAlexCid[WP] Correction of loop-based copy function not prooved if using 32-bit integer sizes
### Steps to reproduce the issue
Save the following code into a file called "copy.c"
```C
#include <stdint.h>
typedef uint32_t size_t;
typedef enum {
OK, NOK
} error_t;
typedef struct {
size_t size;
unsigned int *values;
} bu...
### Steps to reproduce the issue
Save the following code into a file called "copy.c"
```C
#include <stdint.h>
typedef uint32_t size_t;
typedef enum {
OK, NOK
} error_t;
typedef struct {
size_t size;
unsigned int *values;
} buffer_t ;
/*@
requires
\valid(destination) && \valid(source) &&
\valid(destination->values+(0..destination->size-1)) &&
\valid(source->values+(0..source->size-1)) &&
\separated(source->values+(0..source->size-1), destination->values+(0..destination->size-1));
assigns
*(destination->values+(0..source->size-1));
ensures
(destination->size >= source->size) ==> ((\forall integer i; 0 <= i < source->size
==> (destination->values[i] == source->values[i])) && \result == OK);
ensures
(destination->size < source->size) ==> (\forall integer i; 0 <= i < destination->size
==> (destination->values[i] == \old(destination->values[i])) && \result == NOK);
*/
error_t copy(buffer_t* source, buffer_t* destination) {
error_t ret = NOK;
if (destination->size >= source->size) {
/*@
loop invariant 0 <= i <= source->size <= destination->size;
loop invariant \forall integer j ; 0 <= j < i ==> destination->values[j] == source->values[j];
loop assigns i, destination->values[0..source->size-1];
loop variant source->size-i;
*/
for(size_t i=0; i<source->size; i++) {
destination->values[i] = source->values[i];
}
ret = OK;
}
return ret;
}
```
Then analyse this code using the WP plugin with the command
`frama-c copy.c -wp -wp-rte -wp-prover alt-ergo,z3,cvc4 -wp-cache none`
<!--
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 annotations should be proved. Indeed, if the type of our local "size_t" type is changed to uint8_t, uint16_t or uint64_t, then all assertions are proved.
<!--
Please explain here what is the expected behaviour.
-->
### Actual behaviour
Only 12 out of the 20 assertions are proved. Notably, none of the loop annotations can be proved.
### Contextual information
- Frama-C installation mode: docker
- Frama-C version: 23.1
- Plug-in used: Eva, WP
- OS name: Ubuntu
- OS version: 20.04