frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2023-11-27T15:03:11Zhttps://git.frama-c.com/pub/frama-c/-/issues/2680[WP] Using Z3 when predicate with access to struct defined leads to inconsist...2023-11-27T15:03:11ZReMarxist[WP] Using Z3 when predicate with access to struct defined leads to inconsistency### Steps to reproduce the issue
Launch the following example with this command (note big timeout):
```bash
frama-c -wp -rte -wp-prover="z3" -wp-timeout 100 acsl.c
```
Example:
```c
struct S
{
int n;
};
/*@ axiomatic Block {
pr...### Steps to reproduce the issue
Launch the following example with this command (note big timeout):
```bash
frama-c -wp -rte -wp-prover="z3" -wp-timeout 100 acsl.c
```
Example:
```c
struct S
{
int n;
};
/*@ axiomatic Block {
predicate isZero(int left) =
left == 0;
// Unused, but necessary for verification
logic int getN(struct S *s) = s->n;
}*/
/*@ requires \valid(s);
requires isZero(s->n);
assigns \nothing;
ensures \false; // Verified by Z3
*/
void g(struct S *s)
{
}
/*@ assigns \nothing;
ensures \false; // Verified by Z3
*/
void f()
{
struct S s;
s.n = 0;
g(&s);
}
```
As you can see, specifications establish that f() and g() ensure obviously false statement. The problem is in verification of g(), I've defined f() to show that preconditions of g() can be satisfied.
### Expected behaviour
Attempt to prove `\false` in postcondition of `g()` should fail.
### Actual behaviour
Z3 proves `\false` in postcondition of `g()`:
```
[kernel] Parsing tmp/acsl/acsl.c (with preprocessing)
[rte:annot] annotating function f
[rte:annot] annotating function g
[wp] Running WP plugin...
[wp] 9 goals scheduled
[wp] Proved goals: 9 / 9
Qed: 7
Z3 4.12.2: 2
```
### Contextual information
- Frama-C installation mode: opam
- Frama-C version: 27.1 (Cobalt)
- Z3 version 4.12.2 - 64 bit
- Why3 platform version: 1.6.0
- Plug-in used: WP
- OS name: Ubuntu
- OS version: 20.04
### Additional information
The problem may be in Z3 itself, because Alt-Ergo and CVC4 cannot prove these goals. I've also reproduced the problem using docker image from Docker Hub.
I've posted this report as a question on StackOverflow previously (https://stackoverflow.com/questions/77460683/why-wp-with-z3-proves-false-when-access-to-struct-field-is-defined) as I wasn't able to post an issue here.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2666Alias plugin's `Abstract_state` API requires using private `Alias__Abstract_s...2023-11-06T08:47:52ZBasile ClémentAlias plugin's `Abstract_state` API requires using private `Alias__Abstract_state` moduleThe Alias plugin exposes [the `Abstract_state` module](https://git.frama-c.com/pub/frama-c/-/blob/master/src/plugins/alias/abstract_state.mli) through [`API.mli`](https://git.frama-c.com/pub/frama-c/-/blob/master/src/plugins/alias/API.ml...The Alias plugin exposes [the `Abstract_state` module](https://git.frama-c.com/pub/frama-c/-/blob/master/src/plugins/alias/abstract_state.mli) through [`API.mli`](https://git.frama-c.com/pub/frama-c/-/blob/master/src/plugins/alias/API.mli).
However, OCaml doesn't know that the modules `G` and `LSet` used in the `Abstract_state` module are the same as those exposed in the `API` module, even though [they are](https://git.frama-c.com/pub/frama-c/-/blob/master/src/plugins/alias/API.ml#L26-28), because the `.mli` do not expose this information. To use `API.Abstract_state` in a meaningful way, the `G` and `LSet` modules must be accessed through the private `Alias__Abstract_state` module generated by `dune`.Jan RochelJan Rochelhttps://git.frama-c.com/pub/frama-c/-/issues/2668[EVA] unsoundness when initializing in switch statement before first case2023-09-20T08:51:15ZJulien Lepiller[EVA] unsoundness when initializing in switch statement before first case<!--
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.
-->
The following code is validated by EVA:
```c
#include <stdio.h>
int main(int argc, char *argv[]) {
switch(argc) {
int i = 5;
case 0:
i = 17;
// fall-through
default:
//@ assert i == 17;
printf("%d\n", i);
}
return 0;
}
```
The file is run through frama-c:
```bash
frama-c -eva test.c
```
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
Eva should not validate the assert, since "i" is possibly uninitialized. This is because in C, code between the switch statement and the first case is not executed. Note that frama-c-gui correctly shows that code as dead code.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
Eva validates the assert. No warnings are generated.
### Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *27.1 (Cobalt)*
- Plug-in used: *Eva*
- OS name: *Ubuntu*
- OS version: *22.04*
### 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.
-->
When using `-slevel 2` or above, Eva does not validate the assert, but still validates the generated `\initialized` assert for `printf`.
If `int i` is not initialized before the first case, Eva does not validate the assert. If a `break` is inserted, it does not validate the assert either.David BühlerDavid Bühlerhttps://git.frama-c.com/pub/frama-c/-/issues/2637libgnomecanvas disabled in brew2023-06-21T08:15:31ZLaura Titololibgnomecanvas disabled in brewTrying to install frama-c in a Mac machine, when executing
`brew libgnomecanvas`
an error occurs since the library is currently disabled.
The libgnomecanvas repository seems archived since November 29, 2022 (https://formulae.brew.sh/for...Trying to install frama-c in a Mac machine, when executing
`brew libgnomecanvas`
an error occurs since the library is currently disabled.
The libgnomecanvas repository seems archived since November 29, 2022 (https://formulae.brew.sh/formula/libgnomecanvas. https://gitlab.gnome.org/Archive/libgnomecanvas).https://git.frama-c.com/pub/frama-c/-/issues/2580Non ghost lvalue when assigning array (frama-c 22)2022-10-05T06:41:34ZRaul MontiNon ghost lvalue when assigning array (frama-c 22)The following code aborts when using the e-acsl plug-in of frama-c 22.0, while it passes when using frama-c 20.0. I paste the failing case output bellow. The warning mentions lines `//@ ghost int acopy[len];` and `//@ ghost acopy[i] = a[...The following code aborts when using the e-acsl plug-in of frama-c 22.0, while it passes when using frama-c 20.0. I paste the failing case output bellow. The warning mentions lines `//@ ghost int acopy[len];` and `//@ ghost acopy[i] = a[i];`. I am wondering if this is actually not allowed or if it is just a bug?
Regards,
Raúl Monti.
```
#include <stdio.h>
/*@ requires len >= 0;
@ requires \valid(a+(0..len-1));
@*/
void add1(int* a, int len) {
//@ ghost int acopy[len];
int i;
for(i = 0; i < len; i++) {
//@ ghost acopy[i] = a[i];
}
for(i = 0; i < len; i++) {
a[i] = a[i] + 1;
}
//@ assert \forall integer i; 0 <= i < len ==> a[i] == acopy[i] + 1;
}
int main() {
int a[3];
a[0] = 0;
a[1] = 1;
a[2] = 2;
add1(a, 3);
return 0;
}
```
The output I get when running e-acsl-gcc.sh add.c -c -O add in frama-c-22:
```
e-acsl-gcc.sh add.c -c -O add
+ frama-c -remove-unused-specified-functions -machdep gcc_x86_64 -cpp-extra-args= -std=c99 -D_DEFAULT_SOURCE -D__NO_CTYPE -D__FC_MACHDEP_X86_64 -no-frama-c-stdlib add.c -e-acsl -e-acsl-share=.../.opam/default/bin/../share/frama-c/e-acsl/ -then-last -print -ocode a.out.frama.c
[kernel] Parsing add.c (with preprocessing)
[kernel:ghost:bad-use] add.c:7: Warning:
Call to non-ghost function from ghost code is not allowed
[kernel:ghost:bad-use] add.c:10: Warning:
'*(acopy + i)' is a non-ghost lvalue, it cannot be assigned in ghost code
[e-acsl] beginning translation.
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[e-acsl] translation done in project "e-acsl".
[kernel] Warning: warning ghost:bad-use treated as deferred error. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.
```Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/372It is impossble to change log file without kinds of message changing.2022-09-28T14:06:22Zmantis-gitlab-migrationIt is impossble to change log file without kinds of message changing.ID0002274:
**This issue was created automatically from Mantis Issue 2274. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002274:
**This issue was created automatically from Mantis Issue 2274. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002274 | Frama-C | Kernel | public | 2017-01-19 | 2017-01-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Max P. | **Assigned To** | maroneze | **Resolution** | open |
| **Priority** | low | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
I wanted to explore how the analysis settings affect the output messages.
I changed settings and name of log file. But output messages were copied in the file that was pointed firstly.
Only if kinds of messages are changed a new file is created.
### Steps To Reproduce :
In GUI do follows:
1. Set -kernel-log rw:kernel.log
2. Run analysis
3. Verify that a file kernel.log was created.
4. Set -kernel-log rw:kernel2.log
5. Run analysis
6. Verify that a file kernel2.log was not created, but the time of last modification of the kernel.log was changed.
7. Set -kernel-log ruw:kernel2.log
8. Run analysis
9. Verify that a file kernel2.log was created.Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/128Syntax error in reorder_defs.ml after running make2022-09-28T11:13:02Zmantis-gitlab-migrationSyntax error in reorder_defs.ml after running makeID0002480:
**This issue was created automatically from Mantis Issue 2480. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002480:
**This issue was created automatically from Mantis Issue 2480. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002480 | Frama-C | Plug-in > clang | public | 2019-10-03 | 2019-10-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | gpajela | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | block | **Reproducibility** | have not tried |
| **Platform** | Linux x86_64 | **OS** | Ubuntu | **OS Version** | 18.04.3 LTS |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | - |
### Description :
I am trying to follow the instructions at https://frama-c.com/frama-clang.html to install Frama-Clang. However, I get a "Syntax error" after I run make:
$ make
Generating .Makefile.plugin.generated
Ocamlc intermediate_format.cmi
Ocamlc intermediate_format_parser.cmi
Ocamlc intermediate_format_parser.cmo
Ocamlc frama_Clang_option.cmi
Ocamlc frama_Clang_option.cmo
Ocamlc fclang_datatype.cmi
Ocamlc fclang_datatype.cmo
Ocamlc reorder_defs.cmi
Ocamlc reorder_defs.cmo
File "reorder_defs.ml", line 310, characters 6-10:
Error: Syntax error
/data/loewenheim/a/gpajela/.opam/default/share/frama-c/Makefile.generic:77: recipe for target 'reorder_defs.cmo' failed
make: *** [reorder_defs.cmo] Error 2
### Additional Information :
I am using Frama-C 19.0 Potassium, which I installed using opam pin. I am using version 2.0.4 of opam. I am using the default versions of OCaml and Clang for this version of Ubuntu: OCaml 4.05.0 and clang version 6.0.0.Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/1832journalization of -print option2022-07-12T07:07:41ZPatrick Baudinjournalization of -print optionID0001450:
**This issue was created automatically from Mantis Issue 1450. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001450:
**This issue was created automatically from Mantis Issue 1450. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001450 | Frama-C | Kernel | public | 2013-07-04 | 2013-09-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Loading a script file issued previously with -journal-enable option should perform the same job as previously done.
That is not the case with -print option:
Once the -print option is journalized, executing that journal performs two print!
> frama-c -print file.c -journal-enable
> frama-c -load-script frama_c_journal.ml
### Additional Information :
> cat file.c
//@ lemma l : 1 == 1;
> frama-c -print file.c -journal-enable
[kernel] preprocessing with "gcc -C -E -I. file.c"
/* Generated by Frama-C */
/*@ lemma l: 1 ? 1;
*/
[kernel] writing journal in file `frama_c_journal.ml'.
> frama-c -load-script frama_c_journal.ml
[kernel] preprocessing with "gcc -C -E -I. file.c"
/* Generated by Frama-C */
/*@ lemma l: 1 ? 1;
*/
/* Generated by Frama-C */
/*@ lemma l: 1 ? 1;
*/Julien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/2593Build failure if only the eva plugin is selected: -rectypes is required2022-07-11T15:44:07Zfx-cartonBuild failure if only the eva plugin is selected: -rectypes is required### Steps to reproduce the issue
- untar the frama-c-24.0 sources
- configure with: --disable-landmarks --with-no-plugin --enable-gui --enable-callgraph --enable-server --enable-eva
- make
### Expected behaviour
Compilation succeeds
#...### Steps to reproduce the issue
- untar the frama-c-24.0 sources
- configure with: --disable-landmarks --with-no-plugin --enable-gui --enable-callgraph --enable-server --enable-eva
- make
### Expected behaviour
Compilation succeeds
### Actual behaviour
Compilation fails with the following message:
```
Ocamlc src/plugins/value/domains/multidim_domain.cmo
File "src/plugins/value/domains/multidim_domain.ml", line 1:
Error: Invalid import of Abstract_memory, which uses recursive types.
The compilation flag -rectypes is required
make: *** [share/Makefile.generic:78: src/plugins/value/domains/multidim_domain.cmo] Error 2
```
### Contextual information
- Frama-C installation mode: from source
- Frama-C version: 24.0
- Plug-in used: Eva (and dependencies)
- OS name: Linux
- OS version: Gentoo linux
### Additional information (optional)
- With no configure options, it builds fine.
- I've tried to debug the issue, and I think this is caused by having "-rectypes" added to BFLAGS for the rule compiling src/kernel_services/abstract_interp/abstract_memory.mli; which seems to be added as a side effect of the following line in the Makefile:
```
src/kernel_services/abstract_interp/abstract_memory.cmo: BFLAGS += -rectypes
```
For some reason, the dependency tree happens to change between the two configurations (default ./configure and ./configure with the aforementioned options), and in the latter case, the .cmi is a dependency of the .cmo, and thus inherits the local variables including BFLAGS.
- If I run `make src/kernel_services/abstract_interp/abstract_memory.cmi` and then `make`, it builds fine, because in the first make invocation the .cmo is not in the dependency tree, so -rectypes won't be added.Andre MaronezeAndre Maronezehttps://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/181Missing cast in code generated by RTE2021-04-20T07:27:57ZJulien SignolesMissing cast in code generated by RTEID0002419:
**This issue was created automatically from Mantis Issue 2419. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002419:
**This issue was created automatically from Mantis Issue 2419. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002419 | Frama-C | Plug-in > RTE | public | 2018-12-17 | 2018-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
==========
int main(void) {
int i = 2;
unsigned int j = i < 2;
return 0;
}
$ frama-c -check -rte -warn-unsigned-downcast -print -ocode res.c
[kernel] Parsing a.c (with preprocessing)
[rte] annotating function main
/* Generated by Frama-C */
int main(void)
{
int __retres;
int i = 2;
/*@ assert rte: unsigned_downcast: (i < 2) ≤ 4294967295; */
/*@ assert rte: unsigned_downcast: 0 ≤ (i < 2); */
unsigned int j = (unsigned int)(i < 2);
__retres = 0;
return __retres;
}
$ frama-c res.c
[kernel] Parsing res.c (with preprocessing)
[kernel:annot-error] res.c:6: Warning:
comparison of incompatible types: 𝔹 and ℤ. Ignoring code annotation
[kernel] User Error: warning annot-error treated as fatal error.
==========
The terms (i < 2) should be casted to int in the generated predicatesJulien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/180E-ACSL crash with RTE generated assertion with booleans2021-04-20T07:09:09Zmantis-gitlab-migrationE-ACSL crash with RTE generated assertion with booleansID0002412:
**This issue was created automatically from Mantis Issue 2412. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002412:
**This issue was created automatically from Mantis Issue 2412. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002412 | Frama-C | Plug-in > E-ACSL | public | 2018-12-03 | 2018-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | rmalak | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Linux x86_64 | **OS Version** | Debian Sid |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
There might be a regression with the RTE or E-ACSL plugin with Argon.
/////////// boolean.c
#include <stdbool.h>
bool return_false(void)
{
return false;
}
int main(void)
{
return 0;
}
///////////////////////////
### Additional Information :
On Chlorine-20180502 (bfd93b819) :
$ frama-c -machdep x86_64 boolean.c -rte -print -ocode rte_boolean.c
[kernel] Parsing boolean.c (with preprocessing)
[rte] annotating function main
[rte] annotating function return_false
$ frama-c -machdep x86_64 rte_boolean.c -e-acsl
[kernel] Parsing local-frama-c/share/frama-c/e-acsl/e_acsl_gmp_api.h (with preprocessing)
[kernel] Parsing local-frama-c/share/frama-c/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing rte_boolean.c (with preprocessing)
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
### Steps To Reproduce :
On Argon 18.0 (2f7a0eee0) :
$ frama-c -machdep x86_64 boolean.c -rte -print -ocode rte_boolean.c
[kernel] Parsing boolean.c (with preprocessing)
[rte] annotating function main
[rte] annotating function return_false
$ frama-c -machdep x86_64 rte_boolean.c -e-acsl
[kernel] Parsing local-frama-c/share/frama-c/e-acsl/e_acsl_gmp_api.h (with preprocessing)
[kernel] Parsing local-frama-c/share/frama-c/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing rte_boolean.c (with preprocessing)
[e-acsl] beginning translation.
[kernel] Current source was: rte_boolean.c:10
The full backtrace is:
Raised at file "src/libraries/project/project.ml", line 402, characters 50-57
Called from file "src/plugins/e-acsl/main.ml", line 155, characters 12-1023
Called from file "src/plugins/e-acsl/main.ml", line 121, characters 12-34
Called from file "src/libraries/project/state_builder.ml", line 565, characters 17-22
Called from file "src/plugins/e-acsl/main.ml", line 255, characters 11-56
Called from file "queue.ml", line 105, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 792, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 822, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 229, characters 4-8
Unexpected error (Stack overflow).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is 18.0 (Argon).
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_guidelines
## Attachments
- [boolean.c](/uploads/1b34c066b4dc860013dcc10c38a49aad/boolean.c)Julien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/2445Frama-C/Jessie: memory set problem2021-04-15T09:17:47ZVirgile PrevostoFrama-C/Jessie: memory set problemID0000039:
**This issue was created automatically from Mantis Issue 39. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000039:
**This issue was created automatically from Mantis Issue 39. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000039 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2009-11-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
[bug 7548 from old bts, reported by Dillon Pariente]
Hello,
(Issue already sent to discussion-list, and now registred into the BTS! Sorry for this "duplication".)
Launching:
frama-c.byte.exe -jessie-analysis -jessie-gen-goals foo.c
with foo.c containing:
//*****************************************
typedef struct {int i;int j;} las;
/*@ requires \valid(a) && \valid(b);
assigns *a, *b; */
void g (int *a,int *b){ *a=11; *b=15; }
/*@ requires \valid(p) ;
assigns p->i,p->j;
*/
void f (las *p)
{ g (&(p->i), &(p->j)); }
//*****************************************
returns the following error (Jessie/Why version is 2.18):
memory (mem-field(int_M),b_21)
in memory set (mem-field(int_M),a_20),
(mem-field(int_M),b_21)
File "jc/jc_interp_misc.ml", line 716, characters 7-7:
Uncaught exception: File "jc/jc_interp_misc.ml", line 716, characters 7-13: Assertion failed
Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs foo.cloc foo.jcClaude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2456Frama-C/Jessie: typing error2021-04-15T09:17:47ZVirgile PrevostoFrama-C/Jessie: typing errorID0000040:
**This issue was created automatically from Mantis Issue 40. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000040:
**This issue was created automatically from Mantis Issue 40. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000040 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2009-10-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
[bug 7554 from old bts, reported by Dillon Pariente]
Hello,
The two following files can be compiled separately:
//===== FILE FOO.c
typedef struct {float k;} las;
void g (float * y);
void f (las *c) { g(&(c->k)); }
//===== FILE SPECS.h
typedef struct {float k;} las;
//@ requires \valid(c); assigns c->k;
void f (las * c);
but the command line below:
//===== COMMAND LINE
frama-c.byte.exe -jessie-analysis -jessie-gui FOO.c SPECS.h
generates the following error:
//===== STDOUT
Calling Jessie tool in subdir wholeprogram.jessie File "wholeprogram.jc", line 401, characters 15-26: typing
error: type float_P[..] expected instead of real
Jessie subprocess failed: jessie -why-opt -split-user-conj -v
-why-opt -fast-wp -separation -locs wholeprogram.cloc w
holeprogram.jcClaude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2357Jessie: struct field's validity2021-04-15T09:17:41ZDillon ParienteJessie: struct field's validityID0000102:
**This issue was created automatically from Mantis Issue 102. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000102:
**This issue was created automatically from Mantis Issue 102. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000102 | Frama-C | Plug-in > jessie | public | 2009-05-27 | 2010-07-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
(This issue was previously discussed through private messages but not fully resolved. It is now recorded into the BTS for traceability reasons.)
The following annotated code can not be proved by ATPs.
Function f() needs an invariant on global var v :
//@ global invariant aa: \valid(&v.c);
that should normally be generated automatically.
Function f2() needs a type invariant :
//@ type invariant Tt(las* l) = \valid(&(l->c)); but this type invariant is visibly not taken into account in the Why generated file (predicate Tt does exist but is not axiomatized).
Source code:
typedef struct { int c; } las;
las v;
//@ requires \valid(p);
void g(int * p);
void f(){ g(&v.c); }
//@ requires \valid(x);
void f2(las * x){ g(&(x->c)); }
Commande line:
frama-c -jessie-analysis -jessie-gui file.cClaude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2494type error in generated why file2021-04-15T09:17:39ZFabrice Derepastype error in generated why fileID0000178:
**This issue was created automatically from Mantis Issue 178. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000178:
**This issue was created automatically from Mantis Issue 178. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000178 | Frama-C | Plug-in > jessie | public | 2009-07-09 | 2009-07-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | derepas | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Let us consider the following program 'simple.c':
void g(int * j, int *k) {
int tmp= *j;
*j=*k;
*k=tmp;
}
void f(int * vector, int size) {
int i=0;
if (i<size)
g (&vector[i],&vector[i+1]);
}
The command line 'frama-c -main f -jessie simple.c' generates the following error:
[kernel...] preprocessing with "gcc -C -E -I. -dD simple.c"
Starting Jessie translation
Producing Jessie files in subdir simple.jessie
File simple.jessie/simple.jc written.
File simple.jessie/simple.cloc written.
Calling Jessie tool in subdir simple.jessie
Generating Why function g
Generating Why function f
Calling VCs generator.
gwhy-bin [...] why/simple.why
Computation of VCs...
File "why/simple.why", line 552, characters 9-49:
Term i is expected to have type int
make: *** [simple.stat] Erreur 1
Jessie subprocess failed: make -f simple.makefile gui
The funny thing is that when the body of function g is empty this error does not occur (though the error seems to be in function f).Claude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2339assigns nothing ?2021-04-15T09:17:13Zmantis-gitlab-migrationassigns nothing ?ID0000617:
**This issue was created automatically from Mantis Issue 617. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000617:
**This issue was created automatically from Mantis Issue 617. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000617 | Frama-C | Plug-in > jessie | public | 2010-10-26 | 2010-11-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jnarboux | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi,
Using the following example:
/*@
ensures \result == 1;
assigns \nothing;
*/
int foo()
{
int v[9];
v[0] =1;
return 1;
}
I get:
[kernel] preprocessing with "gcc -C -E -I. -dD bug.c"
[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir bug.jessie
[jessie] File bug.jessie/bug.jc written.
[jessie] File bug.jessie/bug.cloc written.
[jessie] Calling Jessie tool in subdir bug.jessie
Generating Why function foo
[jessie] Calling VCs generator.
gwhy-bin [...] why/bug.why
Computation of VCs...
File "why/bug.why", line 392, characters 20-42:
Unbound variable int_P_v_1_alloc_table
make: *** [bug.stat] Erreur 1
is it normal ? if I remove the assign nothing it works.
Julien NarbouxClaude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/526zombie processes (again)2021-04-15T08:46:59ZJens Gerlachzombie processes (again)ID0002205:
**This issue was created automatically from Mantis Issue 2205. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002205:
**This issue was created automatically from Mantis Issue 2205. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002205 | Frama-C | Plug-in > wp | public | 2016-02-01 | 2016-02-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | - |
### Description :
This is related #2154 and #2132.
I have updated my Frama-C installation under OS X with a patch provided by Loïc Correnson.
The situation has improved in the sense that my system is not so sluggish anymore but there still a substantial number of zombie processes: 86 (before the patch I counted 111 for the same example).
## Attachments
- [command.ml](/uploads/53d60edd523f389028615aaf8ed6c2a3/command.ml)
- [command.mli](/uploads/bf305b67d611a41cda9b7c025b58739d/command.mli)
- [task.ml](/uploads/122a5d6e2d50c4bfcf7d91c4148a15ea/task.ml)
- [task.mli](/uploads/2c222544f2dd773830d8266c242cc2d4/task.mli)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/371translation to why3 of int* argument to logic function2021-04-15T08:10:47ZJochen Burghardttranslation to why3 of int* argument to logic functionID0002275:
**This issue was created automatically from Mantis Issue 2275. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002275:
**This issue was created automatically from Mantis Issue 2275. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002275 | Frama-C | Plug-in > wp | public | 2017-02-02 | 2017-02-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Silicon-20161101 | **OS** | xubuntu 16.04.1 LTS | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-prover eprover foo.c" proves lemma "foo" in line 7, although it essentially says that no objects of type "int*" exist at all.
The problem disappears if either
(1) the result type "int" of "deref" is changed to "integer" in line 3,
(2) "deref" is inlined at line 5,
(3) "large" is inlined at line 7, or
(4) "large(s) && !large(s)" is simplified to "\false" in line 7.
Using option "-wp-out", and comparing the files "Axiomatic.why" before and after change (1), see attached files "Axiomatic_int.why" and "Axiomatic_integer.why", reveals that the former has an "axiom Q_TL_deref" while the latter does not. This axiom essentially says that any value fetched from an integer array (i.e. a "map addr int" in why3 language) is already an int (i.e. satisfies "is_sint32" in why3 language), which imho is wrong.
When using "-wp alt-ergo" instead of "-wp eprover", the generated mlw files before and after change (1) literally agree, see attached file "lemma_foo_Alt-Ergo_int.mlw" and "lemma_foo_Alt-Ergo_integer.mlw"; they contain no occurrence of "deref" or "large".
The input given to eprover has been intercepted and boiled down as far as possible, resulting in file "foo_eprover_input.p" which is attached for convenience. Its axiom "q_TL_deref" in line 18 is a boiled-down translation of axiom "Q_TL_deref" from the why3 file, and is wrong as argued above.
## Attachments
- [foo.c](/uploads/820f364a77e732e708ee0a21ae3d0123/foo.c)
- [Axiomatic_int.why](/uploads/10f847d1cf681d6ecde0ea21bab12d96/Axiomatic_int.why)
- [Axiomatic_integer.why](/uploads/3493da1d13894db1a171428f9e5c269e/Axiomatic_integer.why)
- [lemma_foo_Alt-Ergo_int.mlw](/uploads/ffc94494f9b1a25f6bc9ff99c712ec1e/lemma_foo_Alt-Ergo_int.mlw)
- [lemma_foo_Alt-Ergo_integer.mlw](/uploads/ee7e41ba4da81b0485dc5e5cc5d53a89/lemma_foo_Alt-Ergo_integer.mlw)
- [foo_eprover_input.p](/uploads/c00d2b593bcbd384b5bc9781d696e9b7/foo_eprover_input.p)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/878insufficient precoditions given to Alt-Ergo to prove validity of memory acces...2021-04-15T07:31:44ZJochen Burghardtinsufficient precoditions given to Alt-Ergo to prove validity of memory access for user-defined "->" operatorID0002026:
**This issue was created automatically from Mantis Issue 2026. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002026:
**This issue was created automatically from Mantis Issue 2026. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002026 | Frama-Clang | Plug-in > wp | public | 2014-12-11 | 2015-02-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The goal given to Alt-Ergo for the memory access in line 13 is:
566 goal main_assert_rte_mem_access:
567 forall t_1,t : int farray.
568 forall a : addr.
569 linked(t) ->
570 valid_rw(t_1, shiftfield_F__Z1X_a(a), 1)
where "t_1" doesn't appear outside the conclusion (line 570), and therefor the formula doesn't hold.
It looks like some "assigns \nothing" was missing in the C++ source; however, there is no more place where such a contract could be added. Maybe some function that is used internally by Cxx needs an additional "assigns" clause?
## Attachments
- [402.cpp](/uploads/a8e1183a90e9cb8e331049d590b3eaa2/402.cpp)
- [main_assert_rte_mem_access_Alt-Ergo.mlw](/uploads/b5497d0bcb4de5a5afd6458a58f4e8ac/main_assert_rte_mem_access_Alt-Ergo.mlw)
- [402a.cpp](/uploads/e84e1416b4bf04f413a3f61071eeb1c4/402a.cpp)Loïc CorrensonLoïc Correnson