frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2023-11-27T15:03:11Zhttps://git.frama-c.com/pub/frama-c/-/issues/2680[WP] Using Z3 when predicate with access to struct defined leads to inconsist...2023-11-27T15:03:11ZReMarxist[WP] Using Z3 when predicate with access to struct defined leads to inconsistency### Steps to reproduce the issue
Launch the following example with this command (note big timeout):
```bash
frama-c -wp -rte -wp-prover="z3" -wp-timeout 100 acsl.c
```
Example:
```c
struct S
{
int n;
};
/*@ axiomatic Block {
pr...### Steps to reproduce the issue
Launch the following example with this command (note big timeout):
```bash
frama-c -wp -rte -wp-prover="z3" -wp-timeout 100 acsl.c
```
Example:
```c
struct S
{
int n;
};
/*@ axiomatic Block {
predicate isZero(int left) =
left == 0;
// Unused, but necessary for verification
logic int getN(struct S *s) = s->n;
}*/
/*@ requires \valid(s);
requires isZero(s->n);
assigns \nothing;
ensures \false; // Verified by Z3
*/
void g(struct S *s)
{
}
/*@ assigns \nothing;
ensures \false; // Verified by Z3
*/
void f()
{
struct S s;
s.n = 0;
g(&s);
}
```
As you can see, specifications establish that f() and g() ensure obviously false statement. The problem is in verification of g(), I've defined f() to show that preconditions of g() can be satisfied.
### Expected behaviour
Attempt to prove `\false` in postcondition of `g()` should fail.
### Actual behaviour
Z3 proves `\false` in postcondition of `g()`:
```
[kernel] Parsing tmp/acsl/acsl.c (with preprocessing)
[rte:annot] annotating function f
[rte:annot] annotating function g
[wp] Running WP plugin...
[wp] 9 goals scheduled
[wp] Proved goals: 9 / 9
Qed: 7
Z3 4.12.2: 2
```
### Contextual information
- Frama-C installation mode: opam
- Frama-C version: 27.1 (Cobalt)
- Z3 version 4.12.2 - 64 bit
- Why3 platform version: 1.6.0
- Plug-in used: WP
- OS name: Ubuntu
- OS version: 20.04
### Additional information
The problem may be in Z3 itself, because Alt-Ergo and CVC4 cannot prove these goals. I've also reproduced the problem using docker image from Docker Hub.
I've posted this report as a question on StackOverflow previously (https://stackoverflow.com/questions/77460683/why-wp-with-z3-proves-false-when-access-to-struct-field-is-defined) as I wasn't able to post an issue here.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2648Frama-c-gui does not install on macOS Ventura2023-06-21T08:02:03ZNikolaus HuberFrama-c-gui does not install on macOS VenturaI have tried installing Frama-C through opam on macOS Ventura (13.0.1) for a few days now. I have followed the official installation instructions including the installation of all required tools with brew and setting PKG_CONFIG_PATH. Aft...I have tried installing Frama-C through opam on macOS Ventura (13.0.1) for a few days now. I have followed the official installation instructions including the installation of all required tools with brew and setting PKG_CONFIG_PATH. After issuing `opam install frama-c` Frama-C gets installed, however, whatever I tried frama-c-gui is never available.
When I try
```
opam uninstall frama-c
opam install frama-c.25.0
```
everything works perfectly. I have tried it both on an Intel and an M2 MacBookPro. Does anyone have a similar problem?Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2635e_acsl_assert is not getting added for all given asserts2022-11-09T10:25:29Zamruthabennye_acsl_assert is not getting added for all given assertsI am new to Frama-C. I specifically need to use e-acsl plugin for verification purposes. I used first.i file as
```
int main(void) {
int x = 0;
/∗@ assert x == 0; ∗/
/∗@ assert x == 1; ∗/
return 0;
}
```
Created monitored_first.c ...I am new to Frama-C. I specifically need to use e-acsl plugin for verification purposes. I used first.i file as
```
int main(void) {
int x = 0;
/∗@ assert x == 0; ∗/
/∗@ assert x == 1; ∗/
return 0;
}
```
Created monitored_first.c file from first.i file using the following command.
`$ frama-c -e-acsl first.i -then-last -print -ocode monitored_first.c`
The main function inside the monitored_first.c looks like the one below.
```
int main(void)
{
int __retres;
__e_acsl_memory_init((int *)0,(char ***)0,8UL);
int x = 0;
__retres = 0;
__e_acsl_memory_clean();
return __retres;
}
```
It is not adding e_acsl assertion for x==1.
I tried it using the "e-acsl-gcc.sh" script , which generated the monitored_first.i file. But the main function inside monitored_first.i is same as that in monitored_first.c.
`$ e-acsl-gcc.sh -c -omonitored_first.i first.i`
The above command generated two executable, "a.out.e-acsl" and "a.out". It also generates some warnings when run in ubuntu 22.04 as follows:
```
/home/amrutha/.opam/4.11.1/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/amrutha/.opam/4.11.1/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)
/tmp/ppannot15ad34.c:362: warning: "__STDC_IEC_60559_BFP__" redefined
362 | #define __STDC_IEC_60559_BFP__ 201404L
|
In file included from <command-line>:
/usr/include/stdc-predef.h:39: note: this is the location of the previous definition
39 | # define __STDC_IEC_60559_BFP__ 201404L
|
/tmp/ppannot15ad34.c:363: warning: "__STDC_IEC_60559_COMPLEX__" redefined
363 | #define __STDC_IEC_60559_COMPLEX__ 201404L
|
In file included from <command-line>:
/usr/include/stdc-predef.h:49: note: this is the location of the previous definition
49 | # define __STDC_IEC_60559_COMPLEX__ 201404L
|
[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/amrutha/.opam/4.11.1/bin/../share/frama-c/e-acsl -o a.out.e-acsl monitored_first.i /home/amrutha/.opam/4.11.1/bin/../share/frama-c/e-acsl/e_acsl_rtl.c /home/amrutha/.opam/4.11.1/bin/../lib/frama-c/e-acsl/libeacsl-dlmalloc.a -lgmp -lm
```
In ubuntu 20.04 there is no any warning, only the end part is getting displayed. When run ./a.out.e-acsl , it simply run the code without any message, which is not supposed. The expected output should look like this:
```
$ ./a.out.e-acsl
first.i: In function 'main'
first.i:4: Error: Assertion failed:
The failing predicate is:
x == 1.
Aborted (core dumped)
$ echo $?
134
```
I tried it in ubuntu 22.04 with opam version 2.1.2 and Fragma-C 25.0
and ubuntu 20.04 with opam version 2.0.5 and Fragma-C 25.0https://git.frama-c.com/pub/frama-c/-/issues/2632-wp-print for only failed goals2023-07-21T13:01:36ZDavid Cok-wp-print for only failed goalsI suggest a variation on -wp-print that only lists the details for failed goals, perhaps -wp-print-failuresI suggest a variation on -wp-print that only lists the details for failed goals, perhaps -wp-print-failuresLoïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2631Naming the anonymous behavior for -wp-bhv2023-06-21T08:58:19ZDavid CokNaming the anonymous behavior for -wp-bhvFeature request (or perhaps just information):
in using WP, the -wp-bhv option works fine for named behaviors. But how does one indicate to check just the anonymous behavior?
If there is no way currently, then please add some syntax tha...Feature request (or perhaps just information):
in using WP, the -wp-bhv option works fine for named behaviors. But how does one indicate to check just the anonymous behavior?
If there is no way currently, then please add some syntax that does not interfere with most shells. For example -wp-bhv ~Loïc CorrensonLoïc Corrensonhttps://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/2571struct fields not assignable if any are const2021-08-31T16:52:57ZAaron Carrollstruct fields not assignable if any are const### Steps to reproduce the issue
Consider the following C snippet:
```
struct A {
const int x;
int y;
};
static struct A a;
/*@
assigns a.y;
*/
void f(void)
{
a.y = 1;
}
```
produces:
```
$ frama-c test_global_assi...### Steps to reproduce the issue
Consider the following C snippet:
```
struct A {
const int x;
int y;
};
static struct A a;
/*@
assigns a.y;
*/
void f(void)
{
a.y = 1;
}
```
produces:
```
$ frama-c test_global_assign.c
[kernel] Parsing test_global_assign.c (with preprocessing)
[kernel:annot-error] test_global_assign.c:9: Warning:
not an assignable left value: a.y. Ignoring logic specification of function f
[kernel] User Error: warning annot-error treated as fatal error.
[kernel] User Error: stopping on file "test_global_assign.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
```
### Expected behavior
Frama-C should accept the snippet since the `y` field of `a` is mutable.
### Actual behaviour
Code is rejected for `a.y` being non-assignable lvalue. Frama-C seems to treat the entire struct `a` as const, even though only one field is declared const. Removing the `const` specifier from `x` causes Frama-C to accept the code.
### Contextual information
23.1 (Vanadium) via opam on macOS. Does not reproduce on Frama-C 22.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/43Frama-C 22 beta also runs on macOS 11.0.1 Beta ("Big Sur")2021-04-15T11:37:39ZJens GerlachFrama-C 22 beta also runs on macOS 11.0.1 Beta ("Big Sur")This might be of minor interest but Titanium beta also runs on the latest beta-version
of Apple's upcoming macOS 11.0 release.
I only checked WP.
RegardsThis might be of minor interest but Titanium beta also runs on the latest beta-version
of Apple's upcoming macOS 11.0 release.
I only checked WP.
Regardshttps://git.frama-c.com/pub/frama-c/-/issues/2692[alias] expose more functions2024-03-14T10:51:28ZJan Rochel[alias] expose more functionsCopied from https://git.frama-c.com/pub/frama-c/-/issues/2677#note_229339 by @bclement-ocp
Some additional functions need to be exposed in the `Abstract_state` for programmatic use if access to the underlying graph is needed (I need to ...Copied from https://git.frama-c.com/pub/frama-c/-/issues/2677#note_229339 by @bclement-ocp
Some additional functions need to be exposed in the `Abstract_state` for programmatic use if access to the underlying graph is needed (I need to iterate over all equivalence classes, and I think only raw access to the graph allows this).
More precisely:
* `get_lval` / `find_aliases` now only returns variable aliases; there is `reconstruct_lvals` internally to compute all the aliases but it is not exposed (it is used by find_all_aliases, but that also brings aliases from other equivalence classes);
* edge labels are not exposed, so it is not possible to distinguish between pointer and field edges from outside the plugin, making raw access to the graph impossible to do correctly
Would it be possible to expose `EdgeLabel `and (an equivalent of) `reconstruct_lvals` from the plugin's API?Jan RochelJan Rochelhttps://git.frama-c.com/pub/frama-c/-/issues/2691Cannot use ppx_inline_test in a Frama-C plugin2024-02-28T22:02:33Zpepega007xdCannot use ppx_inline_test in a Frama-C plugin<!--
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
Setup a minimal Frama-C plugin which uses the `ppx_inline_tests` test runner, and run tests using `dune runtest`.
The test runner is configured according to this documentation: https://dune.readthedocs.io/en/stable/tests.html#inline-tests
Project structure:
```
hello/
├── dune
├── dune-project
└── hello.ml
```
dune-project:
```
(lang dune 3.2)
(using dune_site 0.1)
(name frama-c-hello)
(package (name frama-c-hello))
```
dune:
```
(library
(name hello)
(public_name frama-c-hello.core)
(libraries frama-c.kernel)
(preprocess (pps ppx_inline_test))
(inline_tests)
)
(plugin
(optional)
(name hello)
(libraries frama-c-hello.core)
(site (frama-c plugins))
)
```
hello.ml:
```ml
let%test "should fail" = 1 = 2
```
### Expected behaviour
The test inside `hello.ml` executes and prints an assertion error.
### Actual behaviour
Building the test fails with the following error:
```
Error: No implementation found for virtual library "frama-c.init" in
/home/tb/.opam/default/lib/frama-c/init.
-> required by library "frama-c.kernel" in
/home/tb/.opam/default/lib/frama-c/kernel
-> required by library "frama-c-hello.core" in _build/default
-> required by
_build/default/.hello.inline-tests/inline_test_runner_hello.exe
-> required by _build/default/.hello.inline-tests/partitions-best
-> required by alias runtest in dune:6
```
### Contextual information
- Frama-C installation mode: installed using `opam install frama-c`
- Frama-C version: 28.0 (Nickel)
- Plug-in used: minimal plugin
- OS name: Fedora Linux
- OS version: 38 (Workstation Edition)
### Additional information (optional)
The project build just fine using `dune build`, only the `@runtest` target fails to build.https://git.frama-c.com/pub/frama-c/-/issues/2690[WP] Frama-C/WP 28.0 does not work with Isabelle/HOL2024-03-06T11:53:41Zkwaxer[WP] Frama-C/WP 28.0 does not work with Isabelle/HOL### Steps to reproduce the issue
1. Make sure Isabelle/HOL is installed and `why3` is configured to use it.
2. Create file `test.h` with the following code:
```
/*@
logic \list<integer> enumeration (integer n) = n == 0 ? \Nil : enu...### Steps to reproduce the issue
1. Make sure Isabelle/HOL is installed and `why3` is configured to use it.
2. Create file `test.h` with the following code:
```
/*@
logic \list<integer> enumeration (integer n) = n == 0 ? \Nil : enumeration (n - 1) ^ [|n - 1|];
lemma enumeration_length: \forall integer n; 0 <= n ==> \length (enumeration (n)) == n;
*/
```
3. Run WP plugin selecting Isabelle/HOL as a backend: `frama-c -wp -wp-prover=why3:isabelle -wp-interactive=fix -wp-cache=none test.h`
### Expected behaviour
Earlier versions of Frama-C (e.g. 27.1) produce the following output:
```
[kernel] Parsing test.h (with preprocessing)
[wp] 1 goal scheduled
[wp] Proved goals: 1 / 1
Qed: 0
Isabelle 2022: 1 (8.1s)
```
with the theory
```isabelle
theory lemma_enumeration_length imports Why3.Why3 begin
why3_open "lemma_enumeration_length.xml"
why3_vc wp_goal
using assms L_enumeration_def
by (induction i) (simp_all add: facts.length_concat length_cons length_nil)
why3_end
end
```
### Actual behaviour
Frama-C 28.0 produces the following:
```
[kernel] Parsing test.h (with preprocessing)
[wp] 1 goal scheduled
[wp] [Failure] typed_lemma_enumeration_length (Isabelle)
[wp] Proved goals: 0 / 1
Qed: 0
Failed: 1
```
### Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *28.0 (Nickel)*
- Plug-in used: *WP*
- OS name: *Ubuntu*
- OS version: *22.04.4 LTS*
### Additional information (optional)
`-wp-msg-key why3_api` gives the following error trace:
```
[wp] Failure: [Why3 Error] anomaly: Sys_error(".../.frama-c/wp/interactive/lemma_enumeration_length/.xml: No such file or directory")
Raised by primitive operation at Stdlib.open_out_gen in file "stdlib.ml", line 331, characters 29-55
Called from Stdlib.open_out in file "stdlib.ml" (inlined), line 336, characters 2-74
Called from Frama_c_kernel__Command.pp_to_file in file "src/libraries/utils/command.ml", line 31, characters 13-35
Called from Wp__ProverWhy3.prepare in file "src/plugins/wp/ProverWhy3.ml", line 1339, characters 6-130
Called from Wp__ProverWhy3.interactive in file "src/plugins/wp/ProverWhy3.ml", line 1352, characters 8-37
Called from Wp__ProverWhy3.build_proof_task in file "src/plugins/wp/ProverWhy3.ml", line 1413, characters 8-59
```
There is an unexpected slash right the before `.xml` file extension.https://git.frama-c.com/pub/frama-c/-/issues/2689[wp] Failing to understand certain bitwise properties2024-02-14T11:19:42ZPhillip Allen Lane[wp] Failing to understand certain bitwise properties<!--
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
I have the following Frama-C which should prove this seemingly trivial assertion about an integer containing all 1s:
```c
#include <stdint.h>
#define ALLONES 0xFFFFFFFFu
/*@
assigns \nothing;
*/
void tests(void)
{
uint32_t allones = ALLONES;
//@ assert \forall uint32_t i ; 0 <= i < 32 ==> (allones & (1u << i)) != 0;
}
```
### Expected behaviour
All goals should be proven.
### Actual behaviour
Running with:
```
frama-c -wp -wp-rte -wp-smoke-tests -wp-prover z3 -wp-par 32 -wp-print test.c
```
I get:
```
[kernel] Parsing test.c (with preprocessing)
[rte:annot] annotating function tests
[wp] 2 goals scheduled
[wp] [Timeout] typed_tests_assert (Qed 0.86ms) (Z3) (Cached)
[wp] [Cache] updated:1
[wp] Proved goals: 3 / 4
Terminating: 1
Unreachable: 1
Qed: 1
Timeout: 1
------------------------------------------------------------
Function tests
------------------------------------------------------------
Goal Assertion (file test.c, line 10):
Assume { (* Goal *) When: (0 <= i) /\ (i <= 31). }
Prove: land(4294967295, lsl(1, i)) != 0.
Prover Z3 4.8.12 returns Timeout (Qed:0.86ms) (2s)
------------------------------------------------------------
Goal Assigns nothing in 'tests':
Prove: true.
Prover Qed returns Valid
------------------------------------------------------------
```
### Contextual information
I have tried other provers (CVC4, Alt-Ergo) and none of them are able to prove the assertion. Looking at some of the Coq axioms generated, I am suspicious that Frama-C is not providing the SMT solvers with enough information about bitwise operations to be able to deduce the conclusion.
When I run Frama-C with a different assertion:
```c
//@ assert \forall uint32_t i ; i == 0 ==> (allones & (1u << i)) != 0;
```
The assertion succeeds (via Qed). This works for all valid values of `i` (e.g., `i in [0 .. 31]`), but fails when I try to quantify over the entire range.
Here's some relevant information that may be helpful:
- Frama-C installation mode: Opam
- Frama-C version: 28.0 (Nickel)
- Plug-in used: WPLoïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2688[wp] Failure: [Why3 Error] anomaly: Not_found2024-01-19T08:10:37ZJulia Lawall[wp] Failure: [Why3 Error] anomaly: Not_foundSee attached files. The output with the command line argument -wp-msg-key why3_api ends with the following. The attached directory contains a make file, so you can just run `make v1`.
```
> [wp:why3_api] of_term prop c_1.F1_cpumask_bi...See attached files. The output with the command line argument -wp-msg-key why3_api ends with the following. The attached directory contains a make file, so you can just run `make v1`.
```
> [wp:why3_api] of_term prop c_1.F1_cpumask_bits[0]=c_0.F1_cpumask_bits[0]
> [wp] Failure: [Why3 Error] anomaly: Not_found
> Raised at Qed__Term.Make.tau_of_arraysort in file
> "src/plugins/qed/term.ml", line 2831, characters 11-26
> Called from Wp__ProverWhy3.of_term in file "src/plugins/wp/ProverWhy3.ml", line 461, characters 14-29
> Called from Wp__ProverWhy3.of_term in file "src/plugins/wp/ProverWhy3.ml", line 450, characters 14-39
> Called from Wp__ProverWhy3.of_term.fold in file "src/plugins/wp/ProverWhy3.ml", line 453, characters 16-44
> Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
> Called from Wp__ProverWhy3.share in file "src/plugins/wp/ProverWhy3.ml", line 633, characters 10-33
> Called from Wp__ProverWhy3.successive_binders in file "src/plugins/wp/ProverWhy3.ml", line 669, characters 8-24
> Called from Wp__ProverWhy3.successive_binders in file "src/plugins/wp/ProverWhy3.ml", line 666, characters 23-49
> Called from Wp__ProverWhy3.successive_binders in file "src/plugins/wp/ProverWhy3.ml", line 666, characters 23-49
> Called from Wp__ProverWhy3.successive_binders in file "src/plugins/wp/ProverWhy3.ml", line 666, characters 23-49
> Called from Wp__ProverWhy3.successive_binders in file "src/plugins/wp/ProverWhy3.ml", line 666, characters 23-49
> Called from Wp__ProverWhy3.successive_binders in file "src/plugins/wp/ProverWhy3.ml", line 666, characters 23-49
> Called from Wp__ProverWhy3.successive_binders in file "src/plugins/wp/ProverWhy3.ml", line 666, characters 23-49
```
[files.tar.gz](/uploads/39c90bd26cf8493c15edcdffa8c55c24/files.tar.gz)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2687Ivette: server not running error2024-01-28T03:46:19ZHugo GimbertIvette: server not running errorHello,
I understand frama-c-gui is not available anymore for MacOSX,
so I tried to move to Ivette.
I performed a fresh install of frama-c
on my laptop (MacBookPro Apple M1 Max with macOs Sonoma).
using brew + opam, following the offi...Hello,
I understand frama-c-gui is not available anymore for MacOSX,
so I tried to move to Ivette.
I performed a fresh install of frama-c
on my laptop (MacBookPro Apple M1 Max with macOs Sonoma).
using brew + opam, following the official guidelines
https://frama-c.com/html/get-frama-c.html
Unfortunately, for the moment I am unable to use the new editor Ivette,
I cannot add any source file to the workspace.
There is a red blinking dot plus a warning sign at the bottom left of the editor
but I do not know how to interpret that.
When I open developper tools, I can see an error "Server not running" but I do not know which Server should be running.
Below is a screen shot of the problem
![image](/uploads/3329bfe5feef0132326781e04aa19af4/image.png)
What is the procedure to start the frama-c server required by Ivette?
Any help appreciated.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2686Frama-C cannot use Alt-Ergo 2.5.x by default with Why3 1.7.02024-01-11T12:34:19ZHugo GimbertFrama-C cannot use Alt-Ergo 2.5.x by default with Why3 1.7.0Installing Frama-C on Ubuntu 22.04 with opam consistently fails on several machines,
including mine and all of my student's using Ubuntu 22.04.
A solution is to downgrade from fraam-28.0 to framac-26.0.
Current patch for installing on ...Installing Frama-C on Ubuntu 22.04 with opam consistently fails on several machines,
including mine and all of my student's using Ubuntu 22.04.
A solution is to downgrade from fraam-28.0 to framac-26.0.
Current patch for installing on Ubuntu 22.04:
- follow the instructions at https://frama-c.com/html/get-frama-c.html
- opam remove --force frama-c
- opam install frama-c.26.0
- why3 config detectAllan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2685[WP] save / load not saving strategies2023-12-14T10:13:17ZTeo BERNIER[WP] save / load not saving strategies### Steps to reproduce the issue
On the attached examples :
[test.c](/uploads/8a2ca334a3a2ef8d696da2df986bdd45/test.c)
running the following command
`frama-c test.c -wp -wp-prover=tip -wp-prop post`
works perfectly, but when we u...### Steps to reproduce the issue
On the attached examples :
[test.c](/uploads/8a2ca334a3a2ef8d696da2df986bdd45/test.c)
running the following command
`frama-c test.c -wp -wp-prover=tip -wp-prop post`
works perfectly, but when we use the save / load features with the following command (and after removing the existing scripts)
`frama-c test.c -save tmp.sav ; frama-c -load tmp.sav -wp -wp-prover=tip -wp-prop post`
it does not work anymore and, when we add option
`-wp-strategy InstanceForall`,
Frama-C outputs
`[wp] Warning: Invalid -wp-strategy 'InstanceForall' (undefined strategy name)`
### Expected behaviour
We would expect save / load to keep strategies available.
### Actual behaviour
Strategies seems to not be correctly saved / loaded and when specified, they are declared `undefined` by WP.
### Contextual information
* Frama-C installation mode: opam install frama-c.28.0
* Frama-C version: 28.0
* Plug-in used: WP with why3 1.6.0 and Alt-Ergo 2.4.3
* OS name: Ubuntu
* OS version: 20.04
FYI: @nkosmatovhttps://git.frama-c.com/pub/frama-c/-/issues/2684[WP] crash observed with scripts and strategies2023-12-14T10:28:20ZNikolai Kosmatov[WP] crash observed with scripts and strategies### Expected behaviour
No crash
### Actual behaviour
Crash in some situations when running WP in the presence of existing scripts recorded via strategies.
Here is a screenshot (with a hidden full file name).
![crash_on_recorded_scri...### Expected behaviour
No crash
### Actual behaviour
Crash in some situations when running WP in the presence of existing scripts recorded via strategies.
Here is a screenshot (with a hidden full file name).
![crash_on_recorded_scripts](/uploads/11287a2731db4ea55108b4395f95b940/crash_on_recorded_scripts.png)
### Contextual information
- Frama-C installation mode: *Opam from public GIT*
- Frama-C version: *28.0+dev (Nickel)* commit cdd528, similar behavior observed on 28.0beta
- Plug-in used: *WP*
- OS name: *Ubuntu*
- OS version: *22.04*
FYI @tbernierhttps://git.frama-c.com/pub/frama-c/-/issues/2683[WP] non-matching of strategies with forall and implication2023-11-27T09:24:34ZTeo BERNIER[WP] non-matching of strategies with forall and implication### Steps to reproduce the issue
On the attached examples :
- [forall_pattern.c](/uploads/2df4b07af5737279a5d34001b7d10822/forall_pattern.c)
running the following command
`frama-c-gui forall_pattern.c -wp -wp-rte -wp-prover...### Steps to reproduce the issue
On the attached examples :
- [forall_pattern.c](/uploads/2df4b07af5737279a5d34001b7d10822/forall_pattern.c)
running the following command
`frama-c-gui forall_pattern.c -wp -wp-rte -wp-prover=tip -wp-prop post`
to apply a strategy with Instance does not seem to accept the pattern and to match the precondition using `\forall`.
```
strategy FastAltErgo: \prover("alt-ergo", 1); // run Alt-Ergo for 1 sec.
strategy InstanceForall:
\tactic("Wp.instance",
\pattern(\forall integer _; _), // fails to select the \forall (invalid pattern)
// \when(_), // works in this specific example
\goal(P_P(i)),
\param("P1", i),
\children(FastAltErgo)
);
proof InstanceForall: post;
```
- [implication_pattern.c](/uploads/8c4a42b5917b980ffe994189507fb7c6/implication_pattern.c)
running the following command
`frama-c-gui implication_pattern.c -wp -wp-rte -wp-prover=tip -wp-prop post`
to apply a strategy with Cut does not seem to accept the pattern and to match the precondition using `==>`.
```
strategy FastAltErgo: \prover("alt-ergo", 1); // run Alt-Ergo for 1 sec.
strategy CutImplication:
\tactic("Wp.cut",
\pattern(A ==> _), // fails to select the implication (invalid pattern)
// \incontext(A: _ <= 99), // works in this specifi example
\param("case", "CASES"),
\param("clause", A),
\children(FastAltErgo)
);
proof CutImplication: post;
```
### Expected behaviour
We would expect `\forall` and `==>` to be matched like other acsl expression.
### Actual behaviour
Syntax error is reported (Invalid pattern. Ignoring global annotation).
### Contextual information
- Frama-C installation mode: opam pin add frama-c https://git.frama-c.com/pub/frama-c.git#64438ed52f9af0052d6f3970202fc48dbc580dba
- Frama-C version: 28.0+dev (commit 64438ed52f9af0052d6f3970202fc48dbc580dba)
- Plug-in used: WP with why3 1.6.0 and Alt-Ergo 2.5.2
- OS name: Ubuntu
- OS version: 22.04
FYI: @nkosmatovLoïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2682[WP] Preservation of "is_finite" property2023-11-24T10:40:34ZArnaud Fontaine[WP] Preservation of "is_finite" property### Steps to reproduce the issue
Run the following example with the command
`frama-c -wp-model typed+int+float -wp-rte -wp-timeout 5 -wp test.c`
```
#include <__fc_builtin.h>
/*@
@requires \valid(vec + (0 .. (size - 1)));
@require...### Steps to reproduce the issue
Run the following example with the command
`frama-c -wp-model typed+int+float -wp-rte -wp-timeout 5 -wp test.c`
```
#include <__fc_builtin.h>
/*@
@requires \valid(vec + (0 .. (size - 1)));
@requires \forall unsigned i; i < size ==> \is_finite(vec[i]);
@requires \forall unsigned i; i < size ==> !\is_NaN(vec[i]);
@terminates \true;
@ensures \forall unsigned i; i < size ==> \is_finite(vec[i]);
@ensures \forall unsigned i; i < size ==> !\is_NaN(vec[i]);
@ensures \forall unsigned i; i < size ==> vec[i] == \old(vec)[i];
@assigns vec[0 .. (size - 1)];
@*/
extern void vec_nop(double * const vec, unsigned const size);
void vec_nop(double * const vec, unsigned const size) {
/*@
@loop invariant i <= size;
@loop invariant \forall unsigned x; x < i ==> \is_finite(vec[x]);
@loop invariant \forall unsigned x; x < i ==> !\is_NaN(vec[x]);
@loop invariant \forall unsigned x; x < i ==> vec[x] == \at(vec, LoopEntry)[x];
@loop assigns i;
@loop variant (size - i);
@*/
for (unsigned i = 0; i < size; ++i) {
}
}
/*@
@requires \valid(vec + (0 .. (size - 1)));
@requires \forall unsigned i; i < size ==> \is_finite(vec[i]);
@requires \forall unsigned i; i < size ==> !\is_NaN(vec[i]);
@terminates \true;
@ensures \forall unsigned i; i < size ==> \is_finite(vec[i]);
@ensures \forall unsigned i; i < size ==> !\is_NaN(vec[i]);
@ensures \forall unsigned i; i < size ==> vec[i] == \old(vec)[i];
@assigns vec[0 .. (size - 1)];
@*/
extern void vec_ident(double * const vec, unsigned const size);
void vec_ident(double * const vec, unsigned const size) {
/*@
@loop invariant i <= size;
@loop invariant \forall unsigned x; x < i ==> \is_finite(vec[x]);
@loop invariant \forall unsigned x; x < i ==> !\is_NaN(vec[x]);
@loop invariant \forall unsigned x; x < i ==> vec[x] == \at(vec, LoopEntry)[x];
@loop assigns i;
@loop assigns vec[0 .. (size - 1)];
@loop variant (size - i);
@*/
for (unsigned i = 0; i < size; ++i) {
vec[i] = vec[i];
}
}
```
### Expected behaviour
All properties should be validated.
### Actual behaviour
In the given example, all properties of the `vec_nop` are correctly verified with WP. However, in the `vec_ident` function below where the only difference with the `vec_nop` function is the addition of the statement `vec[i] = vec[i];` in the loop, the loop invariant `\is_finite(vec[x])` is not verified anymore.
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 27.1 (Cobalt)
- Plug-in used: WP
- OS name: Linux
### Additional information (optional)
When using model `typed+int+real` all properties are validated...Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2681[kernel] Conflicting types error for enum & typedef enum2024-01-17T11:25:46ZT-Gruber[kernel] Conflicting types error for enum & typedef enumI have encountered a problem that leads to an error when parsing. This occurs when an enum is defined multiple times as shown below. The expectation would be that it works as with the struct shown:
- forward declaration of struct/enum
- ...I have encountered a problem that leads to an error when parsing. This occurs when an enum is defined multiple times as shown below. The expectation would be that it works as with the struct shown:
- forward declaration of struct/enum
- introducing an alias via typedef
- both in one
```C
// test.c
// works
struct my_struct;
typedef struct my_struct my_struct;
typedef struct my_struct {
int val;
} my_struct;
// fails
enum my_enum;
typedef enum my_enum my_enum;
typedef enum my_enum {
VAL
} my_enum;
```
### Steps to reproduce the issue
Parse source file:
```
frama-c test.c
```
### Expected behaviour
Output:
```
[kernel] Parsing test.c
```
### Actual behaviour
Output:
```
[kernel] Parsing test.c
[kernel] test.c:14: User Error:
redefinition of type 'my_enum' in the same scope with conflicting type.
Previous declaration was at test.c:10
[kernel] User Error: stopping on file "test.c" that has errors.
[kernel] Frama-C aborted: invalid user input.
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 27.0 (Cobalt)
- OS: Ubuntu 22.04.2 LTS (WSL)