frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2024-03-06T11:53:41Zhttps://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/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/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/2673[WP] non-matching of strategies with logical operators2024-03-04T10:14:59ZNikolai Kosmatov[WP] non-matching of strategies with logical operators### Steps to reproduce the issue
On the attached example
[logical_pattern.c](/uploads/0bb48f222b06fb2a470e76d756be35f0/logical_pattern.c)
running the following command
`frama-c-gui logical_pattern.c -wp -wp-rte -wp-prover=alt-ergo,...### Steps to reproduce the issue
On the attached example
[logical_pattern.c](/uploads/0bb48f222b06fb2a470e76d756be35f0/logical_pattern.c)
running the following command
`frama-c-gui logical_pattern.c -wp -wp-rte -wp-prover=alt-ergo,tip -wp-timeout 1 -wp-prop post`
to apply a strategy with Split does not seem to accept the pattern and to match the precondition with logical operations `&&` and `||`
```
strategy FastAltErgo: \prover("alt-ergo", 1); // run Alt-Ergo for 1 sec.
strategy EagerAltErgo: \prover("alt-ergo",10); // run Alt-Ergo for 10 sec.
strategy SplitProver:
FastAltErgo,
\tactic("Wp.split"
,\pattern( ((A && B) || (C && D)) )
,\children(EagerAltErgo)
),
EagerAltErgo;
proof SplitProver: post;
```
### Expected behaviour
According to documentation, ACSL logical operations are recognized and after a successful matching, a script is created with two subgoals (to be completed).
### Actual behaviour
Syntax error is reported (Invalid pattern. Ignoring global annotation).
### Contextual information
- Frama-C installation mode: opam from GIT pub
- Frama-C version: first version of the strategy mechanism (https://git.frama-c.com/pub/frama-c.git#3396bd), also the recent update on master on pub (by the branch fix/wp/strategies)
- Plug-in used: WP with Why3 1.6.0 and Alt-Ergo 2.4.3
- OS name: Ubuntu
- OS version: 22.04Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2663Parse-print-reparse error with WP strategies2023-07-21T09:11:17ZNikolai KosmatovParse-print-reparse error with WP strategies## Contextual information: currently used versions
- Frama-C installation mode: *Opam*
- Frama-C version 27.0dev (tested commit: 3396bd)
- Alt-Ergo 2.4.3
- OS name: *Ubuntu*
- OS version: *20.04*
## The issue
On the attached file, aft...## Contextual information: currently used versions
- Frama-C installation mode: *Opam*
- Frama-C version 27.0dev (tested commit: 3396bd)
- Alt-Ergo 2.4.3
- OS name: *Ubuntu*
- OS version: *20.04*
## The issue
On the attached file, after parsing and printing the code, running frama-c again to parse the code produces an error (due to missing parentheses around a list of arguments (..)).
[strategy.c](/uploads/d089f42a7b3f32480a9d03227f201f0a/strategy.c)
Commands used:
`frama-c strategy.c -print -no-unicode -ocode pp_strategy.c`
`frama-c pp_strategy.c`Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2657frama-c-gui frozen and why3 not found2023-04-13T14:44:13ZRongframa-c-gui frozen and why3 not found### Problem Description ###
When running `opam install alt-ergo`, my terminal shows:
```
Package alt-ergo is already installed (current version is 2.4.2).
```
However, when running `frama-c-gui -wp -rte -main.c`, the terminal shows:
...### Problem Description ###
When running `opam install alt-ergo`, my terminal shows:
```
Package alt-ergo is already installed (current version is 2.4.2).
```
However, when running `frama-c-gui -wp -rte -main.c`, the terminal shows:
```
(frama-c-gui:4023): GLib-CRITICAL **: 09:36:25.664: Source ID 8 was not found when attempting to remove it.
```
The GUI is opened but frozen. No clicking is responded and the console shows `User Error: Prover 'alt-ergo' not found in why3.conf.`
### Steps to reproduce the issue
frama-c-gui -wp -rte -main.c
### Expected behaviour
open the window of frama-c-gui and run normally
### Actual behaviour
The GUI is opened but frozen. No clicking is responded and the console shows `User Error: Prover 'alt-ergo' not found in why3.conf.`
### Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *frama-c.26.1*
- Plug-in used: *Plug-in used*
- OS name: *Ubuntu*
- OS version: *22.04.2 LTS*
### Additional information (optional)
After running "opam upgrade", the following information appears:
```
Everything as up-to-date as possible (run with --verbose to show unavailable upgrades).
The following packages are not being upgraded because the new versions conflict with other installed packages:
- ocaml-config.3
- ocplib-simplex.0.5
∗ alt-ergo-lib.2.4.2 is installed and requires ocplib-simplex (>= 0.4 & < 0.5)
- why3.1.6.0
∗ frama-c.26.1 is installed and requires why3 (>= 1.5.1 & < 1.6~)
However, you may "opam upgrade" these packages explicitly, which will ask permission to downgrade or uninstall the conflicting packages.
Nothing to do.
# Run eval $(opam env) to update the current shell environment
```https://git.frama-c.com/pub/frama-c/-/issues/2650Stack overflow using WP in Wp__Register.step_finally2023-03-29T20:08:35ZChristophe GarionStack overflow using WP in Wp__Register.step_finallyFrama-C 26.1 and its WP plugin crash with a stack overflow when trying to prove a function:
```
The full backtrace is:
Raised at Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 834, characters 41-48
Called fro...Frama-C 26.1 and its WP plugin crash with a stack overflow when trying to prove a function:
```
The full backtrace is:
Raised at Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 834, characters 41-48
Called from Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 835, characters 2-12
Called from Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 835, characters 2-12
Called from Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 835, characters 2-12
Called from Stdlib__Queue.iter.iter in file "queue.ml", line 121, characters 6-15
Called from Frama_c_boot__Boot.play_analysis in file "src/init/boot/boot.ml", line 36, characters 4-20
Called from Frama_c_kernel__Cmdline.play_in_toplevel_one_shot in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 850, characters 2-9
Called from Frama_c_kernel__Cmdline.play_in_toplevel in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 880, characters 18-64
Called from Frama_c_kernel__Cmdline.catch_toplevel_run in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 233, characters 4-8
Unexpected error (Stack overflow).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 26.1 (Iron).
```
The function to be proved is part of a rather big C file included in the attached archive. Sorry for the complexity (and maybe the bad quality) of the C code, it is in fact produced by a Lustre compiler we are working on. I will try to produce a real MWE...
Running Frama-C and WP on the whole file causes a stack overflow on `List.map` but I reduce the error when proving the `Arrays1_Arrays1_node_step` function. I use the `ref` and the `real` memory model.
When launching Frama-C on the function, no goal is produced (at least there is no printing of it), only Frama-C is running (there is no process involving Alt-Ergo or Z3 for instance). the crash happens after 13 minutes (!) on my computer (a recent laptop with i9 cores).
### Steps to reproduce the issue
* open the attached archive
* issue the following command:
```
frama-c -wp -wp-model ref,real -wp-fct Arrays1_Arrays1_node_step Arrays1.c
```
### Contextual information
- Frama-C installation mode: opam with an OCaml 4.14.0 switch
- Frama-C version: 26.1 (Iron)
- Plug-in used: WP
- OS name: Linux
- OS version: 22.04
Thanks,
Christophe
[arrays_stack_overflow_wo_optimization.tgz](/uploads/e88a0fcabd4de811d59024517c679f5d/arrays_stack_overflow_wo_optimization.tgz)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2644[WP] Fails to verify left shift by 2 on range2023-01-24T11:13:25ZCostava[WP] Fails to verify left shift by 2 on range<!--
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.
-->
```c
/*@
requires a == 1;
assigns \nothing;
ensures \result == (a << 2);
*/
unsigned int do_one(const unsigned int a) {
return (a << 2);
}
/*@
requires a == 2;
assigns \nothing;
ensures \result == (a << 2);
*/
unsigned int do_two(const unsigned int a) {
return (a << 2);
}
/*@
requires 1 <= a <= 2;
assigns \nothing;
ensures \result == (a << 2);
*/
unsigned int do_some_shift2(const unsigned int a) {
return (a << 2);
}
/*@
requires 1 <= a <= 2;
assigns \nothing;
ensures \result == (a << 1);
*/
unsigned int do_some_shift1(const unsigned int a) {
return (a << 1);
}
```
```sh
$ frama-c -wp -wp-rte fcshift.c
```
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
All goals verified successfully.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
```sh
$ frama-c -wp -wp-rte fcshift.c
[kernel] Parsing fcshift.c (with preprocessing)
[rte:annot] annotating function do_one
[rte:annot] annotating function do_some_shift1
[rte:annot] annotating function do_some_shift2
[rte:annot] annotating function do_two
[wp] 8 goals scheduled
[wp] [Alt-Ergo 2.4.1] Goal typed_do_some_shift2_ensures : Timeout (Qed:2ms) (10s)
[wp] Proved goals: 7 / 8
Qed: 6 (0.33ms-0.64ms-2ms)
Alt-Ergo 2.4.1: 1 (10ms) (92) (interrupted: 1)
```
The ensures goal can be verified when `a` has a single value of either `1` or `2` respectively for the `do_one` and `do_two` functions.
But if `a` is `1` or `2` (for function `do_some_shift2`), then the ensures goal fails to verify.
Oddly, the goal succeeds if the left shift is by `1` instead of `2` (function `do_some_shift1`).
[cppreference.com](https://en.cppreference.com/w/c/language/arithmetic_types) is stating that `unsigned int` should always have at least 16 bits, so it is weird to me that changing the amount of the shift is making a difference.
Doubling the timeout to 20 does not make the goal succeed automatically.
Using `frama-c-gui`, I know that I can apply tactic `Logical Shift` on `lsl(a, 2)` in order to make the goal succeed, but a goal that is this specific and simple failing to verify seems like a bug.
### Contextual information
- Frama-C installation mode: opam
- Frama-C version: 25.0 (Manganese)
- Plug-in used: WP, RTE, Alt-Ergo 2.4.1
- OS name: Manjaro Linux
- OS version: Sikaris 22.0.0
### 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.
-->
N/ALoïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2636[WP] Builtin \sign(float64) is not defined2022-12-14T12:36:37ZNiksonber[WP] Builtin \sign(float64) is not defined<!--
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]…
-->
### Description
Built-in \\sign is not defined in WP.
`Builtin \sign(float64) not defined`
`[wp] Failure: Logic type 'sign' undefined`
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
### Steps To Reproduce
Run: `frama-c -wp -wp-out . -wp-prover coq -wp-model +float -wp-interactive update just_sign.c`
Where `just_sign.c` is:
```
#include <math.h>
/*@
predicate is_same_sign(double X, double Y) = \sign(X) == \sign(Y);
*/
/*@
ensures (is_same_sign(a_double, \result)) ;
assigns \nothing;
*/
double dummy (double a_double) {
return a_double;
}
```
I got the following output:
```
[wp] Warning: Missing RTE guards
[wp] just_sign.c:4: Warning: Builtin \sign(float64) not defined
[wp] just_sign.c:4: Warning: Builtin \sign(float64) not defined
[wp] 2 goals scheduled
[wp] Failure: Logic type 'sign' undefined
```
### Expected behaviour
Expected a definition for \sign.
<!--
Please explain here what is the expected behaviour.
-->
### Actual behaviour
WP reports:
```
[wp] Failure: Logic type 'sign' undefined
[wp] just_sign.c:4: Warning: Builtin \sign(float64) not defined
```
<!--
Please explain here what is the actual (faulty) behaviour.
-->
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 24.0, 25.0 (Manganese), 26.0+dev (Iron) (I tried Several versions)
- Plug-in used: WP
- OS name: Ubuntu
- OS version: 22.04 LTS
<!--
### 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.
-->Allan BlanchardAllan Blanchardhttps://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/2629Anomalous behavior of anonymous 'behavior'2022-09-22T08:58:47ZDavid CokAnomalous behavior of anonymous 'behavior'
### Steps to reproduce the issue
See this code:
```
int P;
int Q;
/*@
requires P != 0;
behavior always:
assigns Q;
ensures Q == 1;
complete behaviors always;
*/
void b() {
Q = 1;
}
//@ assigns Q;
void a() {
b();
}
...
### Steps to reproduce the issue
See this code:
```
int P;
int Q;
/*@
requires P != 0;
behavior always:
assigns Q;
ensures Q == 1;
complete behaviors always;
*/
void b() {
Q = 1;
}
//@ assigns Q;
void a() {
b();
}
/*@
requires P != 0;
assigns Q;
ensures Q == 1;
*/
void d() {
Q = 1;
}
//@ assigns Q;
void c() {
d();
}
```
which is an minimal as I could make it.
Note that a calls b, where b has a always-true behavior. c calls d the same way, but without a behavior.
The example is extracted from a larger specification with lots of behaviors.
### Actual behaviour
In my environment, the above, run with `frama-c -wp` produces
```
fc $ frama-c -wp behavior.c
[kernel] Parsing behavior.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 11 goals scheduled
[wp] [Alt-Ergo 2.4.1] Goal typed_a_assigns_exit : Timeout (Qed:0.81ms) (10s)
[wp] [Alt-Ergo 2.4.1] Goal typed_a_call_b_requires : Timeout (Qed:0.78ms) (10s)
[wp] [Alt-Ergo 2.4.1] Goal typed_a_assigns_normal : Timeout (Qed:0.77ms) (10s)
[wp] [Alt-Ergo 2.4.1] Goal typed_c_call_d_requires : Timeout (10s)
[wp] Proved goals: 7 / 11
Qed: 7
Alt-Ergo 2.4.1: 0 (interrupted: 4)
```
That is c calling d is fine. a calling b is not.
### Expected behaviour
I expect a calling be to behave precisely like c calling d.
It appears that even with a prefix consisting of just requires clauses, WP produces an
anonymous behavior that contains something like `assigns \everything`. That then causes
the very mysterious assigns errors that you see above.
Fortunately, now that I know the problem there is an easy workaround -- but prior to that it wasted many days of time.
### Contextual information
Frama-C 25.0, built from source, with WP
MacOS 12.5Loïc CorrensonLoïc Corrensonhttps://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/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/2575[WP] Soundness issue when handling a pointer on a structure containing an array.2021-10-06T07:07:23ZAlexCid[WP] Soundness issue when handling a pointer on a structure containing an array.<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
Save the following code into a file called "error.c":
```C
#include <__fc_builtin.h>
struct slice {
int len;
char *buf;
};
int main() {
char b[4] = {0};
struct slice s = {.len = Frama_C_int_interval(2, 100000), .buf=b};
struct slice *p = &s;
//@ assert \valid_read(p->buf + (0..(p->len-1)));
return (int)p->buf[p->len-1];
}
```
Then analyse this code using the WP plugin with the command
`frama-c error.c -eva -wp -wp-rte -wp-prover alt-ergo`
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
### Expected behaviour
The assertion `//@ assert \valid_read(p->buf + (0..(p->len-1)));` does obviously not hold and should be rejected by WP.
<!--
Please explain here what is the expected behaviour.
-->
### Actual behaviour
The manually added assertion, as well as the RTE assertion generated by wp-rte, are proved by alt-ergo. Using a different prover (z3, cvc4) yields the same result.
<!--
Please explain here what is the actual (faulty) behaviour.
-->
### Contextual information
- Frama-C installation mode: docker
- Frama-C version: 23.1
- Plug-in used: Eva, WP
- OS name: Ubuntu
- OS version: 20.04
### Additional information (optional)
Handling a pointer on a structure containing the array is required to trigger the bug - a simple structure containing the array won't trigger it.
This bug can also be triggered in a slightly more complex setting, where the array access is done in a second function and the `assert` clause is replaced by an equivalent `requires` clause in the preconditions of that second function.
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2548Error: Unbound value Why3.Whyconf.load_default_config_if_needed2021-04-13T17:49:41ZQixError: Unbound value Why3.Whyconf.load_default_config_if_needed
Before submitting the issue, please confirm (by adding a X in the [ ]):
- [x] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [ ] the issue has not yet been reported on our old
[BTS](htt...
Before submitting the issue, please confirm (by adding a X in the [ ]):
- [x] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [ ] the issue has not yet been reported on our old
[BTS](https://bts.frama-c.com) (*note: the old BTS is deprecated*); **(Can't tell; getting a database connection error)**
- [ ] you installed Frama-C as prescribed in the [instructions](INSTALL.md). **(Not exactly; I'm building from source within a Dockerfile)**
# Contextual information
- Frama-C installation mode: from source
- Frama-C version: c4d10fb975d443e3c40289843fae89c424b54e63
- Plug-in used: WP
- OS name: Debian Buster
- OS version: 20210326 (10.8)
# Steps to reproduce the issue
Dockerfile:
```Dockerfile
FROM debian:buster-20210326 AS base
RUN apt update -y
RUN apt install -y gnupg2 wget apt-transport-https ca-certificates
RUN wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key | apt-key add -
RUN bash -c "cat >> /etc/apt/sources.list <<< \"deb http://apt.llvm.org/buster/ llvm-toolchain-buster main\""
RUN bash -c "cat >> /etc/apt/sources.list <<< \"deb-src http://apt.llvm.org/buster/ llvm-toolchain-buster main\""
RUN bash -c "cat >> /etc/apt/sources.list <<< \"deb http://apt.llvm.org/buster/ llvm-toolchain-buster-12 main\""
RUN bash -c "cat >> /etc/apt/sources.list <<< \"deb-src http://apt.llvm.org/buster/ llvm-toolchain-buster-12 main\""
RUN cat /etc/apt/sources.list
RUN apt update -y
RUN apt install -y clang-12 lld-12 grub-common ninja-build git libssl-dev libgmp-dev pkg-config make m4 unzip tar bzip2 gcc g++ autoconf zlib1g-dev time
RUN cc --version
RUN c++ --version
WORKDIR /opam
RUN wget https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh
RUN echo "/opam" | sh install.sh --no-backup
ENV PATH="/opam:/opam/bin:${PATH}"
RUN opam --version
RUN time opam init -y --disable-sandboxing --jobs=1
RUN time opam install -y depext ocamlfind ocamlgraph zarith yojson why3.1.4.0 alt-ergo.2.4.0
ENV PATH="/root/.opam/default/bin:${PATH}"
RUN why3 --version
RUN why3 config detect
ARG FRAMAC_REF=c4d10fb975d443e3c40289843fae89c424b54e63
WORKDIR /framac
RUN git init .
RUN git remote add origin https://git.frama-c.com/pub/frama-c.git
RUN git fetch origin ${FRAMAC_REF}
RUN git checkout ${FRAMAC_REF}
RUN autoconf
RUN ./configure
RUN make -j4
RUN make install
RUN frama-c --version; echo
```
# Expected behaviour
Should build to completion.
# Actual behaviour
```
File "src/plugins/wp/Why3Provers.ml", line 31, characters 19-61:
31 | let config = Why3.Whyconf.load_default_config_if_needed config in
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Unbound value Why3.Whyconf.load_default_config_if_needed
make: *** [share/Makefile.generic:78: src/plugins/wp/Why3Provers.cmo] Error 2
make: *** Waiting for unfinished jobs....
The command '/bin/sh -c make -j4' returned a non-zero code: 2
```
---
Some context: Trying to verify a new toy OS and having a bunch of issues since I can't use the standard C library that ships with Frama-C (as there is no C library available in this environment) so I've ended up copying the axiomatic clauses from the `__fc_xxx.h` headers directly.
I saw on StackOverflow that a few bugs that seemed to be affecting me were recently patched on master but not yet released, so I spun up a Dockerfile in order to try to see if any of the verification could be fixed by trying it with the latest head.
However, it doesn't seem to be working - much less getting even simple programs to verify correctly :/ Hence why I'm trying to update everything to latest to see if I can't get _any_ verification to work.
Anyway this is the latest issue I've hit trying to get everything up to date.
Note that there is a lot of stuff in there that isn't directly related to this bug - this is a stripped down Dockerfile, and there is a bunch of extra stuff that comes after this step that I removed to keep things small.https://git.frama-c.com/pub/frama-c/-/issues/2547"Unknown Error" with Alt-Ergo2021-06-01T11:23:20ZQix"Unknown Error" with Alt-ErgoBefore submitting the issue, please confirm (by adding a X in the [ ]):
- [x] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [X] the issue has not yet been reported on our old
[BTS](http...Before submitting the issue, please confirm (by adding a X in the [ ]):
- [x] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [X] the issue has not yet been reported on our old
[BTS](https://bts.frama-c.com) (*note: the old BTS is deprecated*);
- [X] you installed Frama-C as prescribed in the [instructions](INSTALL.md).
# Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *21.1 (Scandium)*
- Plug-in used: *wp*
- OS name: *Windows (via WSL 1)*
- OS version: *Windows 10 Pro build 19041.685*
I have also done `rm -f ~/.why3.conf; why3 config --detect --full-config` quite a few times now.
# Steps to reproduce the issue
Just creating a simple C file called `swap.c`:
```c
/*@
requires \valid(a) && \valid(b);
assigns *a, *b;
ensures *a == \old(*b);
ensures *b == \old(*a);
*/
void swap(int *a, int *b) {
int tmp = *a;
*a = *b;
*b = tmp;
}
int main() {
int a = 42;
int b = 37;
swap(&a, &b);
//@ assert a == 37 && b == 42;
return 0;
}
```
And running it with
```shell
frama-c -wp swap.c
```
# Expected behaviour
All goals proven.
# Actual behaviour
Alt-Ergo gives an `Unknown error`.
```
[kernel] Parsing swap.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
[wp] [Alt-Ergo 2.2.0] Goal typed_swap_ensures : Failed
Unknown error
[wp] Proved goals: 5 / 6
Qed: 5
Alt-Ergo 2.2.0: 0 (failed: 1)
```
I'm seeing this happen with a much larger project for just about every single goal there, too. I cannot verify a single C program with ACSL annotations, it seems.
# Fix ideas
No idea. I can't seem to find any information about this aside from a single unanswered StackOverflow question.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/46Question: Dump why3 file generated by frama-c2023-06-05T07:47:25ZLeo ViezensQuestion: Dump why3 file generated by frama-cHey, <br>
if I proove a file with the wp plugin, the C code gets transpiled into WhyML, is that right? <br>
If so, is it already possible, to dump the generated WhyML into a file? <br>
Thank you for your help.Hey, <br>
if I proove a file with the wp plugin, the C code gets transpiled into WhyML, is that right? <br>
If so, is it already possible, to dump the generated WhyML into a file? <br>
Thank you for your help.https://git.frama-c.com/pub/frama-c/-/issues/41Z3 and CVC4 working for Frama-C 22 (Titanium) beta after some initial problems2021-04-13T17:49:41ZJens GerlachZ3 and CVC4 working for Frama-C 22 (Titanium) beta after some initial problems**I updated the title after figuring out a solution**
- [x] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [x] the issue has not yet been reported on our [BTS](https://bts.frama-c.com);
- ...**I updated the title after figuring out a solution**
- [x] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [x] the issue has not yet been reported on our [BTS](https://bts.frama-c.com);
- [x] you installed Frama-C as prescribed in the [instructions](INSTALL.md).
# Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *22.0-beta (Titanium)*
- Plug-in used: *WP*
- OS name: *Xubuntu*
- OS version: *Ubuntu 20.04.1 LTS*
*Please add specific information deemed relevant with regard to this issue.*
I am able to use the options `-wp-prover Alt-Ergo -wp-prover native:coq ` with *ACSL by Example*.
However when using either `-wp-prover Z3` or `-wp-prover z3` I receive the following error message.
(Note that `z3` (4.8.6) has been installed and that it has been successfully registered with `why3 config --full-config`)
```
[kernel] Parsing find.c (with preprocessing)
[rte] annotating function find
[wp] User Error: Prover 'z3' not found in why3.conf
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 25 goals scheduled
[wp] Proved goals: 25 / 25
Qed: 16 (2ms-6ms-20ms)
Alt-Ergo 2.3.3: 9 (5ms-12ms) (87)
[wp] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Plug-in wp aborted: invalid user input.
```
Similar with `CVC4` and `cvc4`.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/55z3 ERROR: unknown parameter 'model_compress'2021-02-22T12:52:03Zrwmjonesz3 ERROR: unknown parameter 'model_compress'ID0002509:
**This issue was created automatically from Mantis Issue 2509. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002509:
**This issue was created automatically from Mantis Issue 2509. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002509 | Frama-C | Plug-in > wp | public | 2020-10-15 | 2020-10-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | rwmjones | **Assigned To** | correnson | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Apparently z3 dropped this parameter and replaced it with "model.compact" without bothering with backward compatibility: https://github.com/Z3Prover/z3/issues/2704#issuecomment-554489258
### Steps To Reproduce :
Use z3 4.8.9, turn on debugging.
<6.827036,call_prover>Call_provers: actual command is:
z3 -smt2 -t:10000 sat.random_seed=42
model_compress=false nlsat.randomize=false
smt.random_seed=42 -st
/tmp/why_b9efc2_zilch-T-wp_goal.smt2
ERROR: unknown parameter 'model_compress'