frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2022-05-30T08:20:54Zhttps://git.frama-c.com/pub/frama-c/-/issues/2594Unsafe uses of Obj in Unmarshal2022-05-30T08:20:54ZVincent LavironUnsafe uses of Obj in UnmarshalA few pieces of code in the `Unmarshal` module are too obviously unsafe for the Flambda 2 compiler's taste, and results in the compiler deliberately inserting a segfault.
The `Sys.opaque_identity` function can be used to tell the compile...A few pieces of code in the `Unmarshal` module are too obviously unsafe for the Flambda 2 compiler's taste, and results in the compiler deliberately inserting a segfault.
The `Sys.opaque_identity` function can be used to tell the compiler not to make any assumptions on the underlying value, and is available since OCaml 4.03, so I'd like to see it used here to allow testing Frama C with Flambda 2.
The three places that are affected are:
- The code for initialising `arch_bigendian`. This can be fixed by inserting a call to `Sys.opaque_identity`.
- The code for initialising `arch_float_endianness`. This can be fixed by inserting a call to `Sys.opaque_identity`.
- The code for computing the `null` value. I assume that the code was intended to compute a null pointer, but it was reading the wrong field anyway so this was instead a pointer to a C-allocated struct (which, it seems, works as well). I'd like to replace it with `Obj.repr (Sys.opaque_identity (ref 0))`, which should work too (it gives you a unique static pointer) and has the advantage of not manipulating naked pointers.
I could propose a patch if you'd like (or even open a merge request, if your GitLab instance accepts merge requests from external contributors)25 (Manganese)François BobotFrançois Bobothttps://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/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/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/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/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/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 Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2671[WP] non-termination of strategies with Split2023-10-25T06:56:31ZNikolai Kosmatov[WP] non-termination of strategies with Split### Steps to reproduce the issue
On the attached example
[code.c](/uploads/ce33987e5d62de016eecf185bf9c0c4c/code.c)
running the following command
`frama-c code.c -wp -wp-rte -wp-prover=tip -wp-timeout 1 -wp-prop vhm_preserved`
t...### Steps to reproduce the issue
On the attached example
[code.c](/uploads/ce33987e5d62de016eecf185bf9c0c4c/code.c)
running the following command
`frama-c code.c -wp -wp-rte -wp-prover=tip -wp-timeout 1 -wp-prop vhm_preserved`
to apply a strategy with Split does not seem to terminate:
```
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 SplitThenProver:
\tactic("Wp.split"
,\goal(_)
,\children(SplitThenProver)
),
EagerAltErgo;
strategy UnfoldVhmThenSplitThenProver:
\tactic("Wp.unfold",
\pattern((P_valid_heap_model((..)))),
\children(UnfoldVhmThenSplitThenProver) ),
SplitThenProver;
proof UnfoldVhmThenSplitThenProver: vhm_preserved;
```
### Expected behaviour
Termination.
### Actual behaviour
Strategy application of Split tactic with WP does not terminate. Is it normal in this case?
### 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 Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2670[WP] non-termination of strategies with Filter2023-10-25T06:56:33ZNikolai Kosmatov[WP] non-termination of strategies with Filter### Steps to reproduce the issue
On the attached example
[code.c](/uploads/9a0f5a75df68310da6dce43ee7cc7568/code.c)
running the following command
`frama-c code.c -wp -wp-rte -wp-prover=tip -wp-timeout 1 -wp-prop vhm_preserved`
t...### Steps to reproduce the issue
On the attached example
[code.c](/uploads/9a0f5a75df68310da6dce43ee7cc7568/code.c)
running the following command
`frama-c code.c -wp -wp-rte -wp-prover=tip -wp-timeout 1 -wp-prop vhm_preserved`
to apply a strategy with Filter does not seem to terminate:
```
strategy FastAltErgo: \prover("alt-ergo", 1); // run Alt-Ergo for 1 sec.
strategy EagerAltErgo: \prover("alt-ergo",10); // run Alt-Ergo for 10 sec.
//Loops for vhm_preserved
strategy FilterProver:
FastAltErgo,
\tactic("Wp.filter"
,\goal(_)
,\children(EagerAltErgo)
),
EagerAltErgo;
proof FilterProver: vhm_preserved;
```
### Expected behaviour
Termination.
### Actual behaviour
Strategy application of Filter tactic with WP does not terminate.
### 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.04
### Additional information (optional)
It seems that similar non-termination was observed with Split but I do not have an example by hand.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2669Plugin containing ppx_compare library crashes at load2023-10-10T09:36:11Zpepega007xdPlugin containing ppx_compare library crashes at load### Steps to reproduce the issue
Create an empty Frama-C plugin with the `ppx_compare` library dependency, and try to run Frama-C with this plugin.
Project structure:
```
hello/
├── dune
├── dune-project
└── hello.ml
```
dune-project:...### Steps to reproduce the issue
Create an empty Frama-C plugin with the `ppx_compare` library dependency, and try to run Frama-C with this plugin.
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)
(flags -open Frama_c_kernel :standard)
(libraries frama-c.kernel ppx_compare)
)
(plugin
(optional)
(name hello)
(libraries frama-c-hello.core)
(site (frama-c plugins))
)
```
hello.ml:
```
let run () = print_endline "Hello"
let () = Db.Main.extend run
```
Execute `dune build` and `dune exec -- frama-c`.
### Expected behaviour
Plugin prints `Hello` to the console.
### Actual behaviour
Frama-C crashes with the following backtrace:
```
[kernel] Current source was: :0
The full backtrace is:
Raised at Dynlink_common.Make.load in file "otherlibs/dynlink/dynlink_common.ml", line 350, characters 23-73
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Dune_site_plugins__Plugins.load_gen in file "otherlibs/dune-site/src/plugins/plugins.ml", line 255, characters 4-36
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Dune_site_plugins__Plugins.load_gen in file "otherlibs/dune-site/src/plugins/plugins.ml", line 255, characters 4-36
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Dune_site_plugins__Plugins.load_gen in file "otherlibs/dune-site/src/plugins/plugins.ml", line 255, characters 4-36
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Dune_site_plugins__Plugins.load_gen in file "otherlibs/dune-site/src/plugins/plugins.ml", line 255, characters 4-36
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Dune_site_plugins__Plugins.load_gen in file "otherlibs/dune-site/src/plugins/plugins.ml", line 255, characters 4-36
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Frama_c_kernel__Kernel.bootstrap_loader in file "src/kernel_services/plugin_entry_points/kernel.ml", line 933, characters 35-62
Called from Frama_c_kernel__Cmdline.parse_and_boot in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 894, characters 2-22
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 (Dynlink.Error (Dynlink.Cannot_open_dll "Dynlink.Error (Dynlink.Cannot_open_dll \"Failure(\\\"/home/tb/.opam/default/lib/ppxlib/astlib/astlib.cmxs: undefined symbol: camlConfig__32\\\")\")")).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 27.1 (Cobalt).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
```
### Contextual information
- Frama-C installation mode: using Opam (ppx_compare is also installed using Opam)
- Frama-C version: `27.1 (Cobalt)`
- Plug-in used: Hello World plugin
- OS name: `Fedora Linux 38 (Workstation Edition)`
### Additional information (optional)
When I put the ppx_compare library also inside the `(plugin (libraries ...))` section in `dune` file, the same thing happens.Allan BlanchardAllan Blanchardhttps://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/2667The Windows (WSL) installation guide is out-of-date2023-09-13T15:15:27ZKaroliine HolterThe Windows (WSL) installation guide is out-of-dateI was trying to install frama-c on WSL by [the guide on the website](https://frama-c.com/html/get-frama-c.html#), and got stuck with the `opam install -y depext` command with the following error:
```
[ERROR] depext unmet availability con...I was trying to install frama-c on WSL by [the guide on the website](https://frama-c.com/html/get-frama-c.html#), and got stuck with the `opam install -y depext` command with the following error:
```
[ERROR] depext unmet availability conditions, e.g. 'opam-version >= "2.0.0~beta5" & opam-version < "2.1"'
```
It took me a while to figure out that in fact [`opam-depext` has been integrated into opam since 2.1](https://github.com/ocaml-opam/opam-depext) and it is sufficient to just run `opam install frama-c` as described in the Linux installation guide.
Therefore I suggest that the WSL installation guides on the [frama-c webpage](https://frama-c.com/html/get-frama-c.html#) and [repository](https://git.frama-c.com/pub/frama-c/blob/master/INSTALL.md) be updated to prevent others, who are using WSL, to be confused.https://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/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 Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2662Stack overflow during e-acsl translation of runtime error assertions on coreu...2024-02-09T14:44:32ZRaphaël MonatStack overflow during e-acsl translation of runtime error assertions on coreutils program<!--
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]…
-->
I'm trying to leverage frama-c rte and e-acsl plugins to encode all runtime errors through assertions, following ["A Lesson on Runtime Assertion Checking with Frama-C"](https://julien-signoles.fr/publis/2013_rv.pdf). I might have gotten a bit ambitious and tried to launch it on some preprocessed coreutils file.
### Steps to reproduce the issue
Attached is [chcon_comb2.c](/uploads/da99c1b868a8909c7f16a5ee69de1119/chcon_comb2.c).
```
$ frama-c -rte chcon_comb2.c -machdep x86_64 -then -e-acsl -then-on e-ascl -print -ocode chcon_comb2_rte.c
[...]
Ignoring annotation.
[kernel] Current source was: chcon_comb2.c:48883
The full backtrace is:
Raised at Frama_c_kernel__Project.on in file "src/libraries/project/project.ml", line 365, characters 59-66
Called from E_ACSL__Main.generate_code.(fun) in file "src/plugins/e-acsl/src/main.ml", line 46, characters 7-1023
Called from Frama_c_kernel__State_builder.Hashtbl.memo in file "src/libraries/project/state_builder.ml", line 569, characters 17-22
Called from E_ACSL__Main.main in file "src/plugins/e-acsl/src/main.ml", line 162, characters 11-56
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.aux in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 865, characters 30-76
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).
```
### Expected behaviour
I was wondering if there was an easy fix in the source code to avoid this Stack overflow?
As a side note, the rte package seems to not support "Builtins for long double type". For now I just changed the types.
### Contextual information
- Frama-C installation mode: opam
- Frama-C version: 27.0 (Cobalt)
- Plug-in used: RTE & E-ACSL
- OS name: Ubuntu
- OS version: 22.04.2Julien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/2660[Eva] The plugin doesn't terminate on this program2023-05-17T08:21:52ZCharles Babu M[Eva] The plugin doesn't terminate on this program### Steps to reproduce the issue
I ran ```dune exec -- frama-c loop_nla.c -eva```
```
/* Compute the floor of the square root, by Dijkstra */
extern void abort(void);
extern void __assert_fail(const char *, const char *, unsigned int...### Steps to reproduce the issue
I ran ```dune exec -- frama-c loop_nla.c -eva```
```
/* Compute the floor of the square root, by Dijkstra */
extern void abort(void);
extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
void reach_error() { __assert_fail("0", "dijkstra-u.c", 5, "reach_error"); }
extern unsigned int __VERIFIER_nondet_uint(void);
extern void abort(void);
void assume_abort_if_not(int cond) {
if(!(cond)) { abort();}
return;
}
void __VERIFIER_assert(int cond) {
if (!(cond)) {
ERROR:
{reach_error();}
}
return;
}
int counter = 0;
int main() {
unsigned int n, p, q, r, h;
n = __VERIFIER_nondet_uint();
assume_abort_if_not(n < 4294967295 / 4); // Avoid non-terminating loop
p = 0;
q = 1;
r = n;
h = 0;
while (counter++<1) {
if (!(q <= n))
break;
q = 4 * q;
}
//q == 4^n
while (counter++<1) {
__VERIFIER_assert(r < 2 * p + q);
__VERIFIER_assert(p*p + r*q - n*q == 0);
__VERIFIER_assert(h * h * h - 12 * h * n * q + 16 * n * p * q - h * q * q - 4 * p * q * q + 12 * h * q * r - 16 * p * q * r == 0);
__VERIFIER_assert(h * h * n - 4 * h * n * p + 4 * (n * n) * q - n * q * q - h * h * r + 4 * h * p * r - 8 * n * q * r + q * q * r + 4 * q * r * r == 0);
__VERIFIER_assert(h * h * p - 4 * h * n * q + 4 * n * p * q - p * q * q + 4 * h * q * r - 4 * p * q * r == 0);
__VERIFIER_assert(p * p - n * q + q * r == 0);
if (!(q != 1))
break;
q = q / 4;
h = p + q;
p = p / 2;
if (r >= h) {
p = p + q;
r = r - h;
}
}
__VERIFIER_assert(h*h*h - 12*h*n + 16*n*p + 12*h*r - 16*p*r - h - 4*p == 0);
__VERIFIER_assert(p*p - n + r == 0);
__VERIFIER_assert(h*h*p - 4*h*n + 4*n*p + 4*h*r - 4*p*r - p == 0);
return 0;
}
```
### Expected behaviour
It should terminate
### Actual behaviour
It does not terminate.
But if I change the ```assume_abort_if_not``` function by replacing the condition as below, it terminates
```
void assume_abort_if_not(int cond) {
if((cond)==0) { abort();}
return;
}
```
### Contextual information
- Frama-C installation mode: from source
- Frama-C version: 25.0~beta (Manganese)
- Plug-in used: EVA
- OS name: Ubuntu
- OS version: 20.04.6 LTSAndre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2659[WP] Unexpected error (Wp__NormAtLabels.LabelError(_))2023-05-10T08:25:17ZYurii Rashkovskii[WP] Unexpected error (Wp__NormAtLabels.LabelError(_))<!--
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.
-->
```
git clone https://github.com/yrashk/clam
cd clam && ./test wp
```
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
Test to complete. It was last observed to work with 22.0
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
```
[kernel] Parsing clam.h (with preprocessing)
[rte:annot] annotating function clam_match_alpha_char
[rte:annot] annotating function clam_match_alphanumeric_char
[rte:annot] annotating function clam_match_anychar
[rte:annot] annotating function clam_match_at_least_n_chars
[rte:annot] annotating function clam_match_char
[rte:annot] annotating function clam_match_chars
[rte:annot] annotating function clam_match_chars_to_end
[rte:annot] annotating function clam_match_end
[rte:annot] annotating function clam_match_lowercase_char
[rte:annot] annotating function clam_match_numeric10_char
[rte:annot] annotating function clam_match_numeric16_char
[rte:annot] annotating function clam_match_posix_flags
[rte:annot] annotating function clam_match_posix_long_option
[rte:annot] annotating function clam_match_posix_option
[rte:annot] annotating function clam_match_posix_terminate_options
[rte:annot] annotating function clam_match_signed_integer10
[rte:annot] annotating function clam_match_unsigned_integer10
[rte:annot] annotating function clam_match_uppercase_char
[rte:annot] annotating function clam_match_windows_long_switch
[rte:annot] annotating function clam_match_windows_switch
[kernel] Current source was: clam.h:513
The full backtrace is:
Raised at Wp__NormAtLabels.labels_fct_pre in file "src/plugins/wp/normAtLabels.ml", line 136, characters 9-29
Called from Wp__NormAtLabels.norm_at#vterm.post.normalize in file "src/plugins/wp/normAtLabels.ml", line 82, characters 30-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
Called from Wp__NormAtLabels.norm_at#vterm.post in file "src/plugins/wp/normAtLabels.ml", line 83, characters 29-54
Called from Frama_c_kernel__Cil.visitCilTerm in file "src/kernel_services/ast_queries/cil.ml", line 1417, characters 12-63
Called from Frama_c_kernel__Cil.childrenPredicateNode.vTerm in file "src/kernel_services/ast_queries/cil.ml" (inlined), line 1799, characters 16-34
Called from Frama_c_kernel__Cil.childrenPredicateNode in file "src/kernel_services/ast_queries/cil.ml", line 1810, characters 14-22
Called from Frama_c_kernel__Cil.doVisit in file "src/kernel_services/ast_queries/cil.ml", line 1304, characters 19-39
Called from Frama_c_kernel__Cil.childrenPredicate in file "src/kernel_services/ast_queries/cil.ml", line 1793, characters 16-56
Called from Frama_c_kernel__Cil.doVisit in file "src/kernel_services/ast_queries/cil.ml", line 1304, characters 19-39
Called from Frama_c_kernel__Cil.childrenPredicateNode.vPred in file "src/kernel_services/ast_queries/cil.ml" (inlined), line 1797, characters 16-39
Called from Frama_c_kernel__Cil.childrenPredicateNode in file "src/kernel_services/ast_queries/cil.ml", line 1817, characters 14-22
Called from Frama_c_kernel__Cil.doVisit in file "src/kernel_services/ast_queries/cil.ml", line 1304, characters 19-39
Called from Frama_c_kernel__Cil.childrenPredicate in file "src/kernel_services/ast_queries/cil.ml", line 1793, characters 16-56
Called from Frama_c_kernel__Cil.doVisit in file "src/kernel_services/ast_queries/cil.ml", line 1304, characters 19-39
Called from Frama_c_kernel__Cil.childrenPredicateNode.vPred in file "src/kernel_services/ast_queries/cil.ml" (inlined), line 1797, characters 16-39
Called from Frama_c_kernel__Cil.childrenPredicateNode in file "src/kernel_services/ast_queries/cil.ml", line 1834, characters 14-22
Called from Frama_c_kernel__Cil.doVisit in file "src/kernel_services/ast_queries/cil.ml", line 1304, characters 19-39
Called from Frama_c_kernel__Cil.childrenPredicate in file "src/kernel_services/ast_queries/cil.ml", line 1793, characters 16-56
Called from Frama_c_kernel__Cil.doVisit in file "src/kernel_services/ast_queries/cil.ml", line 1304, characters 19-39
Called from Frama_c_kernel__Visitor.visitFramacPredicate in file "src/kernel_services/visitors/visitor.ml", line 978, characters 11-48
Called from Wp__CfgAnnot.normalize_pre in file "src/plugins/wp/cfgAnnot.ml", line 80, characters 14-60
Called from Wp__CfgAnnot.CallContract.compile.add in file "src/plugins/wp/cfgAnnot.ml", line 338, characters 30-33
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Wp__CfgAnnot.CallContract.compile.(fun) in file "src/plugins/wp/cfgAnnot.ml", line 348, characters 12-59
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Wp__CfgAnnot.CallContract.compile in file "src/plugins/wp/cfgAnnot.ml", line 341, characters 8-671
Called from Wp__WpContext.Static.memoize in file "src/plugins/wp/wpContext.ml", line 447, characters 14-17
Called from Wp__WpContext.StaticGenerator.get in file "src/plugins/wp/wpContext.ml" (inlined), line 510, characters 12-31
Called from Wp__CfgAnnot.get_call_contract in file "src/plugins/wp/cfgAnnot.ml", line 372, characters 11-30
Called from Wp__CfgCalculus.Make.call in file "src/plugins/wp/cfgCalculus.ml", line 365, characters 12-52
Called from Wp__CfgCalculus.Make.stmt in file "src/plugins/wp/cfgCalculus.ml", line 233, characters 8-23
Re-raised at Wp__CfgCalculus.Make.stmt in file "src/plugins/wp/cfgCalculus.ml", line 237, characters 30-39
Called from Wp__CfgCalculus.Make.wp in file "src/plugins/wp/cfgCalculus.ml", line 214, characters 20-32
Called from Wp__CfgCalculus.Make.transition in file "src/plugins/wp/cfgCalculus.ml", line 305, characters 12-22
Called from Wp__CfgCalculus.Make.wp in file "src/plugins/wp/cfgCalculus.ml", line 213, characters 18-34
Called from Wp__CfgCalculus.Make.compute in file "src/plugins/wp/cfgCalculus.ml", line 544, characters 6-61
Called from Wp__CfgGenerator.Make.compute.(fun) in file "src/plugins/wp/cfgGenerator.ml", line 235, characters 30-53
Called from Wp__WpContext.on_context in file "src/plugins/wp/wpContext.ml", line 139, characters 17-20
Re-raised at Wp__WpContext.on_context in file "src/plugins/wp/wpContext.ml", line 146, characters 4-13
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Stdlib__Map.Make.iter in file "map.ml", line 297, characters 20-25
Called from Stdlib__Map.Make.iter in file "map.ml", line 297, characters 10-18
Called from Wp__CfgGenerator.Make.compute in file "src/plugins/wp/cfgGenerator.ml", line 219, characters 6-1023
Called from Wp__Register.cmdline_run in file "src/plugins/wp/register.ml", line 750, characters 20-61
Called from Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 834, characters 14-17
Re-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 (Wp__NormAtLabels.LabelError(_)).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 26.1 (Iron).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
```
### Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: 26.1
- Plug-in used: WP
- OS name: macOS
- OS version: 13.3.1
### 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.
-->Loïc CorrensonLoïc Correnson