frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2024-03-14T10:51:28Zhttps://git.frama-c.com/pub/frama-c/-/issues/2692[alias] expose more functions2024-03-14T10:51:28ZJan Rochel[alias] expose more functionsCopied from https://git.frama-c.com/pub/frama-c/-/issues/2677#note_229339 by @bclement-ocp
Some additional functions need to be exposed in the `Abstract_state` for programmatic use if access to the underlying graph is needed (I need to ...Copied from https://git.frama-c.com/pub/frama-c/-/issues/2677#note_229339 by @bclement-ocp
Some additional functions need to be exposed in the `Abstract_state` for programmatic use if access to the underlying graph is needed (I need to iterate over all equivalence classes, and I think only raw access to the graph allows this).
More precisely:
* `get_lval` / `find_aliases` now only returns variable aliases; there is `reconstruct_lvals` internally to compute all the aliases but it is not exposed (it is used by find_all_aliases, but that also brings aliases from other equivalence classes);
* edge labels are not exposed, so it is not possible to distinguish between pointer and field edges from outside the plugin, making raw access to the graph impossible to do correctly
Would it be possible to expose `EdgeLabel `and (an equivalent of) `reconstruct_lvals` from the plugin's API?Jan RochelJan Rochelhttps://git.frama-c.com/pub/frama-c/-/issues/2691Cannot use ppx_inline_test in a Frama-C plugin2024-02-28T22:02:33Zpepega007xdCannot use ppx_inline_test in a Frama-C plugin<!--
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
Setup a minimal Frama-C plugin which uses the `ppx_inline_tests` test runner, and run tests using `dune runtest`.
The test runner is configured according to this documentation: https://dune.readthedocs.io/en/stable/tests.html#inline-tests
Project structure:
```
hello/
├── dune
├── dune-project
└── hello.ml
```
dune-project:
```
(lang dune 3.2)
(using dune_site 0.1)
(name frama-c-hello)
(package (name frama-c-hello))
```
dune:
```
(library
(name hello)
(public_name frama-c-hello.core)
(libraries frama-c.kernel)
(preprocess (pps ppx_inline_test))
(inline_tests)
)
(plugin
(optional)
(name hello)
(libraries frama-c-hello.core)
(site (frama-c plugins))
)
```
hello.ml:
```ml
let%test "should fail" = 1 = 2
```
### Expected behaviour
The test inside `hello.ml` executes and prints an assertion error.
### Actual behaviour
Building the test fails with the following error:
```
Error: No implementation found for virtual library "frama-c.init" in
/home/tb/.opam/default/lib/frama-c/init.
-> required by library "frama-c.kernel" in
/home/tb/.opam/default/lib/frama-c/kernel
-> required by library "frama-c-hello.core" in _build/default
-> required by
_build/default/.hello.inline-tests/inline_test_runner_hello.exe
-> required by _build/default/.hello.inline-tests/partitions-best
-> required by alias runtest in dune:6
```
### Contextual information
- Frama-C installation mode: installed using `opam install frama-c`
- Frama-C version: 28.0 (Nickel)
- Plug-in used: minimal plugin
- OS name: Fedora Linux
- OS version: 38 (Workstation Edition)
### Additional information (optional)
The project build just fine using `dune build`, only the `@runtest` target fails to build.https://git.frama-c.com/pub/frama-c/-/issues/2690[WP] Frama-C/WP 28.0 does not work with Isabelle/HOL2024-03-06T11:53:41Zkwaxer[WP] Frama-C/WP 28.0 does not work with Isabelle/HOL### Steps to reproduce the issue
1. Make sure Isabelle/HOL is installed and `why3` is configured to use it.
2. Create file `test.h` with the following code:
```
/*@
logic \list<integer> enumeration (integer n) = n == 0 ? \Nil : enu...### Steps to reproduce the issue
1. Make sure Isabelle/HOL is installed and `why3` is configured to use it.
2. Create file `test.h` with the following code:
```
/*@
logic \list<integer> enumeration (integer n) = n == 0 ? \Nil : enumeration (n - 1) ^ [|n - 1|];
lemma enumeration_length: \forall integer n; 0 <= n ==> \length (enumeration (n)) == n;
*/
```
3. Run WP plugin selecting Isabelle/HOL as a backend: `frama-c -wp -wp-prover=why3:isabelle -wp-interactive=fix -wp-cache=none test.h`
### Expected behaviour
Earlier versions of Frama-C (e.g. 27.1) produce the following output:
```
[kernel] Parsing test.h (with preprocessing)
[wp] 1 goal scheduled
[wp] Proved goals: 1 / 1
Qed: 0
Isabelle 2022: 1 (8.1s)
```
with the theory
```isabelle
theory lemma_enumeration_length imports Why3.Why3 begin
why3_open "lemma_enumeration_length.xml"
why3_vc wp_goal
using assms L_enumeration_def
by (induction i) (simp_all add: facts.length_concat length_cons length_nil)
why3_end
end
```
### Actual behaviour
Frama-C 28.0 produces the following:
```
[kernel] Parsing test.h (with preprocessing)
[wp] 1 goal scheduled
[wp] [Failure] typed_lemma_enumeration_length (Isabelle)
[wp] Proved goals: 0 / 1
Qed: 0
Failed: 1
```
### Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *28.0 (Nickel)*
- Plug-in used: *WP*
- OS name: *Ubuntu*
- OS version: *22.04.4 LTS*
### Additional information (optional)
`-wp-msg-key why3_api` gives the following error trace:
```
[wp] Failure: [Why3 Error] anomaly: Sys_error(".../.frama-c/wp/interactive/lemma_enumeration_length/.xml: No such file or directory")
Raised by primitive operation at Stdlib.open_out_gen in file "stdlib.ml", line 331, characters 29-55
Called from Stdlib.open_out in file "stdlib.ml" (inlined), line 336, characters 2-74
Called from Frama_c_kernel__Command.pp_to_file in file "src/libraries/utils/command.ml", line 31, characters 13-35
Called from Wp__ProverWhy3.prepare in file "src/plugins/wp/ProverWhy3.ml", line 1339, characters 6-130
Called from Wp__ProverWhy3.interactive in file "src/plugins/wp/ProverWhy3.ml", line 1352, characters 8-37
Called from Wp__ProverWhy3.build_proof_task in file "src/plugins/wp/ProverWhy3.ml", line 1413, characters 8-59
```
There is an unexpected slash right the before `.xml` file extension.https://git.frama-c.com/pub/frama-c/-/issues/2689[wp] Failing to understand certain bitwise properties2024-02-14T11:19:42ZPhillip Allen Lane[wp] Failing to understand certain bitwise properties<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
I have the following Frama-C which should prove this seemingly trivial assertion about an integer containing all 1s:
```c
#include <stdint.h>
#define ALLONES 0xFFFFFFFFu
/*@
assigns \nothing;
*/
void tests(void)
{
uint32_t allones = ALLONES;
//@ assert \forall uint32_t i ; 0 <= i < 32 ==> (allones & (1u << i)) != 0;
}
```
### Expected behaviour
All goals should be proven.
### Actual behaviour
Running with:
```
frama-c -wp -wp-rte -wp-smoke-tests -wp-prover z3 -wp-par 32 -wp-print test.c
```
I get:
```
[kernel] Parsing test.c (with preprocessing)
[rte:annot] annotating function tests
[wp] 2 goals scheduled
[wp] [Timeout] typed_tests_assert (Qed 0.86ms) (Z3) (Cached)
[wp] [Cache] updated:1
[wp] Proved goals: 3 / 4
Terminating: 1
Unreachable: 1
Qed: 1
Timeout: 1
------------------------------------------------------------
Function tests
------------------------------------------------------------
Goal Assertion (file test.c, line 10):
Assume { (* Goal *) When: (0 <= i) /\ (i <= 31). }
Prove: land(4294967295, lsl(1, i)) != 0.
Prover Z3 4.8.12 returns Timeout (Qed:0.86ms) (2s)
------------------------------------------------------------
Goal Assigns nothing in 'tests':
Prove: true.
Prover Qed returns Valid
------------------------------------------------------------
```
### Contextual information
I have tried other provers (CVC4, Alt-Ergo) and none of them are able to prove the assertion. Looking at some of the Coq axioms generated, I am suspicious that Frama-C is not providing the SMT solvers with enough information about bitwise operations to be able to deduce the conclusion.
When I run Frama-C with a different assertion:
```c
//@ assert \forall uint32_t i ; i == 0 ==> (allones & (1u << i)) != 0;
```
The assertion succeeds (via Qed). This works for all valid values of `i` (e.g., `i in [0 .. 31]`), but fails when I try to quantify over the entire range.
Here's some relevant information that may be helpful:
- Frama-C installation mode: Opam
- Frama-C version: 28.0 (Nickel)
- Plug-in used: WPLoïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2688[wp] Failure: [Why3 Error] anomaly: Not_found2024-01-19T08:10:37ZJulia Lawall[wp] Failure: [Why3 Error] anomaly: Not_foundSee attached files. The output with the command line argument -wp-msg-key why3_api ends with the following. The attached directory contains a make file, so you can just run `make v1`.
```
> [wp:why3_api] of_term prop c_1.F1_cpumask_bi...See attached files. The output with the command line argument -wp-msg-key why3_api ends with the following. The attached directory contains a make file, so you can just run `make v1`.
```
> [wp:why3_api] of_term prop c_1.F1_cpumask_bits[0]=c_0.F1_cpumask_bits[0]
> [wp] Failure: [Why3 Error] anomaly: Not_found
> Raised at Qed__Term.Make.tau_of_arraysort in file
> "src/plugins/qed/term.ml", line 2831, characters 11-26
> Called from Wp__ProverWhy3.of_term in file "src/plugins/wp/ProverWhy3.ml", line 461, characters 14-29
> Called from Wp__ProverWhy3.of_term in file "src/plugins/wp/ProverWhy3.ml", line 450, characters 14-39
> Called from Wp__ProverWhy3.of_term.fold in file "src/plugins/wp/ProverWhy3.ml", line 453, characters 16-44
> Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
> Called from Wp__ProverWhy3.share in file "src/plugins/wp/ProverWhy3.ml", line 633, characters 10-33
> Called from Wp__ProverWhy3.successive_binders in file "src/plugins/wp/ProverWhy3.ml", line 669, characters 8-24
> Called from Wp__ProverWhy3.successive_binders in file "src/plugins/wp/ProverWhy3.ml", line 666, characters 23-49
> Called from Wp__ProverWhy3.successive_binders in file "src/plugins/wp/ProverWhy3.ml", line 666, characters 23-49
> Called from Wp__ProverWhy3.successive_binders in file "src/plugins/wp/ProverWhy3.ml", line 666, characters 23-49
> Called from Wp__ProverWhy3.successive_binders in file "src/plugins/wp/ProverWhy3.ml", line 666, characters 23-49
> Called from Wp__ProverWhy3.successive_binders in file "src/plugins/wp/ProverWhy3.ml", line 666, characters 23-49
> Called from Wp__ProverWhy3.successive_binders in file "src/plugins/wp/ProverWhy3.ml", line 666, characters 23-49
```
[files.tar.gz](/uploads/39c90bd26cf8493c15edcdffa8c55c24/files.tar.gz)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2687Ivette: server not running error2024-01-28T03:46:19ZHugo GimbertIvette: server not running errorHello,
I understand frama-c-gui is not available anymore for MacOSX,
so I tried to move to Ivette.
I performed a fresh install of frama-c
on my laptop (MacBookPro Apple M1 Max with macOs Sonoma).
using brew + opam, following the offi...Hello,
I understand frama-c-gui is not available anymore for MacOSX,
so I tried to move to Ivette.
I performed a fresh install of frama-c
on my laptop (MacBookPro Apple M1 Max with macOs Sonoma).
using brew + opam, following the official guidelines
https://frama-c.com/html/get-frama-c.html
Unfortunately, for the moment I am unable to use the new editor Ivette,
I cannot add any source file to the workspace.
There is a red blinking dot plus a warning sign at the bottom left of the editor
but I do not know how to interpret that.
When I open developper tools, I can see an error "Server not running" but I do not know which Server should be running.
Below is a screen shot of the problem
![image](/uploads/3329bfe5feef0132326781e04aa19af4/image.png)
What is the procedure to start the frama-c server required by Ivette?
Any help appreciated.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2686Frama-C cannot use Alt-Ergo 2.5.x by default with Why3 1.7.02024-01-11T12:34:19ZHugo GimbertFrama-C cannot use Alt-Ergo 2.5.x by default with Why3 1.7.0Installing Frama-C on Ubuntu 22.04 with opam consistently fails on several machines,
including mine and all of my student's using Ubuntu 22.04.
A solution is to downgrade from fraam-28.0 to framac-26.0.
Current patch for installing on ...Installing Frama-C on Ubuntu 22.04 with opam consistently fails on several machines,
including mine and all of my student's using Ubuntu 22.04.
A solution is to downgrade from fraam-28.0 to framac-26.0.
Current patch for installing on Ubuntu 22.04:
- follow the instructions at https://frama-c.com/html/get-frama-c.html
- opam remove --force frama-c
- opam install frama-c.26.0
- why3 config detectAllan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2685[WP] save / load not saving strategies2023-12-14T10:13:17ZTeo BERNIER[WP] save / load not saving strategies### Steps to reproduce the issue
On the attached examples :
[test.c](/uploads/8a2ca334a3a2ef8d696da2df986bdd45/test.c)
running the following command
`frama-c test.c -wp -wp-prover=tip -wp-prop post`
works perfectly, but when we u...### Steps to reproduce the issue
On the attached examples :
[test.c](/uploads/8a2ca334a3a2ef8d696da2df986bdd45/test.c)
running the following command
`frama-c test.c -wp -wp-prover=tip -wp-prop post`
works perfectly, but when we use the save / load features with the following command (and after removing the existing scripts)
`frama-c test.c -save tmp.sav ; frama-c -load tmp.sav -wp -wp-prover=tip -wp-prop post`
it does not work anymore and, when we add option
`-wp-strategy InstanceForall`,
Frama-C outputs
`[wp] Warning: Invalid -wp-strategy 'InstanceForall' (undefined strategy name)`
### Expected behaviour
We would expect save / load to keep strategies available.
### Actual behaviour
Strategies seems to not be correctly saved / loaded and when specified, they are declared `undefined` by WP.
### Contextual information
* Frama-C installation mode: opam install frama-c.28.0
* Frama-C version: 28.0
* Plug-in used: WP with why3 1.6.0 and Alt-Ergo 2.4.3
* OS name: Ubuntu
* OS version: 20.04
FYI: @nkosmatovhttps://git.frama-c.com/pub/frama-c/-/issues/2684[WP] crash observed with scripts and strategies2023-12-14T10:28:20ZNikolai Kosmatov[WP] crash observed with scripts and strategies### Expected behaviour
No crash
### Actual behaviour
Crash in some situations when running WP in the presence of existing scripts recorded via strategies.
Here is a screenshot (with a hidden full file name).
![crash_on_recorded_scri...### Expected behaviour
No crash
### Actual behaviour
Crash in some situations when running WP in the presence of existing scripts recorded via strategies.
Here is a screenshot (with a hidden full file name).
![crash_on_recorded_scripts](/uploads/11287a2731db4ea55108b4395f95b940/crash_on_recorded_scripts.png)
### Contextual information
- Frama-C installation mode: *Opam from public GIT*
- Frama-C version: *28.0+dev (Nickel)* commit cdd528, similar behavior observed on 28.0beta
- Plug-in used: *WP*
- OS name: *Ubuntu*
- OS version: *22.04*
FYI @tbernierhttps://git.frama-c.com/pub/frama-c/-/issues/2683[WP] non-matching of strategies with forall and implication2023-11-27T09:24:34ZTeo BERNIER[WP] non-matching of strategies with forall and implication### Steps to reproduce the issue
On the attached examples :
- [forall_pattern.c](/uploads/2df4b07af5737279a5d34001b7d10822/forall_pattern.c)
running the following command
`frama-c-gui forall_pattern.c -wp -wp-rte -wp-prover...### Steps to reproduce the issue
On the attached examples :
- [forall_pattern.c](/uploads/2df4b07af5737279a5d34001b7d10822/forall_pattern.c)
running the following command
`frama-c-gui forall_pattern.c -wp -wp-rte -wp-prover=tip -wp-prop post`
to apply a strategy with Instance does not seem to accept the pattern and to match the precondition using `\forall`.
```
strategy FastAltErgo: \prover("alt-ergo", 1); // run Alt-Ergo for 1 sec.
strategy InstanceForall:
\tactic("Wp.instance",
\pattern(\forall integer _; _), // fails to select the \forall (invalid pattern)
// \when(_), // works in this specific example
\goal(P_P(i)),
\param("P1", i),
\children(FastAltErgo)
);
proof InstanceForall: post;
```
- [implication_pattern.c](/uploads/8c4a42b5917b980ffe994189507fb7c6/implication_pattern.c)
running the following command
`frama-c-gui implication_pattern.c -wp -wp-rte -wp-prover=tip -wp-prop post`
to apply a strategy with Cut does not seem to accept the pattern and to match the precondition using `==>`.
```
strategy FastAltErgo: \prover("alt-ergo", 1); // run Alt-Ergo for 1 sec.
strategy CutImplication:
\tactic("Wp.cut",
\pattern(A ==> _), // fails to select the implication (invalid pattern)
// \incontext(A: _ <= 99), // works in this specifi example
\param("case", "CASES"),
\param("clause", A),
\children(FastAltErgo)
);
proof CutImplication: post;
```
### Expected behaviour
We would expect `\forall` and `==>` to be matched like other acsl expression.
### Actual behaviour
Syntax error is reported (Invalid pattern. Ignoring global annotation).
### Contextual information
- Frama-C installation mode: opam pin add frama-c https://git.frama-c.com/pub/frama-c.git#64438ed52f9af0052d6f3970202fc48dbc580dba
- Frama-C version: 28.0+dev (commit 64438ed52f9af0052d6f3970202fc48dbc580dba)
- Plug-in used: WP with why3 1.6.0 and Alt-Ergo 2.5.2
- OS name: Ubuntu
- OS version: 22.04
FYI: @nkosmatovLoïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2682[WP] Preservation of "is_finite" property2023-11-24T10:40:34ZArnaud Fontaine[WP] Preservation of "is_finite" property### Steps to reproduce the issue
Run the following example with the command
`frama-c -wp-model typed+int+float -wp-rte -wp-timeout 5 -wp test.c`
```
#include <__fc_builtin.h>
/*@
@requires \valid(vec + (0 .. (size - 1)));
@require...### Steps to reproduce the issue
Run the following example with the command
`frama-c -wp-model typed+int+float -wp-rte -wp-timeout 5 -wp test.c`
```
#include <__fc_builtin.h>
/*@
@requires \valid(vec + (0 .. (size - 1)));
@requires \forall unsigned i; i < size ==> \is_finite(vec[i]);
@requires \forall unsigned i; i < size ==> !\is_NaN(vec[i]);
@terminates \true;
@ensures \forall unsigned i; i < size ==> \is_finite(vec[i]);
@ensures \forall unsigned i; i < size ==> !\is_NaN(vec[i]);
@ensures \forall unsigned i; i < size ==> vec[i] == \old(vec)[i];
@assigns vec[0 .. (size - 1)];
@*/
extern void vec_nop(double * const vec, unsigned const size);
void vec_nop(double * const vec, unsigned const size) {
/*@
@loop invariant i <= size;
@loop invariant \forall unsigned x; x < i ==> \is_finite(vec[x]);
@loop invariant \forall unsigned x; x < i ==> !\is_NaN(vec[x]);
@loop invariant \forall unsigned x; x < i ==> vec[x] == \at(vec, LoopEntry)[x];
@loop assigns i;
@loop variant (size - i);
@*/
for (unsigned i = 0; i < size; ++i) {
}
}
/*@
@requires \valid(vec + (0 .. (size - 1)));
@requires \forall unsigned i; i < size ==> \is_finite(vec[i]);
@requires \forall unsigned i; i < size ==> !\is_NaN(vec[i]);
@terminates \true;
@ensures \forall unsigned i; i < size ==> \is_finite(vec[i]);
@ensures \forall unsigned i; i < size ==> !\is_NaN(vec[i]);
@ensures \forall unsigned i; i < size ==> vec[i] == \old(vec)[i];
@assigns vec[0 .. (size - 1)];
@*/
extern void vec_ident(double * const vec, unsigned const size);
void vec_ident(double * const vec, unsigned const size) {
/*@
@loop invariant i <= size;
@loop invariant \forall unsigned x; x < i ==> \is_finite(vec[x]);
@loop invariant \forall unsigned x; x < i ==> !\is_NaN(vec[x]);
@loop invariant \forall unsigned x; x < i ==> vec[x] == \at(vec, LoopEntry)[x];
@loop assigns i;
@loop assigns vec[0 .. (size - 1)];
@loop variant (size - i);
@*/
for (unsigned i = 0; i < size; ++i) {
vec[i] = vec[i];
}
}
```
### Expected behaviour
All properties should be validated.
### Actual behaviour
In the given example, all properties of the `vec_nop` are correctly verified with WP. However, in the `vec_ident` function below where the only difference with the `vec_nop` function is the addition of the statement `vec[i] = vec[i];` in the loop, the loop invariant `\is_finite(vec[x])` is not verified anymore.
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 27.1 (Cobalt)
- Plug-in used: WP
- OS name: Linux
### Additional information (optional)
When using model `typed+int+real` all properties are validated...Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2681[kernel] Conflicting types error for enum & typedef enum2024-01-17T11:25:46ZT-Gruber[kernel] Conflicting types error for enum & typedef enumI have encountered a problem that leads to an error when parsing. This occurs when an enum is defined multiple times as shown below. The expectation would be that it works as with the struct shown:
- forward declaration of struct/enum
- ...I have encountered a problem that leads to an error when parsing. This occurs when an enum is defined multiple times as shown below. The expectation would be that it works as with the struct shown:
- forward declaration of struct/enum
- introducing an alias via typedef
- both in one
```C
// test.c
// works
struct my_struct;
typedef struct my_struct my_struct;
typedef struct my_struct {
int val;
} my_struct;
// fails
enum my_enum;
typedef enum my_enum my_enum;
typedef enum my_enum {
VAL
} my_enum;
```
### Steps to reproduce the issue
Parse source file:
```
frama-c test.c
```
### Expected behaviour
Output:
```
[kernel] Parsing test.c
```
### Actual behaviour
Output:
```
[kernel] Parsing test.c
[kernel] test.c:14: User Error:
redefinition of type 'my_enum' in the same scope with conflicting type.
Previous declaration was at test.c:10
[kernel] User Error: stopping on file "test.c" that has errors.
[kernel] Frama-C aborted: invalid user input.
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 27.0 (Cobalt)
- OS: Ubuntu 22.04.2 LTS (WSL)https://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/2679\separated for stack-allocated variable length arrays2023-11-20T07:30:50ZAdharsh Kamath\separated for stack-allocated variable length arraysI have been trying to verify the following program with Frama-c (WP plugin).
```
#include <stdlib.h>
#define assume(e) if(!(e)) exit(-1);
extern int unknown_int(void);
int N;
int main()
{
N = unknown_int();
if(N <=0 )...I have been trying to verify the following program with Frama-c (WP plugin).
```
#include <stdlib.h>
#define assume(e) if(!(e)) exit(-1);
extern int unknown_int(void);
int N;
int main()
{
N = unknown_int();
if(N <=0 ) return 1;
int i;
int a[N];
int b[N];
a[0] = 0;
b[0] = 1;
//@ assert b[0] == 1;
//@ assert \separated(a,b);
//@ assert a[0] == 0;
return 1;
}
```
For which frama-c, outputs the following statuses for each assertion
```
Assertion 0 < sizeof(int) * N <= 18446744073709551615: Valid
Assertion 0 < sizeof(int) * N <= 18446744073709551615: Valid
Assertion *(b + 0) == 1: Valid
Assertion \separated(a + 0, b + 0): Unknown
Assertion *(a + 0) == 0: Partially proven
```
When I change one of the arrays to a constant-sized array, say b to int [100], the output changes to
```
Assertion 0 < sizeof(int) * N <= 18446744073709551615: Valid
Assertion b[0] == 1: Valid
Assertion \separated(a + 0, &b[0]): Valid
Assertion *(a + 0) == 0: Valid
```
Is it not fair to assume stack-allocated arrays don't alias? Why does Frama-c treat variable length arrays differently from constant-sized ones?Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2678Turn off implicit promotion of float and double2023-11-20T07:30:29ZAdharsh KamathTurn off implicit promotion of float and doubleI have a function `f` whose post-condition I want to verify. Following is the function `f` along with its ensures clause:
```c
/*@
ensures \result == x - (x*x*x)/6.0f;
*/
float f(float x)
{
return x - (x*x*x)/6.0f;
}
```
Frama-C, (wi...I have a function `f` whose post-condition I want to verify. Following is the function `f` along with its ensures clause:
```c
/*@
ensures \result == x - (x*x*x)/6.0f;
*/
float f(float x)
{
return x - (x*x*x)/6.0f;
}
```
Frama-C, (with WP only) returns "Unknown" as the status of this post-condition. Does this have anything to do with the implicit promotion of floats to reals?
From the ACSL Implementation document ([https://frama-c.com/download/frama-c-acsl-implementation.pdf](https://frama-c.com/download/frama-c-acsl-implementation.pdf), Section 2.2.5):
> Unlike the promotion of C integer types to mathematical integers, there are special float values that do not naturally map to a real number, namely the IEEE-754 special values for “not-a-number”, +∞ and −∞. See below for a detailed discussion on such special values. However, remember that ACSL’s logic has only total functions. Thus, there are implicit promotion functions `real_of_float` and `real_of_double` whose results on
the 3 values above is left unspecified.
Is there a way to turn off this implicit promotion of `float` to `real`?
**More importantly, is there a way to verify the post-condition of functions like `f` (given above), that involve floating point values?**Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2677Alias plugin does not propagate inside records and arrays2024-03-09T12:39:09ZBasile ClémentAlias plugin does not propagate inside records and arraysThe Alias plug-in does not seem to know that if `p` points to `x`, then `x.ptr` and `p->ptr` are the same. This is also the case for pointers to arrays of pointers (with `*(*)[]` types).
The attached files should reproduce the issue; wh...The Alias plug-in does not seem to know that if `p` points to `x`, then `x.ptr` and `p->ptr` are the same. This is also the case for pointers to arrays of pointers (with `*(*)[]` types).
The attached files should reproduce the issue; when running them through `frama-c -alias` I get
```
[alias] May-aliases at the end of function main:
{ a; t.field } { z; q } { z->field; b } { q->field; n }
```
which places the pointers `a`, `b` and `n` in different classes even though we can check by running the program that `a == b` and `a == n` hold at the end of the `main` function.
Note that in the plug-in's README, "pointer arithmetic, and array and structure accesses" is listed under "imprecisely-supported constructs", so this may be expected — however it would be surprising to me that "imprecisely-supported" means "unsound".
[records.c](/uploads/8864c33684705ab86d725ccbe5ba3e38/records.c)
[arrays.c](/uploads/11360a2237d2be19e3359dcfabe7157d/arrays.c)Jan RochelJan Rochelhttps://git.frama-c.com/pub/frama-c/-/issues/2676E-ACSL : non-existent assigns clause in behavior2023-11-09T08:24:50ZYani ZIANIE-ACSL : non-existent assigns clause in behavior<!--
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.
-->
Run the following code with E-ACSL using ``e-acsl-gcc.sh -c -O assigns_test.out assigns_test.c``:
```C
/* assigns_test.c */
#include <limits.h>
int global_int;
/*@
requires INT_MIN < global_int < INT_MAX;
assigns global_int;
*/
int abs_global(){
if(global_int < 0) {return -global_int;}
return global_int;
}
int main(){
global_int = 0;
int local_int = abs_global();
return local_int;
}
```
### Expected behaviour
Instrumentation happens without warning.
### Actual behaviour
The following warning ``[e-acsl] assigns_test.c:9: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported.`` is reported, despite the function contract of ``abs_global`` not featuring any behavior.
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: at least from 26, still there in 28~beta
- Plug-in used: E-ACSL
- OS name: Ubuntu (via WSL)
- OS version: 22.04.2 LTS
FYI @nkosmatov
<!--
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.
-->Julien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/2675Unclear status for loop invariants in CSV report2023-11-06T08:45:05ZAdharsh KamathUnclear status for loop invariants in CSV reportThe meaning of the status for each loop invariant in the CSV file output by the report plugin is unclear. The WP plugin manual does not contain any details regarding the same.
What does "Unknown" or "Partially Proven" status mean for a l...The meaning of the status for each loop invariant in the CSV file output by the report plugin is unclear. The WP plugin manual does not contain any details regarding the same.
What does "Unknown" or "Partially Proven" status mean for a loop invariant?
Does "Unknown" mean the following?
> Under the hypothesis that the other invariants are inductive (established and preserved), this invariant could not be proven to be inductive (failed establishment or preservation, or both)
For example, consider the following program:
```c
extern int unknown_int(void);
int main() {
int i, m, n;
int j, k;
n = unknown_int();
i = unknown_int();
m = unknown_int();
if (!( n == i / 32 )) return 0;
/*@
loop invariant i1: 0 <= j <= i / 8;
loop invariant i2: 0 <= j <= m;
loop invariant i3: j * 4 <= i;
loop invariant i4: j <= n * 8;
*/
for (j = 0; (j < i / 8) && (j < m); j++) {
//@ assert( j/4 < n);
}
return 0;
}
```
Invoking Frama-C with the following command, results in a CSV file with the status for each property:
```
frama-c -wp -wp-verbose 100 -wp-debug 100 -wp-timeout 3 -wp-prover=z3,alt-ergo,cvc4 temp.c -then -report -report-csv frama_c_dump_.csv
```
The CSV output file contains the following:
```
directory file line function property kind status property
. temp.c 1 unknown_int assigns clause Unknown assigns \nothing;
. temp.c 1 unknown_int from clause Unknown assigns \result \from \nothing;
. temp.c 13 main loop invariant Unknown 0 ≤ j ≤ i / 8
. temp.c 14 main loop invariant Unknown 0 ≤ j ≤ m
. temp.c 15 main loop invariant Unknown j * 4 ≤ i
. temp.c 16 main loop invariant Partially proven j ≤ n * 8
. temp.c 19 main user assertion Unknown j / 4 < n
```
What does the status "Unknown" assigned to multiple invariants i1, i2, and i3 mean?
More specifically, **what does it mean to have multiple "Unknown" loop invariants?** Is there a formal description of the possible status values and their meanings? If so, could you please point me in that direction?Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2674Consistency of uses of \from clauses2023-10-25T16:54:47ZNikolai KosmatovConsistency of uses of \from clausesThis issue describes a certain inconsistency in usages of the `\from` clauses in different plugins.
WP relies on `\from` clauses to facilitate pointer analysis for correct memory model assumptions.
This feature is very helpful.
MetAcsl...This issue describes a certain inconsistency in usages of the `\from` clauses in different plugins.
WP relies on `\from` clauses to facilitate pointer analysis for correct memory model assumptions.
This feature is very helpful.
MetAcsl relies on (`assigns` and in particular) `\from` clauses to instantiate metaproperties
for callees based on their contracts. This can be used for undefined functions or in some cases
for defined functions for better performances of the global proof. This feature is also very helpful.
There is a certain inconsistency of both usages on the same code: only a base address is
necessary for the first usage, while a complete list of dependencies is expected in the second case.
It would be desirable to avoid the usage of the same clause in two different ways.
One suggestion can be to use another clause like `\from_ptr` or `\from_base` for the first case.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2673[WP] non-matching of strategies with logical operators2024-03-04T10:14:59ZNikolai Kosmatov[WP] non-matching of strategies with logical operators### Steps to reproduce the issue
On the attached example
[logical_pattern.c](/uploads/0bb48f222b06fb2a470e76d756be35f0/logical_pattern.c)
running the following command
`frama-c-gui logical_pattern.c -wp -wp-rte -wp-prover=alt-ergo,...### Steps to reproduce the issue
On the attached example
[logical_pattern.c](/uploads/0bb48f222b06fb2a470e76d756be35f0/logical_pattern.c)
running the following command
`frama-c-gui logical_pattern.c -wp -wp-rte -wp-prover=alt-ergo,tip -wp-timeout 1 -wp-prop post`
to apply a strategy with Split does not seem to accept the pattern and to match the precondition with logical operations `&&` and `||`
```
strategy FastAltErgo: \prover("alt-ergo", 1); // run Alt-Ergo for 1 sec.
strategy EagerAltErgo: \prover("alt-ergo",10); // run Alt-Ergo for 10 sec.
strategy SplitProver:
FastAltErgo,
\tactic("Wp.split"
,\pattern( ((A && B) || (C && D)) )
,\children(EagerAltErgo)
),
EagerAltErgo;
proof SplitProver: post;
```
### Expected behaviour
According to documentation, ACSL logical operations are recognized and after a successful matching, a script is created with two subgoals (to be completed).
### Actual behaviour
Syntax error is reported (Invalid pattern. Ignoring global annotation).
### Contextual information
- Frama-C installation mode: opam from GIT pub
- Frama-C version: first version of the strategy mechanism (https://git.frama-c.com/pub/frama-c.git#3396bd), also the recent update on master on pub (by the branch fix/wp/strategies)
- Plug-in used: WP with Why3 1.6.0 and Alt-Ergo 2.4.3
- OS name: Ubuntu
- OS version: 22.04Loïc CorrensonLoïc Correnson