frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2020-10-02T11:00:15Zhttps://git.frama-c.com/pub/frama-c/-/issues/30Wanted features related to Why3-Coq2020-10-02T11:00:15ZAllan BlanchardWanted features related to Why3-CoqThis is a follow up on frama-c/frama-c#956 and discussion we had with Jens on the ACSL by Example GitLab about Coq via Why3 in Frama-C.
At least two features could be added to make it easier to use (in particular for ACSL by Example):
...This is a follow up on frama-c/frama-c#956 and discussion we had with Jens on the ACSL by Example GitLab about Coq via Why3 in Frama-C.
At least two features could be added to make it easier to use (in particular for ACSL by Example):
1. drivers that are only applied to Coq (or any prover), an that can be verified,
2. user defined (restricted) context for the proof of lemmas in Coq.
### Drivers
This shall be the job of the driver. We probably need to a way to refine the why3 context *per prover*. Then, it is easy to enrich the Task generated by `ProverWhy3`, which is already « prepared » in a specific way for each prover.
Currently, the supported import directives for WP drivers are:
```
why3.file="mydir/foo.why"
why3.file="mydir/foo.why:Bar"
why3.file="mydir/foo.why:Bar:T"
why3.import="foo.Bar"
why3.import="foo.Bar:T"
```
@lcorrenson suggests to reformulate all of them into something fully understandable from why3 users:
```
[for "myProver",...] loadpath "path/to/dir";
[for "myProver",...] import foo.Bar [as T];
```
This is indeed more flexible than using our custom `meta` directives.
### Restricted context
If we have two files like:
```c
lemma Foo: // ...
lemma To_Prove: // uses Foo
```
```c
lemma Bar: // ...
lemma Foo: // ...
lemma To_Prove: // uses Foo
```
The two files generate different proof contexts for lemmas, because even if `To_Prove` only needs `Foo`, WP collects all lemmas that appear before `To_Prove`. This is why I suggest to provide the user with a way to specify precisely the proof context so that it can remain the same from a file to another.
I think we could create an ACSL extension like:
```c
/*@
lemma Foo: ...
lemma Bar: ...
lemma Proved_with_Coq: ...
lemma_dependencies Proved_with_Coq: Foo ;
*/
```
So that the user can restrict the proof context of the lemma can be as simple and predictable as possible. Note that we should check that it compatible with the `RefUsage` analysis.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/370problem with Qed's simplification power2021-02-22T13:00:23ZJochen Burghardtproblem with Qed's simplification powerID0002278:
**This issue was created automatically from Mantis Issue 2278. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002278:
**This issue was created automatically from Mantis Issue 2278. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002278 | Frama-C | Plug-in > wp | public | 2017-02-06 | 2017-02-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Silicon-20161101 | **OS** | Ubuntu 16.04.1 LTS | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-out wp-out shift.c" on the attached file and inspecting the file "wp-out/typed/foo_post_Alt-Ergo.mlw" shows that lemma "ShiftAssociative" is simplified to "true" (see line 360) by Qed. (The postcondition of foo doesn't matter here, except that it is intentionally unprovable in order to demonstrate the lemma's simplification.)
This situation doesn't change even when all options to disable Qed functionality (i.e. "-wp-no-bits -wp-no-clean -wp-no-core -wp-no-filter -wp-no-init-summarize-array -wp-no-let -wp-no-pruning -wp-no-simpl -wp-no-simplify-forall -wp-no-simplify-is-cint -wp-no-simplify-type") are given. (In contrast, in the somewhat related issue #1751, providing option "-wp-no-bits" is sufficient to circumvent the problem.)
While Qed's simplification capabilities are appreciated in general, the disappearance of the lemma can be a problem:
* In many Coq proofs related to C address computation, a similar lemma has to be stated and proven again and again. There seems to be no easy way to make Coq see what is considered trivial by Qed.
* Considering the discussion at https://github.com/OCamlPro/alt-ergo/issues/19, if I understood the Alt-Ergo people right, Alt-Ergo isn't complete on linear arithmetic with arrays (except for quantifier-free formulas). Therefore it sometimes needs trivial lemmas. In the particular example, to make Alt-Ergo prove the goal "reverse", a kind of associtivity property (axiom "arith") is needed that Qed would simplify also to "true", and even Alt-Ergo would.
Generally speaking, Qed should be (configurable such that it is) no stronger than any of the external provers, such as Coq and Alt-Ergo. This would enable the user to provide appropriate prover hints that are not simplified away by Qed. Maybe a command line option to completely switch off Qed is sufficient. As an alternative, a command-line switch could reduce the capabilities of Qed when applied to lemmas, assuming that the user is responsible to give them in an optimal form.
## Attachments
- [shift.c](/uploads/572d124b06bee30721a80150255027ac/shift.c)
- [foo_post_Alt-Ergo.mlw](/uploads/746bbaa9bc36a947691d7be190773542/foo_post_Alt-Ergo.mlw)Loïc CorrensonLoïc Corrensonhttps://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/1023WP crash when type casting in lemma2021-04-15T15:42:55Zmantis-gitlab-migrationWP crash when type casting in lemmaID0001804:
**This issue was created automatically from Mantis Issue 1804. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001804:
**This issue was created automatically from Mantis Issue 1804. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001804 | Frama-C | Plug-in > wp | public | 2014-06-06 | 2014-06-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Ian | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | Ubuntu | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
When using Typed+cast, a cast in a lemma can cause wp to crash.
In the below example, removing the lemma will cause the assert to validate.
### Steps To Reproduce :
Create file ptr_cast.c :
/*@
lemma valid_pointers:
\forall int **ptr; sizeof(int *) >= sizeof(int) ==> \valid(ptr) ==> \valid((int *) ptr);
*/
void f(int **ptr){
//@ assert sizeof(int *) >= sizeof(int) ==> \valid(ptr) ==> \valid((int *) ptr);
}
Run :
frama-c -cpp-command 'gcc -C -E' -pp-annot -wp -wp-model Typed+cast ptr_cast.c
Receive output :
[kernel] preprocessing with "gcc -C -E -dD ptr_cast.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
ptr_cast.c:4:[wp] warning: Cast with incompatible pointers types (source: int**) (target: sint32*)
[wp] failure: Context 'Warning' non-initialized.
[kernel] Current source was: ptr_cast.c:7
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "src/wp/Warning.ml", line 117, characters 10-31
Called from file "src/wp/MemTyped.ml", line 799, characters 3-111
Called from file "src/wp/MemVar.ml", line 374, characters 23-51
Called from file "src/wp/Cvalues.ml", line 433, characters 30-42
Called from file "src/wp/LogicSemantics.ml", line 768, characters 12-27
Called from file "src/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/wp/Context.ml", line 34, characters 41-46
Called from file "src/wp/LogicCompiler.ml", line 358, characters 20-35
Called from file "src/wp/LogicSemantics.ml", line 779, characters 12-37
Called from file "src/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/wp/Context.ml", line 34, characters 41-46
Called from file "src/wp/LogicCompiler.ml", line 357, characters 28-51
Called from file "src/wp/LogicSemantics.ml", line 779, characters 12-37
Called from file "src/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/wp/Context.ml", line 34, characters 41-46
Called from file "src/wp/LogicCompiler.ml", line 357, characters 28-51
Called from file "src/wp/LogicSemantics.ml", line 779, characters 12-37
Called from file "src/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/wp/Context.ml", line 34, characters 41-46
Called from file "src/wp/Lang.ml", line 869, characters 33-38
Re-raised at file "src/wp/Lang.ml", line 870, characters 40-43
Called from file "src/wp/LogicSemantics.ml", line 684, characters 11-54
Called from file "src/wp/LogicSemantics.ml", line 779, characters 12-37
Called from file "src/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/wp/Context.ml", line 34, characters 41-46
Called from file "src/wp/LogicCompiler.ml", line 326, characters 14-25
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/LogicCompiler.ml", line 401, characters 24-83
Called from file "src/wp/LogicCompiler.ml", line 673, characters 6-97
Called from file "src/wp/LogicCompiler.ml", line 690, characters 19-41
Called from file "src/wp/cfgWP.ml", line 1294, characters 31-42
Called from file "map.ml", line 169, characters 20-25
Called from file "src/wp/cfgWP.ml", line 1369, characters 14-54
Called from file "src/wp/Model.ml", line 111, characters 17-20
Re-raised at file "src/wp/Model.ml", line 116, characters 25-28
Called from file "src/wp/Model.ml", line 117, characters 19-36
Called from file "src/wp/register.ml", line 435, characters 17-42
Called from file "src/wp/register.ml", line 574, characters 17-24
Re-raised at file "src/wp/register.ml", line 578, characters 29-31
Called from file "src/wp/register.ml", line 575, characters 17-24
Re-raised at file "src/wp/register.ml", line 579, characters 32-34
Called from file "src/wp/register.ml", line 575, characters 17-24
Re-raised at file "src/wp/register.ml", line 579, characters 32-34
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 37, characters 4-20
Called from file "src/kernel/cmdline.ml", line 735, characters 2-9
Called from file "src/kernel/cmdline.ml", line 214, characters 4-8
Plug-in wp aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelinesAllan 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/2098suggest to provide FILE,LINE references for proof obligations in WP cmd-line ...2021-08-05T13:14:10ZJochen Burghardtsuggest to provide FILE,LINE references for proof obligations in WP cmd-line outputID0001011:
**This issue was created automatically from Mantis Issue 1011. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001011:
**This issue was created automatically from Mantis Issue 1011. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001011 | Frama-C | Plug-in > wp | public | 2011-11-04 | 2011-11-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Currently, the command-line (i.e. non-gui) version of WP gives internally-generated names of proof obligations, like e.g.
[wp] [Simplify] Goal store_axiom_pop_of_push_pre31_push_stack_s1 : Valid
[wp] [Simplify] Goal store_axiom_pop_of_push_pre26_pop_stack_s2 : Timeout
In order to support the user in improving his program to get it verified, it should be made clear where an unproven obligation originated from, by providing file name and line number. Although a lot of information can be found in the directory specified with "-wp-out", the FILE,LINE information cannot.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/907axiom "addr_le_def" given to Alt-Ergo considered too weak2021-08-05T14:15:00ZJochen Burghardtaxiom "addr_le_def" given to Alt-Ergo considered too weakID0002047:
**This issue was created automatically from Mantis Issue 2047. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002047:
**This issue was created automatically from Mantis Issue 2047. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002047 | Frama-Clang | Plug-in > wp | public | 2015-01-12 | 2015-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Jan2015-Neon-20140301+dev-STANC | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The loop invariant "xx5" of the attached program "fill1.c" can't be proven with Alt-Ergo. The goal reads fine, viz.:
goal fill_loop_inv_xx5_preserved:
forall a_3,a_2,a_1,a : addr.
(a_1 <> a_2) ->
addr_le(a_3, a_2) ->
(region(a.base) <= 0) ->
(region(a_3.base) <= 0) ->
addr_le(a_3, shift_sint16(a_2, 1))
However, the axiom "addr_le_def" appears to be too weak, it currently reads:
axiom addr_le_def :
(forall p:addr. forall q:addr [addr_le(p, q)]. (((p).base = (q).base) ->
(addr_le(p, q) -> ((p).offset <= (q).offset))))
While the loop inveriant certainly should be provable, I don't see any way to prove a_3.base=a_2.base with the current version of the file.
Moreover, in order for axioms "addr_le_def" and "addr_le_def1" to be a definition of "addr_le(.,.)" in terms of "=" and "<=" etc., axiom "addr_le_def" should be changed to:
axiom addr_le_def :
(forall p:addr. forall q:addr [addr_le(p, q)].
(addr_le(p, q) -> p.base = q.base and p.offset <= q.offset))
After that change, Alt-Ergo proves the goal without any problems. The attached file "fill_loop_inv_xx5_preserved_Alt-Ergo.mlw" contains the changed version in a comment at line 408.
If my argument is right, the whole axiomatization should be reviewed to remove similar flaws, which give Frama-C a rather poor performance on address arithmetic. (For that reason, I assigned a higher severity.)
### Additional Information :
Originally, I'd submitted this issue to the Alt-Ergo issue tracker, see https://github.com/OCamlPro/alt-ergo/issues/9. I'm indebted to Mohamed Iguernelala for hinting at the weak axiom "addr_le_def", where I had a blind spot.
## Attachments
- [fill1.c](/uploads/e5ff187165a5e10b7858e1f325eea68a/fill1.c)
- [fill_loop_inv_xx5_preserved_Alt-Ergo.mlw](/uploads/6292554fc2953d67792737e6dac31199/fill_loop_inv_xx5_preserved_Alt-Ergo.mlw)
- [fill.c](/uploads/c1dcc11d568e2e09d95aeabf0b9df093/fill.c)
- [fill4.c](/uploads/5ce99f117503a2df12c827af1b439520/fill4.c)
- [fill5.c](/uploads/ece00cbe919a18c0800d32b0adb27fb2/fill5.c)
- [fill4r.c](/uploads/81225ff5f9ecee0d89645919cbe59e44/fill4r.c)
- [find_arr.c](/uploads/fec90cf4fecefaee9a7cea344c14b693/find_arr.c)
- [find_ptr.c](/uploads/8430a7bbd76c8f263bd433d3cfd746d8/find_ptr.c)
- [find_ptr_foo_post_Alt-Ergo_modified.mlw](/uploads/d52e028cdf21562b07c9e340031cef8c/find_ptr_foo_post_Alt-Ergo_modified.mlw)Loïc CorrensonLoïc Corrensonhttps://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/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/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/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/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/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/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/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/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/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/2652Unproven validity of memory access2023-05-16T06:54:01ZYani ZIANIUnproven validity of memory access<!--
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
According to the ACSL language implementation p.67 for Frama-C v26.0 and 26.1 (modulo potential alignment constraints), the ``valid {L}(p) <==> \valid{L}(((char *)p)+(0 .. sizeof(*p)-1))`` equivalence should hold true for any pointer ``p`` (and would be in line with C's behavior when trying to access any pointer as an array of bytes). But I've run into trouble trying to prove it in simple cases, be it using the ``Typed`` memory model, or its extension using ``+cast``.
### 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 char_ptr.c -wp `` and ``frama-c-gui char_ptr.c -wp -wp-model Typed+cast`` using the attachments.
```C
#include <stdio.h>
typedef struct {
int test_buffer[5];
} test_type;
int * test_ptr;
test_type * _test_type_ptr;
int dummy_valid()
{
/*@ check \valid(test_ptr) ==> \valid(((char *) test_ptr) + (0 .. (size_t) sizeof(*test_ptr) -
/*@ check \valid(((char *) test_ptr) + (0 .. (size_t) sizeof(*test_ptr) - 1)) ==> \valid(
/*@ check \valid(_test_type_ptr) ==> \valid(((char *) _test_type_ptr) + (0 .. (size_t) sizeof(*_test_type_ptr) -
/*@ check \valid((char *) _test_type_ptr + (0 .. (size_t) sizeof(*_test_type_ptr) - 1)) ==> \valid(_test_type_ptr);*/
return 0;
}
```
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
All check clauses should be proved when using the ``+cast`` variant of ``Typed``.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
None of the check clauses extending the validity of the original pointer to the validity of the corresponding byte array are proved.
My understanding/guess would be that it may be due to WP's ability to translate the cast to ``char *`` to byte accesses, but I'm really not clear on what's actually happening there.
```
```
### Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: 26.0 (Iron)
- Plug-in used: WP
- OS name: Ubuntu
- OS version: 20.04.4 LTS
### Additional information (optional)
- Alt-Ergo version : 2.4.2
<!--
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
[char_ptr.c](/uploads/8ebaf1fac5f9a9c8de2e0367ef0cd628/char_ptr.c)Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/32Known WP limitation: Dynamic allocation is not supported2023-07-21T13:06:10ZBob RubbensKnown WP limitation: Dynamic allocation is not supportedHello everyone,
A colleague of mine tried to use variables as a length argument for an array:
```c
int const n = 4;
int main() {
int xs[n];
}
```
This yielded the following frama-c output:
```bash
[nix-shell:~]$ frama-c -wp program...Hello everyone,
A colleague of mine tried to use variables as a length argument for an array:
```c
int const n = 4;
int main() {
int xs[n];
}
```
This yielded the following frama-c output:
```bash
[nix-shell:~]$ frama-c -wp program.c
[kernel] Parsing program.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] program.c:4: Warning:
Cast with incompatible pointers types (source: sint32*) (target: sint8*)
[wp] program.c:4: Warning:
Cast with incompatible pointers types (source: sint8*) (target: sint32*)
[wp] 1 goal scheduled
[wp] Proved goals: 1 / 1
Qed: 1
```
Frama-c version (for completeness, I'm using the version from nixpkgs unstable):
```bash
[nix-shell:~]$ frama-c --version
21.1 (Scandium)
```
The warning seems strange, as I use only ints in this program. With my limited knowledge of C, I'd say this program does no such casting. Is this a bug or is this somehow a subtle edge case in C? Or is it benign and can it be ignored?Allan BlanchardAllan Blanchard