frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2022-09-22T08:58:47Zhttps://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/2621[Frama-C/WP] The history of internal state changes VC goal outcomes2022-09-26T13:49:51Zstephengaito[Frama-C/WP] The history of internal state changes VC goal outcomes### Steps to reproduce the issue
Using Allan Blanchard's answer to exercise 3.1.3.3 (file: `code/function-contract/contract/ex-3-alphabet-answer.c`)...
Start `frama-c-gui code/function-contract/contract/ex-3-alphabet-answer.c`.
Right-...### Steps to reproduce the issue
Using Allan Blanchard's answer to exercise 3.1.3.3 (file: `code/function-contract/contract/ex-3-alphabet-answer.c`)...
Start `frama-c-gui code/function-contract/contract/ex-3-alphabet-answer.c`.
Right-click on the function prototype `int alphabet_letter` and select `Prove function annotations by WP`, the first VC (`ensures`) should fail.
Right-click on the function prototype `int alphabet_letter` a second time and select `Prove function annotations by WP`, the first VC (`ensures`) should succeed.
### Expected behaviour
The order in which WP proof invocations *should* *not* change the VC goal outcomes if there is no change to the underlying code/annotations.
### Actual behaviour
The history of WP proof invocations does seem to change the VC goal outcomes.
### Contextual information
- Frama-C, Why3, Alt-Ergo installation mode: *all via Opam*
- Frama-C version: *25.0-beta (Manganese)*
- Plug-in used: *WP*
- Why3 version: *Why3 platform, version 1.5.0*
- Alt-Ergo version: *2.4.1*
- OS name: *Ubuntu*
- OS version: *21.10 (Impish)*
- Number of CPU's: *2*
- CPU speed: *2.80GHz*
- RAM: *16Gb*Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2617[WP] The support of sets is partial2023-02-06T11:02:59ZYani ZIANI[WP] The support of sets is partial<!--
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
Running Frama-C with WP on the following code after uncommenting any of the designated lines. The main idea here was to try and represent a basic C linked list structure as an ACSL tset to easy reasoning and benefit from already existing ACSL clauses.
```C
#include <stdio.h>
typedef struct NODE_TEST {
int handle;
struct NODE_TEST * next;
} NODE_TEST;
/**
* Reachability in linked lists as defined in the ACSL language implementation
* on the Frama-C website
*/
/*@ inductive reachable_node_t{L}(NODE_TEST *root, NODE_TEST *to) {
case empty{L}:
\forall NODE_TEST *l; reachable_node_t{L}(l,l) ;
case non_empty{L}: \forall NODE_TEST *l1,*l2;
\valid(l1)
&& reachable_node_t{L}(l1->next,l2)
==> reachable_node_t{L}(l1,l2) ;
@}
*/
/**
* Logic function used to tranlate a C linked list of NODE_TEST into an ASCL
* tset of its nodes (or at least an attempt at making one). The aim here
* would be to store each pointer to each node of a given linked list in a
* ACSL structure in order to facilitate the proofs of properties such as
* memory separation (by applying the \separated clause to the whole tset),
* loop invariants (using, for instance, the existing \in clause for tsets),
* and others.
*/
/*@ axiomatic NodeTestTSet {
logic set<NODE_TEST *> node_to_tset{L}(NODE_TEST *node)
reads { nod->next | struct NODE_TEST* nod ;
reachable_node_t{L}(nod, \null) && nod \in node_to_tset(node) };
axiom node_empty_tset{L}:
\forall NODE_TEST *node;
node == \null
==> node_to_tset{L}(node) == \empty;
axiom node_not_empty_tset{L}:
\forall NODE_TEST *node;
\let tail = node_to_tset{L}(node->next);
( \valid(node) && reachable_node_t{L}(node->next, \null) )
==> node_to_tset{L}(node) == \union({node}, tail);
}
*/
/**
* Axiomatic definition of the length of a well typed linked list
*/
/*@ axiomatic NodeTestListLgth {
logic integer node_lgth{L}(NODE_TEST *node)
reads { nod->next | struct NODE_TEST* nod; nod \in node_to_tset(node) } ;
axiom node_empty_lgth{L}:
\forall NODE_TEST *node;
node == \null ==> node_lgth{L}(node) == 0;
axiom node_t_not_empty_lgth{L}:
\forall NODE_TEST * node;
(node != \null
&& reachable_node_t{L}(node, \null) )
==> node_lgth{L}(node) == node_lgth{L}(node->next) + 1;
}
*/
/**
* Predicates to easy readability
*/
/*@ predicate is_handle_in_list_tset{L}(NODE_TEST *root, int out_handle) =
\exists NODE_TEST *node;
node \in node_to_tset(root) && node->handle == out_handle;
*/
/*@ predicate is_handle_in_list_reach{L}(NODE_TEST *root, int out_handle) =
\exists NODE_TEST *node;
reachable_node_t(root, node) && node->handle == out_handle;
*/
/*****************************************************************/
/*@
requires linked_list != \null && reachable_node_t(linked_list,\null);
requires 0 < node_lgth(linked_list) <= 10000;
behavior handle_in_list:
// assumes is_handle_in_list_tset(linked_list, out_handle); //causes a why3 error when uncommented
assumes is_handle_in_list_reach(linked_list, out_handle);
ensures \result == 616;
behavior handle_not_in_list:
// assumes !(is_handle_in_list_tset(linked_list, out_handle)); //causes a why3 error when uncommented
assumes !(is_handle_in_list_reach(linked_list, out_handle));
ensures \result == 1610;
disjoint behaviors;
complete behaviors;
*/
int getNode(NODE_TEST * linked_list, int out_handle) {
NODE_TEST *temp_node;
/*@ ghost int n = 0;*/
/*@
loop invariant 0 <= n <= node_lgth(linked_list);
loop invariant temp_node \in node_to_tset(linked_list); //causes a why3 error when uncommented
loop invariant reachable_node_t(linked_list, temp_node);
loop invariant reachable_node_t(temp_node, \null);
loop assigns n, temp_node;
loop variant node_lgth(linked_list) + 1 - n;
*/
for (temp_node = linked_list; temp_node != NULL;
temp_node = temp_node->next) {
if (temp_node->handle == out_handle)
return 616;
/*@ghost n++;*/
}
return 1610;
}
```
<!--
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
Proofs of properties ending either successfully or with a timeout.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
Most proofs end up failing with a why3 error ``[Why3 Error] Library file not found: vset``, even those pertaining to properties that would be proven without the "problematic" lines.
### Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: 22.0 (Titanium), 23.0 (Vanadium), 23.1 (Vanadium), *24.0 (Chromium)* and *25.0-beta (Manganese)* (as reported by `frama-c -version`)
- Plug-in used: WP (using Qed and Alt-Ergo)
- OS name: *Ubuntu*
- OS version: *20.04.4 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.
-->
In the case of Frama-C 24, I also did try using both versions 2.3.2 and 2.4.1 of Alt-Ergo, Frama-C 25 was tested using Alt-Ergo 2.4.1, and every other versions of Frama-C used v2.3.2.
FYI @nkosmatovAllan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2609WP - unsoundness with union2024-03-14T22:21:49ZGeoff HuletteWP - unsoundness with union```
/* bug.c */
#include <assert.h>
typedef union {
int a[2];
struct {
int a0, a1;
} s;
} T;
/*@
requires \valid(t);
requires t->a[0] == 0;
requires t->s.a0 == 0;
assigns *t;
ensures t->a[0] == 1;
ensures t->s.a0 == 0;
*/
voi...```
/* bug.c */
#include <assert.h>
typedef union {
int a[2];
struct {
int a0, a1;
} s;
} T;
/*@
requires \valid(t);
requires t->a[0] == 0;
requires t->s.a0 == 0;
assigns *t;
ensures t->a[0] == 1;
ensures t->s.a0 == 0;
*/
void foo(T *t) { t->a[0] = 1; }
/*@
assigns \nothing;
*/
int main() {
T t;
t.a[0] = 0;
t.s.a0 = 0;
foo(&t);
//@ assert t.s.a0 == 0;
assert(t.s.a0 == 0);
return 0;
}
```
In a shell:
```
$ frama-c --version
24.0 (Chromium)
$ frama-c -wp -wp-rte bug.c
[kernel] Parsing bug.c (with preprocessing)
[rte] annotating function foo
[rte] annotating function main
[wp] 18 goals scheduled
[wp] Proved goals: 18 / 18
Qed: 17 (0.74ms-2ms-3ms)
Alt-Ergo 2.3.3: 1 (20ms) (63)
$ clang bug.c
$ ./a.out
a.out: bug.c:29: int main(): Assertion `t.s.a0 == 0' failed.
Aborted (core dumped)
```Allan BlanchardAllan Blanchardhttps://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/2600[WP] Assertion failed in Instance tactic called from a custom strategy2022-05-09T13:44:19ZLélio Brun[WP] Assertion failed in Instance tactic called from a custom strategy### Steps to reproduce the issue
I tried to narrow down the example, but it's hard to determine where is the problem exactly.
I have an example file [foo_lemma.c](/uploads/a25d0ec0213d97096ccd3fd237b822f5/foo_lemma.c) and a custom strat...### Steps to reproduce the issue
I tried to narrow down the example, but it's hard to determine where is the problem exactly.
I have an example file [foo_lemma.c](/uploads/a25d0ec0213d97096ccd3fd237b822f5/foo_lemma.c) and a custom strategy plugin [strategy_foo.ml](/uploads/2ca56a5f301482f8dad081fbaaa2e839/strategy_foo.ml).
Essentially the strategy tries to guide the solvers by finding witnesses in the hypotheses to instantiate existentially quantified predicates in the goal. It follows the iterative nature of the `T` predicates by unfolding them one step at a time until success. As recommended by the WP manual, the custom strategy only uses pre-defined tactics (namely _Definition_ and _Instance_).
Launch `frama-c -wp -load-module strategy_foo.ml -wp-auto Foo:T foo_lemma.c`.
### Expected behaviour
Frama-C should prove the lemma or at least not fail.
### Actual behaviour
Frama-C fails with the following error:
```
[wp] foo_lemma.c:55: Warning:
[Instance] Exception <File "src/plugins/qed/term.ml", line 2516, characters 4-10: Assertion failed>
[kernel] Current source was: foo_lemma.c:55
The full backtrace is:
Raised at ProverSearch.fork in file "src/plugins/wp/ProverSearch.ml", line 57, characters 6-13
Called from ProverSearch.lookup in file "src/plugins/wp/ProverSearch.ml", line 62, characters 10-33
Called from ProverSearch.first in file "src/plugins/wp/ProverSearch.ml", line 84, characters 25-54
Called from ProverScript.Env.search in file "src/plugins/wp/ProverScript.ml", line 192, characters 12-62
Called from ProverScript.autosearch in file "src/plugins/wp/ProverScript.ml", line 299, characters 8-34
Called from Task.Monad.bind.(fun) in file "src/libraries/utils/task.ml", line 92, characters 42-47
Called from Task.Monad.bind.(fun) in file "src/libraries/utils/task.ml", line 92, characters 42-47
Called from Task.Monad.bind.(fun) in file "src/libraries/utils/task.ml", line 92, characters 42-47
Called from Task.Monad.bind.(fun) in file "src/libraries/utils/task.ml", line 92, characters 42-47
Called from Task.Monad.bind.(fun) in file "src/libraries/utils/task.ml", line 92, characters 42-47
Called from Task.Monad.bind.(fun) in file "src/libraries/utils/task.ml", line 92, characters 42-47
Called from Task.Monad.progress in file "src/libraries/utils/task.ml" (inlined), line 98, characters 19-29
Called from Task.progress in file "src/libraries/utils/task.ml", line 363, characters 14-36
Re-raised at Task.progress in file "src/libraries/utils/task.ml", line 369, characters 6-13
Called from Task.server_progress.(fun) in file "src/libraries/utils/task.ml", line 475, characters 14-27
Called from Stdlib__list.find_all.find in file "list.ml", line 242, characters 17-20
Called from Task.server_progress in file "src/libraries/utils/task.ml", line 473, characters 22-273
Called from Task.on_idle.(fun) in file "src/libraries/utils/task.ml", line 344, characters 14-18
Called from Register.do_wp_proofs in file "src/plugins/wp/register.ml", line 656, characters 4-33
Called from Register.cmdline_run in file "src/plugins/wp/register.ml", line 722, characters 8-26
Called from Extlib.try_finally in file "src/libraries/stdlib/extlib.ml", line 280, characters 14-17
Re-raised at Extlib.try_finally in file "src/libraries/stdlib/extlib.ml", line 280, characters 41-48
Called from Extlib.try_finally in file "src/libraries/stdlib/extlib.ml", line 281, characters 2-12
Called from Extlib.try_finally in file "src/libraries/stdlib/extlib.ml", line 281, characters 2-12
Called from Stdlib__queue.iter.iter in file "queue.ml", line 121, characters 6-15
Called from Boot.play_analysis in file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-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 (File "src/plugins/qed/term.ml", line 2516, characters 4-10: 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: WP
- OS name: Ubuntu
- OS version: 20.04.4 LTS
### Additional information
I tried to see if the error would raise in GUI mode by manually activating the custom tactics in the editor instead of using `-wp-auto Foo:T`:
`frama-c-gui -wp -load-module strategy_foo.ml foo_lemma.c`
It turns out that it won't raise an error dialog, but the following stderr message `** (frama-c-gui:426361): CRITICAL **: 17:47:51.667: GSourceFunc: callback raised an exception`, and the GUI remains in a somewhat stuck state.
This could be another issue by itself maybe.
---
I tracked down the error: the assertion fails [here (`qed/term.ml:2516`)](https://git.frama-c.com/pub/frama-c/-/blob/24.0/src/plugins/qed/term.ml#L2516), from the call [here (`wp/TacInstance.ml:163`)](https://git.frama-c.com/pub/frama-c/-/blob/24.0/src/plugins/wp/TacInstance.ml#L163).
It seems that for some reason (maybe related to the way I wrote my tactic?), the variable `x` chosen to _unbind_ `phi` actually is not fresh (enough).
On a local version of Frama-C I tried to replace the [code at line 157](https://git.frama-c.com/pub/frama-c/-/blob/24.0/src/plugins/wp/TacInstance.ml#L157) with the following:
```ocaml
let pool = F.pool ~copy:env.feedback#pool () in
List.iter (F.add_var pool) (F.e_vars (F.QED.lc_repr phi));
let x = F.fresh pool tau in
```
Basically I'm force-ensuring that the subsequent assertion will not fail, and this seems to solve the problem, as far as I can tell.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2597[WP] Out of memory crash2022-04-20T07:18:53ZLélio Brun[WP] Out of memory crash### Steps to reproduce the issue
Here is a (not necessarily) minimal example (see [excludes.c](/uploads/af45da85624b741546d0e395a330d1e5/excludes.c)):
```c
void excludes8(_Bool x1, _Bool x2, _Bool x3, _Bool x4,
_Bool x...### Steps to reproduce the issue
Here is a (not necessarily) minimal example (see [excludes.c](/uploads/af45da85624b741546d0e395a330d1e5/excludes.c)):
```c
void excludes8(_Bool x1, _Bool x2, _Bool x3, _Bool x4,
_Bool x5, _Bool x6, _Bool x7, _Bool x8,
_Bool *excludes)
{
*excludes =
(!x1 && !x2 && !x3 && !x4 && !x5 && !x6 && !x7 && !x8) ||
( x1 && !x2 && !x3 && !x4 && !x5 && !x6 && !x7 && !x8) ||
(!x1 && x2 && !x3 && !x4 && !x5 && !x6 && !x7 && !x8) ||
(!x1 && !x2 && x3 && !x4 && !x5 && !x6 && !x7 && !x8) ||
(!x1 && !x2 && !x3 && x4 && !x5 && !x6 && !x7 && !x8) ||
(!x1 && !x2 && !x3 && !x4 && x5 && !x6 && !x7 && !x8) ||
(!x1 && !x2 && !x3 && !x4 && !x5 && x6 && !x7 && !x8) ||
(!x1 && !x2 && !x3 && !x4 && !x5 && !x6 && x7 && !x8) ||
(!x1 && !x2 && !x3 && !x4 && !x5 && !x6 && !x7 && x8);
//@ assert *excludes == 1;
return;
}
```
Launch Frama-C / WP: `frama-c -wp excludes.c`
### Expected behaviour
The (silly) assertion should be tried by the solvers.
### Actual behaviour
Out of memory crash (on a 16G laptop):
```
[kernel] Parsing FIREFLY_1.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
'frama-c -wp FIREFLY_1.c' terminated by signal SIGKILL
```
### Contextual information
- Frama-C installation mode: opam
- Frama-C version: 24.0 (Chromium)
- Plug-in used: WP
- OS name: Ubuntu
- OS version: 20.04.4 LTS
- Memory: 15605 MiB
### Additional information (optional)
I tried to profile the execution by using [Memtrace](https://github.com/janestreet/memtrace) on a local installation of Frama-C. It seems that WP is filling huge identifiers tables ([Intmap](https://git.frama-c.com/pub/frama-c/-/blob/24.0/src/plugins/qed/intmap.ml#L273), [Idxmap](https://git.frama-c.com/pub/frama-c/-/blob/24.0/src/plugins/qed/idxmap.ml#L72)) when executing code from [Conditions](https://git.frama-c.com/pub/frama-c/-/blob/24.0/src/plugins/wp/Conditions.ml) module.
Here is the corresponding trace, that can be viewed using [Memtrace_viewer](https://github.com/janestreet/memtrace_viewer): [trace.ctf](/uploads/42173f2b5017d16f12a46cf943dc09e7/trace.ctf)Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2596[WP] Type mismatch with Real model2022-03-15T12:28:29ZLélio Brun[WP] Type mismatch with Real model### Steps to reproduce the issue
Here is a minimal example (see [foo.c](/uploads/a0892900e8240b95c1623e300679efa2/foo.c)):
```c
//@ predicate Foo(double y) = y == 0.0;
void foo(double x) {
//@ assert Foo((double) (0.0 + 0.0 * x));
...### Steps to reproduce the issue
Here is a minimal example (see [foo.c](/uploads/a0892900e8240b95c1623e300679efa2/foo.c)):
```c
//@ predicate Foo(double y) = y == 0.0;
void foo(double x) {
//@ assert Foo((double) (0.0 + 0.0 * x));
}
```
Launch Frama-C / WP with Real model: `frama-c -wp -wp-model real foo.c`
### Expected behaviour
No error (as for `frama-c -wp foo.c`):
```
[kernel] Parsing foo.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Cache] found:1
[wp] Proved goals: 1 / 1
Qed: 0
Alt-Ergo 2.4.1: 1 (56ms) (400) (cached: 1)
[wp:pedantic-assigns] foo.c:3: Warning:
No 'assigns' specification for function 'foo'.
Callers assumptions might be imprecise.
```
### Actual behaviour
Type mismatch error:
```
[kernel] Parsing foo.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Alt-Ergo 2.4.1] Goal typed_real_foo_assert : Failed
[Why3 Error] Type mismatch between real and int
[wp] [Cache] not used
[wp] Proved goals: 0 / 1
Alt-Ergo 2.4.1: 0 (failed: 1)
[wp:pedantic-assigns] foo.c:3: Warning:
No 'assigns' specification for function 'foo'.
Callers assumptions might be imprecise.
```
Indeed, we can see with `frama-c-gui` in Script mode that the expression is simplified to `0`, as we are given the following proof context:
```
Goal Assertion:
Prove: P_Foo(0).
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 24.0 (Chromium)
- Plug-in used: WP
- OS name: Ubuntu
- OS version: 20.04.4 LTS
### Additional information
Removing the addition works:
```c
//@ predicate Foo(double y) = y == 0.0;
void foo(double x) {
//@ assert Foo((double) (0.0 * x));
}
```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/2582Frama-C WP crashes with Invalid_argument("Invalid lock on mutex") when trying...2022-09-26T13:52:22ZGuerricChupinFrama-C WP crashes with Invalid_argument("Invalid lock on mutex") when trying to use CoqI'm currently working on a file with WP and RTE where, sometimes, frama-c will crash when using the option `-wp-prover why3:coq -wp-interactive fix`. Note that CVC4, AltErgo and Z3 are also used but disabling them doesn't have an effect....I'm currently working on a file with WP and RTE where, sometimes, frama-c will crash when using the option `-wp-prover why3:coq -wp-interactive fix`. Note that CVC4, AltErgo and Z3 are also used but disabling them doesn't have an effect. The crash happens right after an editor (Emacs with ProofGeneral in my case, but it also happens with CoqIDE) is opened: the editor closes nearly immediately and Frama-C produces the stacktrace below. Modifying the file slightly (e.g. by adding an extra assertion somewhere) will sometime stop Frama-C from crashing, however I can't seem to find a pattern. I'm currently running C-Reduce on my file to extract a MWE, I will post it in the comments as soon as it terminates (if it produces something useful). See below for information on my setup.
I'm wondering if anyone as an idea as to what causes this behaviour and if it can be fixed easily?
```
[kernel] Current source was: FRAMAC_SHARE/libc/stdlib.h:626
The full backtrace is:
Raised at Extlib.try_finally in file "src/libraries/stdlib/extlib.ml", line 268, characters 41-48
Called from Extlib.try_finally in file "src/libraries/stdlib/extlib.ml", line 269, characters 2-12
Called from Extlib.try_finally in file "src/libraries/stdlib/extlib.ml", line 269, characters 2-12
Called from Stdlib__queue.iter.iter in file "queue.ml", line 121, characters 6-15
Called from Boot.play_analysis in file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-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 (Invalid_argument("Invalid lock on mutex")).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 23.1 (Vanadium).
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 informations
- Frama-C installation method: opam
- Frama-C version: 23.1
- Plug-in used: WP + RTE
- OS Name: Fedora
- OS Version: 34
- Coq Version: 8.13.2
- Why3 Version: 1.4.0Allan BlanchardAllan Blanchardhttps://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/2569Known WP limitations on statement contract2022-09-28T11:42:56ZAllan BlanchardKnown WP limitations on statement contractSince [Frama-C 23.0](https://git.frama-c.com/pub/frama-c/-/releases/23.0), statement contract are not supported anymore. Related issues are closed (as duplicates) and listed here.
- pub/frama-c#625
- pub/frama-c#1912
- pub/frama-c#511Since [Frama-C 23.0](https://git.frama-c.com/pub/frama-c/-/releases/23.0), statement contract are not supported anymore. Related issues are closed (as duplicates) and listed here.
- pub/frama-c#625
- pub/frama-c#1912
- pub/frama-c#511Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2568Known WP limitations on the reads clause2021-08-05T09:28:31ZAllan BlanchardKnown WP limitations on the reads clauseThis issue lists known WP issues with the reads clause. Related issues are closed (as duplicates) and listed here.
- [ ] Generate `reads` footprint
- pub/frama-c#1146
- pub/frama-c#410
- [ ] Better handle missing `reads`
- p...This issue lists known WP issues with the reads clause. Related issues are closed (as duplicates) and listed here.
- [ ] Generate `reads` footprint
- pub/frama-c#1146
- pub/frama-c#410
- [ ] Better handle missing `reads`
- pub/frama-c#2172Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2567Known WP limitations on `assigns` handling2022-09-22T08:58:28ZAllan BlanchardKnown WP limitations on `assigns` handlingThis issue lists known WP issues with the handling of `assigns` annotation. Related issues are closed (as duplicates) and listed here.
- [ ] WP assigns verification is stronger than what ACSL specifies
- mitigation: see option `-wp-...This issue lists known WP issues with the handling of `assigns` annotation. Related issues are closed (as duplicates) and listed here.
- [ ] WP assigns verification is stronger than what ACSL specifies
- mitigation: see option `-wp-unfold-assigns`
- pub/frama-c#1018
- pub/frama-c#1002
- pub/frama-c#2584
- [ ] WP does not use per behavior assigns
- pub/frama-c#2104
- pub/frama-c#3
- pub/frama-c#1019
- pub/frama-c#2629
Suggestions:
- pub/frama-c#337Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2560[Plug-in wp] 96-bits floats2021-10-06T07:52:08Zarun-babu[Plug-in wp] 96-bits floatsFeature request, as I get:
```
[kernel] Parsing file.c (with preprocessing)
[kernel] Plug-in wp aborted: unimplemented feature.
You may send a feature request at https://git.frama-c.com/pub/frama-c/issues with:
'[Plug-in wp] 96-bits...Feature request, as I get:
```
[kernel] Parsing file.c (with preprocessing)
[kernel] Plug-in wp aborted: unimplemented feature.
You may send a feature request at https://git.frama-c.com/pub/frama-c/issues with:
'[Plug-in wp] 96-bits floats'.
```
I am not sure what this means though!https://git.frama-c.com/pub/frama-c/-/issues/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/54An option to return error code if there are any problems with the analysis, s...2021-03-29T11:49:28ZvarosiAn option to return error code if there are any problems with the analysis, so that frama-c is easier to be used in CI/CD workflowsFeature Request
- [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*...Feature Request
- [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: Docker: framac/frama-c:22.0
- Frama-C version: 22.0
- Plug-in used: WP and EVA
- OS name: macOS
- OS version: 11.1
# Steps to reproduce the issue
I put frama-c in a BitBucket CI pipeline. With calling directly frama-c executable. CI pipelines fail when error code returned from executables is different than 0. That way it stops you from pushing erroneous code.
# Expected behaviour
It would be great if there is an option so that frama-c executable return non-zero error code if in EVA found any error in my code, or in WP not all conditions are met.
# Actual behaviour
frama-c return 0 even if EVA show errors from the analysed code. It returns 0 if WP have found non correct behaviour also.https://git.frama-c.com/pub/frama-c/-/issues/47Why3 configuration for Frama-C2021-03-31T10:31:21ZAllan BlanchardWhy3 configuration for Frama-C#### Why3 configuration
We should clarify how we should produce the Why3 configuration file in the case of Frama-C. For opam installation we have added a message at the end of the installation but it is easy to ignore (or miss) this mes...#### Why3 configuration
We should clarify how we should produce the Why3 configuration file in the case of Frama-C. For opam installation we have added a message at the end of the installation but it is easy to ignore (or miss) this message. Furthermore, it is not applicable for Linux distribution packages.
One possibility for us could be to generate a Why3 configuration for Frama-C, that would always be used (unless some environment variable or option is set for example).
#### How to get a prover?
Currently, we use:
- `Why3.Whyconf.parse_filter_prover`
- `Why3.Whyconf.filter_one_prover`
However we currently can call them 3 times *for each* prover. One of them is due to the fact that we can have a composed name like "shortname,version,other_info", but for the two others we have a first call with the received name and the second for this same name but in lower case, and both are necessary (see: https://git.frama-c.com/pub/frama-c/-/issues/41#note_99186).
This shoul be simpler on both Frama-C and Why3 sides.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.