frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-05-28T09:30:55Zhttps://git.frama-c.com/pub/frama-c/-/issues/2[wp] non-provable local typing constraints in lemmas2021-05-28T09:30:55ZJens Gerlach[wp] non-provable local typing constraints in lemmas# Steps to reproduce the issue
The attached archive contains the ACSL function `Count` together with several lemma.
Also contained are
- a Makefile
- a coq proof in file `wp0.script.20` for lemma `CountBounds` that works for Frama-C 20...# Steps to reproduce the issue
The attached archive contains the ACSL function `Count` together with several lemma.
Also contained are
- a Makefile
- a coq proof in file `wp0.script.20` for lemma `CountBounds` that works for Frama-C 20
- an attempt of a coq proof in file `wp0.script.21` for lemma `CountBounds` that fails for Frama-C 21
- The files `CountBounds.v.20` and `CountBounds.v.21` contain the coq code as extracted from CoqIde
# Expected behaviour
My problem is that I am unable to adapt the coq proof that worked fro Frama-C 20 to the newer version of Frama-C.
# Actual behaviour
I suspect that this is related to changes in the generated Coq code of the VC of lemma `CountBounds`
This can be best seen when calling `diff CountBounds.v.20 CountBounds.v.21`.
```
$ diff CountBounds.v.20 CountBounds.v.21
39,40c39,40
< (((t.[ (shift_sint32 a x) ]) <> i_2)%Z) -> ((i < i_1)%Z) ->
< ((is_sint32 i_2%Z)) ->
---
> let x_1 := (t.[ (shift_sint32 a x) ])%Z in ((x_1 <> i_2)%Z) ->
> ((i < i_1)%Z) -> ((is_sint32 i_2%Z)) -> ((is_sint32 x_1)) ->
```
# Fix ideas
I think the issue is caused by the condition `((is_sint32 x_1))` for the newly introduced term `x_1 := (t.[ (shift_sint32 a x) ])%Z`. I haven't found a way to satisfy the condition `((is_sint32 x_1))` and I suspect that it is not possible.
If it is possible, then I apologise and ask for a hint.
Regards
Jens Gerlach
[CoqFramac21.tar](/uploads/e95b883ad30f134748c5a7289fa6902d/CoqFramac21.tar)Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/3[wp] shall use per-behaviour assigns at call sites2021-08-05T08:49:16ZNikolai Kosmatov[wp] shall use per-behaviour assigns at call sites# Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *20.0 (Calcium)* (as reported by `frama-c -version`)
- Plug-in used: *WP*
- OS name: *Ubuntu*
- OS version: *19.10*
*Please add specific information deemed...# Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *20.0 (Calcium)* (as reported by `frama-c -version`)
- Plug-in used: *WP*
- OS name: *Ubuntu*
- OS version: *19.10*
*Please add specific information deemed relevant with regard to this issue.*
# Steps to reproduce the issue
frama-c-gui -wp behavior_assigns.c
*Please indicate here steps to follow which reproduce the issue.*
See the attached file for a minimal example. [behavior_assigns.c](/uploads/b4eaee1cce8750d4749d64794e79883c/behavior_assigns.c)
# Expected behaviour
The assigns clause of caller can be proved.
# Actual behaviour
The assigns clause of caller is not proved.
The assigns clauses specific for particular behaviors in a callee cannot be used in the caller
under specific conditions falling into such behavior(s) to prove a more restrictive assigns clause
in the caller, rather than the most general assigns taking into account all behaviors of the callee.
# Fix ideas
Obvious workarounds include additional postconditions, that make the specifications more complex and
make the proof with WP less powerful. Matching the callee's behaviors to prove stronger assigns clauses
in the caller could be helpful.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/16[wp] unsoundness for base-offset2021-02-22T14:00:48ZLoïc Correnson[wp] unsoundness for base-offsetComputation of WP for `\offset()` in MemTyped is actually using a function `base_offset(idx)` that max index of cells in memory to their actual offset in bytes. Example:
```
struct S {
int f; // index 0, offset 0
long g; // in...Computation of WP for `\offset()` in MemTyped is actually using a function `base_offset(idx)` that max index of cells in memory to their actual offset in bytes. Example:
```
struct S {
int f; // index 0, offset 0
long g; // index 1, offset 4
int h; // index 2, offset 12
}; // size,=3, sizeof=16
```
This function is left mostly unspecified, and is required to be monotonic.
This prevent WP from computing exact offsets, but is _not_ a problem, this is just an under-specification.
Moreover, the index-offset correspondance _could_ be formally specified for each known base-address from its type (if it does not changed, as it is assumed in MemTyped).
However, this function is currently the _same_ for all base address, which is certainly incorrect and might cause unsoundness when asking WP for computing `\offset()` within variables of different types.
It **shall** be modelled as `base_offset(base, index)`.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/18WP: Incorrect assigns global/static handling2021-02-22T14:00:16ZAlex CoffinWP: Incorrect assigns global/static handling
View all of the following goals succeed for the following program:
```
#include <assert.h>
unsigned int number = 0;
/*@
assigns number;
ensures \valid(\result);
*/
unsigned int* a_num(void) {
++number;
return &number;
}
void...
View all of the following goals succeed for the following program:
```
#include <assert.h>
unsigned int number = 0;
/*@
assigns number;
ensures \valid(\result);
*/
unsigned int* a_num(void) {
++number;
return &number;
}
void test_a_num(void) {
unsigned int* a = a_num();
unsigned int copy = *a;
assert(copy == *a);
unsigned int* b = a_num();
assert(copy == *a);
}
int main(int argc, char** argv) {
test_a_num();
return 0;
}
```
compiled with `frama-c-gui -wp -wp-rte -wp-smoke-tests test.c`
# Expected behaviour
The second assert function call fails when run, and therefore WP should not be able to prove its preconditions.
# Actual behaviour
It claims that it has proven (incorrectly) that the assert function call will be successful. Of course the `assert` calls may be replaced with `/*@ assert */` statements instead, and it still claims that they pass.
# Fix ideas
Check handling of static/global variables with assigns?Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/55z3 ERROR: unknown parameter 'model_compress'2021-02-22T12:52:03Zrwmjonesz3 ERROR: unknown parameter 'model_compress'ID0002509:
**This issue was created automatically from Mantis Issue 2509. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002509:
**This issue was created automatically from Mantis Issue 2509. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002509 | Frama-C | Plug-in > wp | public | 2020-10-15 | 2020-10-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | rwmjones | **Assigned To** | correnson | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Apparently z3 dropped this parameter and replaced it with "model.compact" without bothering with backward compatibility: https://github.com/Z3Prover/z3/issues/2704#issuecomment-554489258
### Steps To Reproduce :
Use z3 4.8.9, turn on debugging.
<6.827036,call_prover>Call_provers: actual command is:
z3 -smt2 -t:10000 sat.random_seed=42
model_compress=false nlsat.randomize=false
smt.random_seed=42 -st
/tmp/why_b9efc2_zilch-T-wp_goal.smt2
ERROR: unknown parameter 'model_compress'https://git.frama-c.com/pub/frama-c/-/issues/41Z3 and CVC4 working for Frama-C 22 (Titanium) beta after some initial problems2021-04-13T17:49:41ZJens GerlachZ3 and CVC4 working for Frama-C 22 (Titanium) beta after some initial problems**I updated the title after figuring out a solution**
- [x] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [x] the issue has not yet been reported on our [BTS](https://bts.frama-c.com);
- ...**I updated the title after figuring out a solution**
- [x] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [x] the issue has not yet been reported on our [BTS](https://bts.frama-c.com);
- [x] you installed Frama-C as prescribed in the [instructions](INSTALL.md).
# Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *22.0-beta (Titanium)*
- Plug-in used: *WP*
- OS name: *Xubuntu*
- OS version: *Ubuntu 20.04.1 LTS*
*Please add specific information deemed relevant with regard to this issue.*
I am able to use the options `-wp-prover Alt-Ergo -wp-prover native:coq ` with *ACSL by Example*.
However when using either `-wp-prover Z3` or `-wp-prover z3` I receive the following error message.
(Note that `z3` (4.8.6) has been installed and that it has been successfully registered with `why3 config --full-config`)
```
[kernel] Parsing find.c (with preprocessing)
[rte] annotating function find
[wp] User Error: Prover 'z3' not found in why3.conf
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 25 goals scheduled
[wp] Proved goals: 25 / 25
Qed: 16 (2ms-6ms-20ms)
Alt-Ergo 2.3.3: 9 (5ms-12ms) (87)
[wp] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Plug-in wp aborted: invalid user input.
```
Similar with `CVC4` and `cvc4`.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/46Question: Dump why3 file generated by frama-c2023-06-05T07:47:25ZLeo ViezensQuestion: Dump why3 file generated by frama-cHey, <br>
if I proove a file with the wp plugin, the C code gets transpiled into WhyML, is that right? <br>
If so, is it already possible, to dump the generated WhyML into a file? <br>
Thank you for your help.Hey, <br>
if I proove a file with the wp plugin, the C code gets transpiled into WhyML, is that right? <br>
If so, is it already possible, to dump the generated WhyML into a file? <br>
Thank you for your help.https://git.frama-c.com/pub/frama-c/-/issues/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/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/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/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/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/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/2631Naming the anonymous behavior for -wp-bhv2023-06-21T08:58:19ZDavid CokNaming the anonymous behavior for -wp-bhvFeature request (or perhaps just information):
in using WP, the -wp-bhv option works fine for named behaviors. But how does one indicate to check just the anonymous behavior?
If there is no way currently, then please add some syntax tha...Feature request (or perhaps just information):
in using WP, the -wp-bhv option works fine for named behaviors. But how does one indicate to check just the anonymous behavior?
If there is no way currently, then please add some syntax that does not interfere with most shells. For example -wp-bhv ~Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2632-wp-print for only failed goals2023-07-21T13:01:36ZDavid Cok-wp-print for only failed goalsI suggest a variation on -wp-print that only lists the details for failed goals, perhaps -wp-print-failuresI suggest a variation on -wp-print that only lists the details for failed goals, perhaps -wp-print-failuresLoïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2636[WP] Builtin \sign(float64) is not defined2022-12-14T12:36:37ZNiksonber[WP] Builtin \sign(float64) is not defined<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Description
Built-in \\sign is not defined in WP.
`Builtin \sign(float64) not defined`
`[wp] Failure: Logic type 'sign' undefined`
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
### Steps To Reproduce
Run: `frama-c -wp -wp-out . -wp-prover coq -wp-model +float -wp-interactive update just_sign.c`
Where `just_sign.c` is:
```
#include <math.h>
/*@
predicate is_same_sign(double X, double Y) = \sign(X) == \sign(Y);
*/
/*@
ensures (is_same_sign(a_double, \result)) ;
assigns \nothing;
*/
double dummy (double a_double) {
return a_double;
}
```
I got the following output:
```
[wp] Warning: Missing RTE guards
[wp] just_sign.c:4: Warning: Builtin \sign(float64) not defined
[wp] just_sign.c:4: Warning: Builtin \sign(float64) not defined
[wp] 2 goals scheduled
[wp] Failure: Logic type 'sign' undefined
```
### Expected behaviour
Expected a definition for \sign.
<!--
Please explain here what is the expected behaviour.
-->
### Actual behaviour
WP reports:
```
[wp] Failure: Logic type 'sign' undefined
[wp] just_sign.c:4: Warning: Builtin \sign(float64) not defined
```
<!--
Please explain here what is the actual (faulty) behaviour.
-->
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 24.0, 25.0 (Manganese), 26.0+dev (Iron) (I tried Several versions)
- Plug-in used: WP
- OS name: Ubuntu
- OS version: 22.04 LTS
<!--
### Additional information (optional)
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2644[WP] Fails to verify left shift by 2 on range2023-01-24T11:13:25ZCostava[WP] Fails to verify left shift by 2 on range<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
```c
/*@
requires a == 1;
assigns \nothing;
ensures \result == (a << 2);
*/
unsigned int do_one(const unsigned int a) {
return (a << 2);
}
/*@
requires a == 2;
assigns \nothing;
ensures \result == (a << 2);
*/
unsigned int do_two(const unsigned int a) {
return (a << 2);
}
/*@
requires 1 <= a <= 2;
assigns \nothing;
ensures \result == (a << 2);
*/
unsigned int do_some_shift2(const unsigned int a) {
return (a << 2);
}
/*@
requires 1 <= a <= 2;
assigns \nothing;
ensures \result == (a << 1);
*/
unsigned int do_some_shift1(const unsigned int a) {
return (a << 1);
}
```
```sh
$ frama-c -wp -wp-rte fcshift.c
```
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
All goals verified successfully.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
```sh
$ frama-c -wp -wp-rte fcshift.c
[kernel] Parsing fcshift.c (with preprocessing)
[rte:annot] annotating function do_one
[rte:annot] annotating function do_some_shift1
[rte:annot] annotating function do_some_shift2
[rte:annot] annotating function do_two
[wp] 8 goals scheduled
[wp] [Alt-Ergo 2.4.1] Goal typed_do_some_shift2_ensures : Timeout (Qed:2ms) (10s)
[wp] Proved goals: 7 / 8
Qed: 6 (0.33ms-0.64ms-2ms)
Alt-Ergo 2.4.1: 1 (10ms) (92) (interrupted: 1)
```
The ensures goal can be verified when `a` has a single value of either `1` or `2` respectively for the `do_one` and `do_two` functions.
But if `a` is `1` or `2` (for function `do_some_shift2`), then the ensures goal fails to verify.
Oddly, the goal succeeds if the left shift is by `1` instead of `2` (function `do_some_shift1`).
[cppreference.com](https://en.cppreference.com/w/c/language/arithmetic_types) is stating that `unsigned int` should always have at least 16 bits, so it is weird to me that changing the amount of the shift is making a difference.
Doubling the timeout to 20 does not make the goal succeed automatically.
Using `frama-c-gui`, I know that I can apply tactic `Logical Shift` on `lsl(a, 2)` in order to make the goal succeed, but a goal that is this specific and simple failing to verify seems like a bug.
### Contextual information
- Frama-C installation mode: opam
- Frama-C version: 25.0 (Manganese)
- Plug-in used: WP, RTE, Alt-Ergo 2.4.1
- OS name: Manjaro Linux
- OS version: Sikaris 22.0.0
### Additional information (optional)
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->
N/ALoïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2650Stack overflow using WP in Wp__Register.step_finally2023-03-29T20:08:35ZChristophe GarionStack overflow using WP in Wp__Register.step_finallyFrama-C 26.1 and its WP plugin crash with a stack overflow when trying to prove a function:
```
The full backtrace is:
Raised at Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 834, characters 41-48
Called fro...Frama-C 26.1 and its WP plugin crash with a stack overflow when trying to prove a function:
```
The full backtrace is:
Raised at Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 834, characters 41-48
Called from Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 835, characters 2-12
Called from Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 835, characters 2-12
Called from Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 835, characters 2-12
Called from Stdlib__Queue.iter.iter in file "queue.ml", line 121, characters 6-15
Called from Frama_c_boot__Boot.play_analysis in file "src/init/boot/boot.ml", line 36, characters 4-20
Called from Frama_c_kernel__Cmdline.play_in_toplevel_one_shot in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 850, characters 2-9
Called from Frama_c_kernel__Cmdline.play_in_toplevel in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 880, characters 18-64
Called from Frama_c_kernel__Cmdline.catch_toplevel_run in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 233, characters 4-8
Unexpected error (Stack overflow).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 26.1 (Iron).
```
The function to be proved is part of a rather big C file included in the attached archive. Sorry for the complexity (and maybe the bad quality) of the C code, it is in fact produced by a Lustre compiler we are working on. I will try to produce a real MWE...
Running Frama-C and WP on the whole file causes a stack overflow on `List.map` but I reduce the error when proving the `Arrays1_Arrays1_node_step` function. I use the `ref` and the `real` memory model.
When launching Frama-C on the function, no goal is produced (at least there is no printing of it), only Frama-C is running (there is no process involving Alt-Ergo or Z3 for instance). the crash happens after 13 minutes (!) on my computer (a recent laptop with i9 cores).
### Steps to reproduce the issue
* open the attached archive
* issue the following command:
```
frama-c -wp -wp-model ref,real -wp-fct Arrays1_Arrays1_node_step Arrays1.c
```
### Contextual information
- Frama-C installation mode: opam with an OCaml 4.14.0 switch
- Frama-C version: 26.1 (Iron)
- Plug-in used: WP
- OS name: Linux
- OS version: 22.04
Thanks,
Christophe
[arrays_stack_overflow_wo_optimization.tgz](/uploads/e88a0fcabd4de811d59024517c679f5d/arrays_stack_overflow_wo_optimization.tgz)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2657frama-c-gui frozen and why3 not found2023-04-13T14:44:13ZRongframa-c-gui frozen and why3 not found### Problem Description ###
When running `opam install alt-ergo`, my terminal shows:
```
Package alt-ergo is already installed (current version is 2.4.2).
```
However, when running `frama-c-gui -wp -rte -main.c`, the terminal shows:
...### Problem Description ###
When running `opam install alt-ergo`, my terminal shows:
```
Package alt-ergo is already installed (current version is 2.4.2).
```
However, when running `frama-c-gui -wp -rte -main.c`, the terminal shows:
```
(frama-c-gui:4023): GLib-CRITICAL **: 09:36:25.664: Source ID 8 was not found when attempting to remove it.
```
The GUI is opened but frozen. No clicking is responded and the console shows `User Error: Prover 'alt-ergo' not found in why3.conf.`
### Steps to reproduce the issue
frama-c-gui -wp -rte -main.c
### Expected behaviour
open the window of frama-c-gui and run normally
### Actual behaviour
The GUI is opened but frozen. No clicking is responded and the console shows `User Error: Prover 'alt-ergo' not found in why3.conf.`
### Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *frama-c.26.1*
- Plug-in used: *Plug-in used*
- OS name: *Ubuntu*
- OS version: *22.04.2 LTS*
### Additional information (optional)
After running "opam upgrade", the following information appears:
```
Everything as up-to-date as possible (run with --verbose to show unavailable upgrades).
The following packages are not being upgraded because the new versions conflict with other installed packages:
- ocaml-config.3
- ocplib-simplex.0.5
∗ alt-ergo-lib.2.4.2 is installed and requires ocplib-simplex (>= 0.4 & < 0.5)
- why3.1.6.0
∗ frama-c.26.1 is installed and requires why3 (>= 1.5.1 & < 1.6~)
However, you may "opam upgrade" these packages explicitly, which will ask permission to downgrade or uninstall the conflicting packages.
Nothing to do.
# Run eval $(opam env) to update the current shell environment
```https://git.frama-c.com/pub/frama-c/-/issues/2663Parse-print-reparse error with WP strategies2023-07-21T09:11:17ZNikolai KosmatovParse-print-reparse error with WP strategies## Contextual information: currently used versions
- Frama-C installation mode: *Opam*
- Frama-C version 27.0dev (tested commit: 3396bd)
- Alt-Ergo 2.4.3
- OS name: *Ubuntu*
- OS version: *20.04*
## The issue
On the attached file, aft...## Contextual information: currently used versions
- Frama-C installation mode: *Opam*
- Frama-C version 27.0dev (tested commit: 3396bd)
- Alt-Ergo 2.4.3
- OS name: *Ubuntu*
- OS version: *20.04*
## The issue
On the attached file, after parsing and printing the code, running frama-c again to parse the code produces an error (due to missing parentheses around a list of arguments (..)).
[strategy.c](/uploads/d089f42a7b3f32480a9d03227f201f0a/strategy.c)
Commands used:
`frama-c strategy.c -print -no-unicode -ocode pp_strategy.c`
`frama-c pp_strategy.c`Allan BlanchardAllan Blanchard