frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2024-03-04T10:14:59Zhttps://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/2672Handling of wide string literals2023-11-08T18:21:33ZMarvin HäuserHandling of wide string literals### Steps to reproduce the issue
Evaluate `sizeof(L"AA")` during preprocessing, possibly as part of a `_Static_assert`. Take for example the following code snippet:
```
_Static_assert(sizeof(L"AA") == 12, "Incorrect sizeof behaviour");...### Steps to reproduce the issue
Evaluate `sizeof(L"AA")` during preprocessing, possibly as part of a `_Static_assert`. Take for example the following code snippet:
```
_Static_assert(sizeof(L"AA") == 12, "Incorrect sizeof behaviour");
int main(void){}
```
This compiles fine with GCC, but fails preprocessing with ``frama-c -wp``. With varying string lengths, the assertion succeeds Frama-C preprocessing when replacing 12 with the pointer size, but fails to compile with GCC.
### Expected behaviour
The expression evaluates to `sizeof(wchar_t) * 3`, typically 12.
### Actual behaviour
The expression evaluates to `sizeof(wchar_t *)`, typically 4 or 8.
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 27.1 (Cobalt)
- Plug-in used: WP
- OS name: macOS
- OS version: 14.0
### Additional information (optional)
A quick search of the source code yields several special handling of string literals, e.g. the definition of `SizeOfStr()`. It appears most to all of the related code is specific to `char` string literals with no support for `wchar_t` string literals (both as in they do not seem to get special handling, and there is no support in the existing literal code to vary the character size). As I am new to the codebase, please feel free to confirm or correct my observations. Thank you!Virgile PrevostoVirgile Prevostohttps://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/2665Crash when attempting to use frama-c installed via opam on ubuntu.2023-08-31T06:48:24ZchristinaburgeCrash when attempting to use frama-c installed via opam on ubuntu.Here is the error message in full.
> `[kernel] Current source was: :0
The full backtrace is:
Raised at Dune_site_plugins__Plugins.load_plugin in file "otherlibs/dune-site/src/plugins/plugins.ml", line 267, characters 12-74
Called...Here is the error message in full.
> `[kernel] Current source was: :0
The full backtrace is:
Raised at Dune_site_plugins__Plugins.load_plugin in file "otherlibs/dune-site/src/plugins/plugins.ml", line 267, characters 12-74
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 (The plugin "Frama_Clang.cmi" can't be found in the search paths "/home/chrbur02/.opam/default/lib/frama-c/plugins".).
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`https://git.frama-c.com/pub/frama-c/-/issues/2664Tuples are not supported2023-08-08T06:13:21ZAdharsh KamathTuples are not supported## Error while using types and predicates with the WP plugin
### Steps to reproduce the issue
Copy the code snippet from Example 2.35 in Section 2.5.3 in the latest ACSL manual (https://frama-c.com/download/frama-c-acsl-implementation.p...## Error while using types and predicates with the WP plugin
### Steps to reproduce the issue
Copy the code snippet from Example 2.35 in Section 2.5.3 in the latest ACSL manual (https://frama-c.com/download/frama-c-acsl-implementation.pdf) and run Frama-C on this code file, with the WP plugin.
### Expected behaviour
Frama-C should not throw any errors and verify the given method using the predicate.
### Actual behaviour
Multiple errors are reported as follows in the Kernel logs: <br>
[kernel:annot-error] /code.c:4: Warning: unexpected token '('<br>
[kernel:annot-error] /code.c:7: Warning: unexpected token '('<br>
[kernel:annot-error] /code.c:16: Warning: unexpected token ','<br>
which corresponds to the lines:<br>
line 4: //@ type intpair = (integer,integer);<br>
line 7: @ \let (x1,y1) = p1 ;<br>
line 16: @ loop variant (x, y) for lexico;<br>
### Contextual information
- Frama-C installation mode: opam
- Frama-C version: 27.1 (Cobalt)
- Plug-in used: WP
- OS name: Ubuntu
- OS version: 20.04
### Additional comments
I'm not sure what I'm missing here? Is there some flag I'm supposed to switch on, while using these features? Or use a different plugin?
**Is there any other way of specifying lexicographically ordered terms as a variant in Frama-C?**Allan BlanchardAllan Blanchardhttps://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/2661frama-c-gui 27.0 segmentation fault in MacOS Ventura 13.42023-06-21T09:50:07ZDavid Sananframa-c-gui 27.0 segmentation fault in MacOS Ventura 13.4I have installed the latest Frama-C version (27.0) in MacOS Ventura 13.4 on M1 and M2 Macbooks. The installation process is smooth, including Ivette installation.
Once everything is installed when trying to run the GUI I get the followi...I have installed the latest Frama-C version (27.0) in MacOS Ventura 13.4 on M1 and M2 Macbooks. The installation process is smooth, including Ivette installation.
Once everything is installed when trying to run the GUI I get the following
```
[gui] Warning: creating config directory `.config/frama-c/gui'
(frama-c-gui:13363): Gtk-WARNING **: 12:57:42.276: Drawing a gadget with negative dimensions. Did you forget to allocate a size? (node tab owner GtkNotebook)
(frama-c-gui:13363): Gtk-WARNING **: 12:57:42.276: Drawing a gadget with negative dimensions. Did you forget to allocate a size? (node arrow owner GtkNotebook)
(frama-c-gui:13363): Gtk-WARNING **: 12:57:42.277: Drawing a gadget with negative dimensions. Did you forget to allocate a size? (node arrow owner GtkNotebook)
[1] 13363 segmentation fault frama-c-gui
```
I get this behaviour on both computers.
Is there any workaround for this? I tried copying the GUI config file from Linux without any success.
It works well in Linux, though. And the new interface is very neat thank you!
Thanks and best regards,
David.Andre MaronezeAndre Maronezehttps://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 Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2658[WP] Trivial goals of two integer pointer cannot be verified2023-04-20T07:39:42ZJim Chen[WP] Trivial goals of two integer pointer cannot be verified<!--
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.
-->
In this function `fix_target_val`, the goal is to prove that in certain case, pointers target & offset are modified correctly.
I found that `ensures mode == 0 && val < 4 ==> *offset == 1;` can't be verified but `ensures mode == 0 && val < 4 ==> *target == 0;` cannot.
**Both ensures clauses are expected to be valid.**
```console
[kernel] Parsing test2.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 12 goals scheduled
[wp] [Failed] Goal typed_cast_fix_target_val_ensures_2
Coq 8.15.2: Unknown (Qed:8ms)
CVC4 1.7: Unknown (Qed:8ms) (cached)
[wp] [Cache] found:1
[wp] Proved goals: 11 / 12
Qed: 11 (0.93ms-3ms-6ms)
CVC4 1.7: 0 (unknown: 1) (cached: 1)
Coq 8.15.2: 0 (unknown: 1)
```
```cpp
#include <stdio.h>
typedef unsigned char U8;
typedef unsigned long U32;
/*@
requires \valid(target) && \valid(offset);
requires 0 <= val < 1024;
requires 0 <= mode <= 2;
assigns *offset, *target;
ensures mode == 0 && val < 4 ==> *target == 0;
ensures mode == 0 && val < 4 ==> *offset == 1;
@*/
void fix_target_val(U32 val, U8 *offset, U8 *target, U8 mode)
{
if (mode == 0)
{
if (val < 4)
{
*offset = 1;
*target = 0;
}
}
}
```
In another case, I switch the order of the assignment of offset & target.
Here's what I got.
```console
[kernel] Parsing test2.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 12 goals scheduled
[wp] [Failed] Goal typed_cast_fix_target_val_ensures
Coq 8.15.2: Unknown (Qed:8ms)
CVC4 1.7: Unknown (Qed:8ms) (cached)
[wp] [Cache] found:1
[wp] Proved goals: 11 / 12
Qed: 11 (0.93ms-2ms-6ms)
CVC4 1.7: 0 (unknown: 1) (cached: 1)
Coq 8.15.2: 0 (unknown: 1)
```
```cpp
/*@
requires \valid(target) && \valid(offset);
requires 0 <= val < 1024;
requires 0 <= mode <= 2;
assigns *offset, *target;
ensures mode == 0 && val < 4 ==> *target == 0;
ensures mode == 0 && val < 4 ==> *offset == 1;
@*/
void fix_target_val(U32 val, U8 *offset, U8 *target, U8 mode)
{
if (mode == 0)
{
if (val < 4)
{
*target = 0;
*offset = 1;
}
}
}
```
The commend I use:
```bash
frama-c -wp -wp-no-rte \
-wp-prover cvc4,coq \
-wp-model 'Typed+Cast' \
-c11 \
-main fix_target_val \
-lib-entry ./test.c \
```
### Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *25.0 (Manganese)* (as reported by `frama-c -version`)
- Plug-in used: *WP*
- OS name: *Ubuntu*
- OS version: *20.04.6 LTS*https://git.frama-c.com/pub/frama-c/-/issues/2657frama-c-gui frozen and why3 not found2023-04-13T14:44:13ZRongframa-c-gui frozen and why3 not found### Problem Description ###
When running `opam install alt-ergo`, my terminal shows:
```
Package alt-ergo is already installed (current version is 2.4.2).
```
However, when running `frama-c-gui -wp -rte -main.c`, the terminal shows:
...### Problem Description ###
When running `opam install alt-ergo`, my terminal shows:
```
Package alt-ergo is already installed (current version is 2.4.2).
```
However, when running `frama-c-gui -wp -rte -main.c`, the terminal shows:
```
(frama-c-gui:4023): GLib-CRITICAL **: 09:36:25.664: Source ID 8 was not found when attempting to remove it.
```
The GUI is opened but frozen. No clicking is responded and the console shows `User Error: Prover 'alt-ergo' not found in why3.conf.`
### Steps to reproduce the issue
frama-c-gui -wp -rte -main.c
### Expected behaviour
open the window of frama-c-gui and run normally
### Actual behaviour
The GUI is opened but frozen. No clicking is responded and the console shows `User Error: Prover 'alt-ergo' not found in why3.conf.`
### Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *frama-c.26.1*
- Plug-in used: *Plug-in used*
- OS name: *Ubuntu*
- OS version: *22.04.2 LTS*
### Additional information (optional)
After running "opam upgrade", the following information appears:
```
Everything as up-to-date as possible (run with --verbose to show unavailable upgrades).
The following packages are not being upgraded because the new versions conflict with other installed packages:
- ocaml-config.3
- ocplib-simplex.0.5
∗ alt-ergo-lib.2.4.2 is installed and requires ocplib-simplex (>= 0.4 & < 0.5)
- why3.1.6.0
∗ frama-c.26.1 is installed and requires why3 (>= 1.5.1 & < 1.6~)
However, you may "opam upgrade" these packages explicitly, which will ask permission to downgrade or uninstall the conflicting packages.
Nothing to do.
# Run eval $(opam env) to update the current shell environment
```https://git.frama-c.com/pub/frama-c/-/issues/2656Unbound value Why3.Whyconf.load_driver2023-04-07T18:21:10ZpiniUnbound value Why3.Whyconf.load_driverHi,
I'm trying to package `frama-c 26.1` for the gentoo linux distribution.
Build must be done from source *in a sandboxed directory* and ideally should include system-wide dependencies, so I'm not using opam for fetching dependencies...Hi,
I'm trying to package `frama-c 26.1` for the gentoo linux distribution.
Build must be done from source *in a sandboxed directory* and ideally should include system-wide dependencies, so I'm not using opam for fetching dependencies (which relies heavily on a home-directory configuration).
I managed to fix all errors so far but the following one:
```
File "src/plugins/wp/ProverWhy3.ml", line 1129, characters 12-36:
1129 | let drv = Why3.Whyconf.load_driver (Why3.Whyconf.get_main config)
^^^^^^^^^^^^^^^^^^^^^^^^
Error: Unbound value Why3.Whyconf.load_driver
```
The installed version of Why3 is 1.6.0 with `gtk ocamlopt zarith zip` features enabled and `coq doc emacs re sexp stackify` disabled (i.e. the standard selection for this package).
The meaning of these features is documented as follows:
- coq - Add sci-mathematics/coq support
- doc - Add extra documentation (API, Javadoc, etc). It is recommended to enable per package instead of globally
- emacs - Add support for GNU Emacs
- gtk - Build the IDE x11-libs/gtk+
- ocamlopt - Enable ocamlopt support (ocaml native code compiler) -- Produces faster programs (Warning: you have to disable/enable it at a global scale)
- re - Use Re (dev-ml/re) instead of Str for regular expressions
- sexp - Add support for outputting S-expressions with dev-ml/ppx_sexp_conv
- stackify - Enable structure reconstruction algorithm for MLCFG
- zarith - Use Zarith (dev-ml/zarith) instead of Nums (dev-ml/num) for computations
- zip - Enable compression of session files
Here is the ebuild file I came up with: [frama-c-26.1.ebuild](/uploads/0672aa337cb772870b4965879e5759d7/frama-c-26.1.ebuild)
Any tip on how to fix this last compilation error would be great.
Thanks a lot for your work and time.
--
Pierre-Nicolashttps://git.frama-c.com/pub/frama-c/-/issues/2655Suggested corrections/improvements to frama-c installation on Mac2023-04-07T08:19:13ZDavid CokSuggested corrections/improvements to frama-c installation on MacBased on installing frama-c per the instructions for Mac on frama-c.com
on MacOS 12.6.3 (a clean Parallels VM).
- Suggest a step 2.5) run `opam init`
- Suggest a step 6) run `why3 config detect`
But note that when I do, I receive the r...Based on installing frama-c per the instructions for Mac on frama-c.com
on MacOS 12.6.3 (a clean Parallels VM).
- Suggest a step 2.5) run `opam init`
- Suggest a step 6) run `why3 config detect`
But note that when I do, I receive the report:
Prover Alt-Ergo version 2.4.2 is not recognized
Known versions for this prover: 2.4.0, 2.4.1
1 provers added (including 1 prover(s) with na unrecognized version)
This is unsettling. Though a test program seems to indicate that 2.4.2 is used without trouble.https://git.frama-c.com/pub/frama-c/-/issues/2654ACSL v18 release is not present in the ACSL github releases page2023-03-31T16:10:59ZDavid CokACSL v18 release is not present in the ACSL github releases pageThe frama-c download page for ACSL: https://frama-c.com/html/acsl.html
lists a V.18, but this version is not present on the ACSL github site: https://github.com/acsl-language/acsl/releases
where v17 is marked as "latest"
I do see that v...The frama-c download page for ACSL: https://frama-c.com/html/acsl.html
lists a V.18, but this version is not present on the ACSL github site: https://github.com/acsl-language/acsl/releases
where v17 is marked as "latest"
I do see that version.tex says v18 - so perhaps no one pushed the button to publish a build of v18.