frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2024-02-14T11:19:42Zhttps://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/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/2649[WP] no trivial separation of the allocation status of heap and local variabl...2023-02-15T07:38:06ZYani ZIANI[WP] no trivial separation of the allocation status of heap and local variables whose address are taken<!--
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
I'm currently working on specifying and proving functions focused on linked list structures using previous works based on ACSL logic lists (cf this [paper](https://nikolai-kosmatov.eu/publications/blanchard_kl_sac_2019.pdf)), and I've encountered some issues proving relatively simple assertions when certain types of memory separation between pointers are involved.
### 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.
-->
Running Frama-C with WP on the minimal code inlined below, or running ``frama-c-gui linked_ll_dptr_proof.c -wp -wp-rte -wp-prover altergo,cvc4,cvc4-ce -wp-smoke-tests -wp-fct="dummyCaller, dummyCaller_bis" &`` using the attachments.
I've also taken the liberty of attaching an extended version of the code below in ``linked_ll_dptr_proof.c`` including all the logic definitions (modulo name changes) used in the "Logic against Ghosts" paper, as well as the corresponding lemmas in ``lemmas_list.h``, but I'm not really sure of their relevance, as the issue also occurs on variants of the original logic definitions of the paper that are not used by said lemmas.
```C
#include <stdlib.h>
typedef struct LIST {
int handle;
struct LIST * next;
} LIST;
/**** Logic definitions from the "Logic against Ghosts" paper (modulo renaming for node_to_ll) ****/
/*@
predicate ptr_separated_from_range{L}
(LIST* e, \list<LIST*> ll, integer beg, integer end) =
\forall integer n ; 0 <= beg <= n < end <= \length(ll) ==> \separated(\nth(ll, n), e);
predicate dptr_separated_from_range{L}
(LIST** e, \list<LIST*> ll, integer beg, integer end) =
\forall integer n ; 0 <= beg <= n < end <= \length(ll) ==> \separated(\nth(ll, n), e);
predicate ptr_separated_from_list{L}(LIST* e, \list<LIST*> ll) =
ptr_separated_from_range(e, ll, 0, \length(ll));
predicate dptr_separated_from_list{L}(LIST** e, \list<LIST*> ll) =
dptr_separated_from_range(e, ll, 0, \length(ll));
*/
/*@
predicate in_list{L}(LIST* e, \list<LIST*> ll) =
\exists integer n ; 0 <= n < \length(ll) && \nth(ll, n) == e ;
*/
/*@
inductive linked_ll{L}(LIST *bl, LIST *el, \list<LIST*> ll) {
case linked_ll_nil{L}:
\forall LIST *el ; linked_ll{L}(el, el, \Nil);
case linked_ll_cons{L}:
\forall LIST *bl, *el, \list<LIST*> tail ;
\separated(bl, el) ==> \valid(bl) ==>
linked_ll{L}(bl->next, el, tail) ==>
ptr_separated_from_list(bl, tail) ==>
linked_ll{L}(bl, el, \Cons(bl, tail)) ;
}
*/
/*@
axiomatic Node_To_ll {
logic \list<LIST*> node_to_ll{L}(LIST* beg_node, LIST* end_node)
reads { node->next | LIST* node ; \valid(node) && in_list(node, node_to_ll(beg_node, end_node)) } ;
axiom to_ll_nil{L}:
\forall LIST *node ; node_to_ll{L}(node, node) == \Nil ;
axiom to_ll_cons{L}:
\forall LIST *beg_node, *end_node ;
\separated(beg_node, end_node) ==>
\valid{L}(beg_node) ==>
ptr_separated_from_list{L}(beg_node, node_to_ll{L}(beg_node->next, end_node)) ==>
node_to_ll{L}(beg_node, end_node) == (\Cons(beg_node, node_to_ll{L}(beg_node->next, end_node))) ;
}
*/
/*******************************************************************/
/*@
requires node_separation_to_list : dptr_separated_from_list(out_node, node_to_ll(rsrc_list, NULL)); //if uncommented, linked_assert cannot be proved
assigns \nothing;
ensures \result == 616;
*/
int dummyCallee(LIST * rsrc_list, LIST ** out_node);
/*@
requires linked_ll(rsrc_list, NULL, node_to_ll(rsrc_list, NULL));
assigns \nothing;
ensures \result == 616;
*/
int dummyCaller(LIST * rsrc_list, LIST ** out_node)
{
/*@ assert linked_assert : linked_ll(rsrc_list, NULL, node_to_ll(rsrc_list, NULL));*/ // should be proved from the precondition
int r;
LIST *test_node;
r = dummyCallee(rsrc_list, &test_node);
return r;
}
```
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
The ``linked_assert`` assertion in dummyCaller (or dummyCaller_bis in the attached files) should be always proved, even when the ``node_separation_to_list`` (and/or ``int_separation_to_list`` in attachments) preconditions are uncommented.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
None of the linked_assert assertions are proved.
The situation depicted by ``dummyCaller`` and ``dummyCallee``, using ``node_separation_to_list`` as a precondition, is the closest to the code I'm currently working on.
In the code in attachments, I also tried using ``node_separation_to_nil`` as precondition to test whether the issue also occured using a ``\Nil`` logic list, and the ``dummyCaller_bis`` and ``dummyCallee_bis`` functions to test if eliminating lemmas, or changing the datatype used for separation in ``dummyCallees``, had any influence on the issue, but they don't seem to.
```
```
### Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: 26.0 (Iron) (As well as version 25.0)
- Plug-in used: WP and RTE
- OS name: Ubuntu
- OS version: 20.04.4 LTS
### Additional information (optional)
- Alt-Ergo version : 2.4.2
- CVC4 version : 1.7
<!--
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.
-->
FYI @nkosmatov @floulergue
Edit: I completely forgot to add those attachments earlier :
[linked_ll_dptr_proof.c](/uploads/dd969cc3ce822db1c89e21fa939d0d48/linked_ll_dptr_proof.c)
[lemmas_list.h](/uploads/a9620641f45aa49d32cf7234f2d4ccfd/lemmas_list.h)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/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/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/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/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 Blanchard