frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2023-09-13T15:15:27Zhttps://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 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.https://git.frama-c.com/pub/frama-c/-/issues/2653(Simple) Bad link on public web page2023-04-03T08:17:34ZDavid Cok(Simple) Bad link on public web pageOn the "Contact-us" page for frama-c: https://frama-c.com/html/contact.html
the "ACSL on github" links just to a .png: https://frama-c.com/assets/img/community/github.png
rather than to the appropriate github page -- or perhaps that entr...On the "Contact-us" page for frama-c: https://frama-c.com/html/contact.html
the "ACSL on github" links just to a .png: https://frama-c.com/assets/img/community/github.png
rather than to the appropriate github page -- or perhaps that entry is obsolete - as current work is on gitlab.https://git.frama-c.com/pub/frama-c/-/issues/2651[WP] Value of 2D-array does not work well2023-03-28T08:47:37ZJim Chen[WP] Value of 2D-array does not work well<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
```c++
#define NUM 5
int x[NUM][NUM];
/*@
@ requires \forall integer i, j; 0 <= i < NUM && 0 <= j < NUM ==> 0 <= x[i][j] < 100;
@*/
void foo()
{
int tmp;
for (int i = 0; i < NUM; i++)
{
for (int j = 0; j < NUM; j++)
{
tmp = x[i][j] + 1;
//@ assert PASS: 1 <= tmp < 101;
//@ assert ASSERTED: tmp < 100;
}
}
if (tmp > 100)
{
tmp = 1;
return;
}
else
{
tmp = 2;
return;
}
}
```
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
PASS should be pass and ASSERTED should be triggered.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
Both of the assertion were triggered in WP
i'm using command:
`frama-c -wp -wp-no-rte -wp-prover z3-nobv,alt-ergo -wp-cache 'rebuild' -wp-model 'Typed' -pp-annot -c11 -kernel-msg-key pp -main foo -lib-entry ./test.c`
### Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *26.1* (as reported by `frama-c -version`)
- Plug-in used: *WP*
- OS name: *Ubuntu*
- OS version: *20.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.
-->
this 2d-array phenomenon is also observed when I'm writing loop assigns like this:
```c++
#define NUM 5
int x[NUM][NUM];
/*@
@ ;
@*/
void foo()
{
/*@
@ loop assigns x[0 .. NUM - 1][0 .. NUM - 1];
@*/
for (int i = 0; i < NUM; i++)
{
/*@
@ loop assigns x[i][0 .. NUM - 1];
@*/
for (int j = 0; j < NUM; j++)
{
x[i][j] = i * j;
}
}
return;
}
```Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2650Stack overflow using WP in Wp__Register.step_finally2023-03-29T20:08:35ZChristophe GarionStack overflow using WP in Wp__Register.step_finallyFrama-C 26.1 and its WP plugin crash with a stack overflow when trying to prove a function:
```
The full backtrace is:
Raised at Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 834, characters 41-48
Called fro...Frama-C 26.1 and its WP plugin crash with a stack overflow when trying to prove a function:
```
The full backtrace is:
Raised at Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 834, characters 41-48
Called from Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 835, characters 2-12
Called from Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 835, characters 2-12
Called from Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 835, characters 2-12
Called from Stdlib__Queue.iter.iter in file "queue.ml", line 121, characters 6-15
Called from Frama_c_boot__Boot.play_analysis in file "src/init/boot/boot.ml", line 36, characters 4-20
Called from Frama_c_kernel__Cmdline.play_in_toplevel_one_shot in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 850, characters 2-9
Called from Frama_c_kernel__Cmdline.play_in_toplevel in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 880, characters 18-64
Called from Frama_c_kernel__Cmdline.catch_toplevel_run in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 233, characters 4-8
Unexpected error (Stack overflow).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 26.1 (Iron).
```
The function to be proved is part of a rather big C file included in the attached archive. Sorry for the complexity (and maybe the bad quality) of the C code, it is in fact produced by a Lustre compiler we are working on. I will try to produce a real MWE...
Running Frama-C and WP on the whole file causes a stack overflow on `List.map` but I reduce the error when proving the `Arrays1_Arrays1_node_step` function. I use the `ref` and the `real` memory model.
When launching Frama-C on the function, no goal is produced (at least there is no printing of it), only Frama-C is running (there is no process involving Alt-Ergo or Z3 for instance). the crash happens after 13 minutes (!) on my computer (a recent laptop with i9 cores).
### Steps to reproduce the issue
* open the attached archive
* issue the following command:
```
frama-c -wp -wp-model ref,real -wp-fct Arrays1_Arrays1_node_step Arrays1.c
```
### Contextual information
- Frama-C installation mode: opam with an OCaml 4.14.0 switch
- Frama-C version: 26.1 (Iron)
- Plug-in used: WP
- OS name: Linux
- OS version: 22.04
Thanks,
Christophe
[arrays_stack_overflow_wo_optimization.tgz](/uploads/e88a0fcabd4de811d59024517c679f5d/arrays_stack_overflow_wo_optimization.tgz)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2647Frama-C 26 crashes when trying CFG plugin from Frama-C plugin development guide2023-02-10T08:37:41ZChristophe GarionFrama-C 26 crashes when trying CFG plugin from Frama-C plugin development guideHello,
Frama-C 26.0 just crashed when I tried to reproduce the CFG plugin example from the Frama-C plugin development guide. Everything was OK until I tried to use the `bogue` library for the mini-GUI example. Executing Frama-C through ...Hello,
Frama-C 26.0 just crashed when I tried to reproduce the CFG plugin example from the Frama-C plugin development guide. Everything was OK until I tried to use the `bogue` library for the mini-GUI example. Executing Frama-C through dune leads to a crash:
```
Done: 0% (0/0, 0 left) (jobs: 0)[kernel] Current source was: :0
The full backtrace is:
Raised at Dune_site_plugins__Plugins.load_gen in file "otherlibs/site/src/plugins/plugins.ml", line 251, characters 6-89
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/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/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/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/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 918, 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 (It is not possible to dynamically link a plugin which uses the thread library
with an executable not already linked with the thread
library.).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 26.0 (Iron).
```
### Steps to reproduce the issue
- install both Frama-C and bogue through Opam
- extract the attached archive containing the plugin source (see [view-cfg.tar.gz](/uploads/d9bad096f63e6a429bb7c7683789fa97/view-cfg.tar.gz))
- execute `dune build`
- execute Frama-C through dune with `dune exec -- frama-c`
### Contextual information
- Frama-C installation mode: Opam with an OCaml 4.14.1 switch
- Frama-C version: 26.0 (Iron)
- Plug-in used: "homemade" CFG plugin from the plugin development guide
- OS name: Linux
- OS version: Ubuntu 22.04
### Additional information
I looked through the bugtracker but did not find any related issue. I hope I did not make a stupid mistake by copying the code from the guide!Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2645Installation in local OPAM switch with dune-project fails2023-02-14T09:11:20ZLélio BrunInstallation in local OPAM switch with dune-project fails<!--
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.
-->
Create a local OPAM switch, create an empty `dune-project` file, install Frama-C (last version 26).
```
mkdir test
cd test
opam switch create . 4.14.1
eval (opam env)
touch dune-project
opam install frama-c
```
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
Installation succeeds.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
Installation fails:
```
[ERROR] The installation of frama-c failed at "make PREFIX=/home/lelio/Projects/test/_opam MANDIR= install".
#=== ERROR while installing frama-c.26.0 ======================================#
# context 2.1.4 | linux/x86_64 | ocaml-base-compiler.4.14.1 | https://opam.ocaml.org#34077df0
# path ~/Projects/test/_opam/.opam-switch/build/frama-c.26.0
# command ~/.opam/opam-init/hooks/sandbox.sh install make PREFIX=/home/lelio/Projects/test/_opam MANDIR= install
# exit-code 2
# env-file ~/.opam/log/frama-c-2744448-3e4244.env
# output-file ~/.opam/log/frama-c-2744448-3e4244.out
### output ###
# Installing Frama-C to current Opam switch
# (copying and relocating files...)
# make: *** [share/Makefile.installation:62: install] Error 1
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
┌─ The following actions failed
│ ∗ install frama-c 26.0
└─
╶─ No changes have been performed
```
### Contextual information
- Frama-C installation mode: *local Opam switch with `dune-project` file*
- Frama-C version: *26.0*
- OS name: *Archlinux*
### 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.
-->
I precise that the procedure works well for anterior versions (eg. 24, 25). It works also for version 26 if no `dune-project` file is present.
This is a minimal example, in my use case I didn't even have an error message, Frama-C was reported as successfully installed but the `frama-c` binary was actually not installed (in `_opam/bin/frama-c`).Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2644[WP] Fails to verify left shift by 2 on range2023-01-24T11:13:25ZCostava[WP] Fails to verify left shift by 2 on range<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
```c
/*@
requires a == 1;
assigns \nothing;
ensures \result == (a << 2);
*/
unsigned int do_one(const unsigned int a) {
return (a << 2);
}
/*@
requires a == 2;
assigns \nothing;
ensures \result == (a << 2);
*/
unsigned int do_two(const unsigned int a) {
return (a << 2);
}
/*@
requires 1 <= a <= 2;
assigns \nothing;
ensures \result == (a << 2);
*/
unsigned int do_some_shift2(const unsigned int a) {
return (a << 2);
}
/*@
requires 1 <= a <= 2;
assigns \nothing;
ensures \result == (a << 1);
*/
unsigned int do_some_shift1(const unsigned int a) {
return (a << 1);
}
```
```sh
$ frama-c -wp -wp-rte fcshift.c
```
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
All goals verified successfully.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
```sh
$ frama-c -wp -wp-rte fcshift.c
[kernel] Parsing fcshift.c (with preprocessing)
[rte:annot] annotating function do_one
[rte:annot] annotating function do_some_shift1
[rte:annot] annotating function do_some_shift2
[rte:annot] annotating function do_two
[wp] 8 goals scheduled
[wp] [Alt-Ergo 2.4.1] Goal typed_do_some_shift2_ensures : Timeout (Qed:2ms) (10s)
[wp] Proved goals: 7 / 8
Qed: 6 (0.33ms-0.64ms-2ms)
Alt-Ergo 2.4.1: 1 (10ms) (92) (interrupted: 1)
```
The ensures goal can be verified when `a` has a single value of either `1` or `2` respectively for the `do_one` and `do_two` functions.
But if `a` is `1` or `2` (for function `do_some_shift2`), then the ensures goal fails to verify.
Oddly, the goal succeeds if the left shift is by `1` instead of `2` (function `do_some_shift1`).
[cppreference.com](https://en.cppreference.com/w/c/language/arithmetic_types) is stating that `unsigned int` should always have at least 16 bits, so it is weird to me that changing the amount of the shift is making a difference.
Doubling the timeout to 20 does not make the goal succeed automatically.
Using `frama-c-gui`, I know that I can apply tactic `Logical Shift` on `lsl(a, 2)` in order to make the goal succeed, but a goal that is this specific and simple failing to verify seems like a bug.
### Contextual information
- Frama-C installation mode: opam
- Frama-C version: 25.0 (Manganese)
- Plug-in used: WP, RTE, Alt-Ergo 2.4.1
- OS name: Manjaro Linux
- OS version: Sikaris 22.0.0
### Additional information (optional)
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->
N/ALoïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2643[WP] Isabelle/HOL driver does not work2024-02-27T11:34:19Zkwaxer[WP] Isabelle/HOL driver does not work### 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 : enum...### 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 test.h`
4. Observe the following output:
```
[wp] 1 goal scheduled
[wp] [Unknown] typed_lemma_enumeration_length (Isabelle)
[wp] Proved goals: 0 / 1
Qed: 0
Unknown: 1
```
5. Observe that no new files or directories are created.
### Expected behavior
Some generated files/directories that can be used to prove the goal in Isabelle/HOL.
### Actual behavior
Nothing is generated, and no errors are reported. The verification fails silently without any clue about what went wrong.
### Contextual information
- Frama-C: 26.0 (Iron) installed with `opam`
- Why3: 1.5.1 installed with `opam`
- Isabelle: 2021-1
- OS: Ubuntu 22.04.1 LTSLoïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2639Parse-print-reparse error with ranges2024-03-14T16:37:09ZNikolai KosmatovParse-print-reparse error with ranges## Contextual information: currently used versions
- Frama-C installation mode: *Opam*
- Frama-C version 26.0beta
- MetAcsl 0.4beta
- Alt-Ergo 2.3.2
- OS name: *Ubuntu*
- OS version: *20.04*
## The issue
On the attached file, after pa...## Contextual information: currently used versions
- Frama-C installation mode: *Opam*
- Frama-C version 26.0beta
- MetAcsl 0.4beta
- Alt-Ergo 2.3.2
- 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 in ranges).
[f.c](/uploads/dac68b95adf9d3c2c83b7b3ec9ce5898/f.c)
Here is the example
```
// Run frama-c on this file and pretty-print it:
// frama-c f.c -print -no-unicode -ocode f_printed.c
// Run on the resulting pretty-printed file:
// frama-c f_printed.c
typedef unsigned char uchar;
typedef unsigned long ulong;
typedef unsigned char *pchar;
uchar *Ref;
uchar Array[100];
/*@ ghost ulong FCG_Var1[1000]; */
/*@ ensures
sep1:
\let Ref_range = Ref + (0 .. (1 << (size)) - 1);
\let PROP = \forall integer MyNum;
\let myrange = (0 .. (6 - 1));
\let Var2 = &Array[FCG_Var1[MyNum]];
\let CASE_i = 0 <= MyNum < 10;
\let PROP_i =
\separated(Ref_range, Var2 + myrange);
CASE_i ==> PROP_i;
PROP;
*/
static uchar myfun(pchar p_array, short index, uchar size)
{
uchar __retres;
return __retres;
}
```
Here is the error message:
```
[kernel] Parsing f_printed.c (with preprocessing)
[kernel:annot-error] f_printed.c:11: Warning: unexpected token '..'
[kernel] User Error: warning annot-error treated as fatal error.
[kernel] User Error: stopping on file "f_printed.c" that has errors. Add '-kernel-msg-key pp'
for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
```https://git.frama-c.com/pub/frama-c/-/issues/2638Parse-print-reparse error with ghost arrays2023-01-17T13:05:30ZNikolai KosmatovParse-print-reparse error with ghost arrays## Contextual information: currently used versions
- Frama-C installation mode: *Opam*
- Frama-C version 26.0beta
- MetAcsl 0.4beta
- Alt-Ergo 2.3.2
- OS name: *Ubuntu*
- OS version: *20.04*
## The issue
On the attached file, after pa...## Contextual information: currently used versions
- Frama-C installation mode: *Opam*
- Frama-C version 26.0beta
- MetAcsl 0.4beta
- Alt-Ergo 2.3.2
- 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 (that disappears after manually removing \ghost attribute).
[f_cut.c](/uploads/90f52009ec5f1412c371349b3fca3659/f_cut.c)
Here is the example
```
// Run frama-c on this file and pretty-print it:
// frama-c f_cut.c -print -no-unicode -ocode f_cut_printed.c
// Run on the resulting pretty-printed file:
// frama-c f_cut_printed.c
typedef unsigned char uint8;
typedef unsigned short uint16;
typedef unsigned long uint32;
uint8 Array[10];
/*@ ghost uint32 FCG_Number; */
/*@ ghost uint32 FCG_Var1[1000]; */
/*@ ghost uint32 FCG_Var2[1000]; */
/*@
predicate mypredl{L}=
(\forall integer MyNum;
0 <= MyNum < FCG_Number ==> FCG_Var2[MyNum] ==
((uint16)(*((uint8 *)(&Array[FCG_Var1[MyNum]] + (1))) * 256 + *((uint8 *)((&Array[FCG_Var1[MyNum]] + (1 + 2)) + 1)))) ) ;
*/
```
Here is the error message:
```
[kernel] Parsing f_cut_printed.c (with preprocessing)
[kernel:annot-error] f_cut_printed.c:14: Warning: unexpected token '\ghost'
[kernel] User Error: warning annot-error treated as fatal error.
[kernel] User Error: stopping on file "f_cut_printed.c" that has errors. Add '-kernel-msg-key pp'
for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
```