frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2024-02-14T11:19:42Zhttps://git.frama-c.com/pub/frama-c/-/issues/2689[wp] Failing to understand certain bitwise properties2024-02-14T11:19:42ZPhillip Allen Lane[wp] Failing to understand certain bitwise properties<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
I have the following Frama-C which should prove this seemingly trivial assertion about an integer containing all 1s:
```c
#include <stdint.h>
#define ALLONES 0xFFFFFFFFu
/*@
assigns \nothing;
*/
void tests(void)
{
uint32_t allones = ALLONES;
//@ assert \forall uint32_t i ; 0 <= i < 32 ==> (allones & (1u << i)) != 0;
}
```
### Expected behaviour
All goals should be proven.
### Actual behaviour
Running with:
```
frama-c -wp -wp-rte -wp-smoke-tests -wp-prover z3 -wp-par 32 -wp-print test.c
```
I get:
```
[kernel] Parsing test.c (with preprocessing)
[rte:annot] annotating function tests
[wp] 2 goals scheduled
[wp] [Timeout] typed_tests_assert (Qed 0.86ms) (Z3) (Cached)
[wp] [Cache] updated:1
[wp] Proved goals: 3 / 4
Terminating: 1
Unreachable: 1
Qed: 1
Timeout: 1
------------------------------------------------------------
Function tests
------------------------------------------------------------
Goal Assertion (file test.c, line 10):
Assume { (* Goal *) When: (0 <= i) /\ (i <= 31). }
Prove: land(4294967295, lsl(1, i)) != 0.
Prover Z3 4.8.12 returns Timeout (Qed:0.86ms) (2s)
------------------------------------------------------------
Goal Assigns nothing in 'tests':
Prove: true.
Prover Qed returns Valid
------------------------------------------------------------
```
### Contextual information
I have tried other provers (CVC4, Alt-Ergo) and none of them are able to prove the assertion. Looking at some of the Coq axioms generated, I am suspicious that Frama-C is not providing the SMT solvers with enough information about bitwise operations to be able to deduce the conclusion.
When I run Frama-C with a different assertion:
```c
//@ assert \forall uint32_t i ; i == 0 ==> (allones & (1u << i)) != 0;
```
The assertion succeeds (via Qed). This works for all valid values of `i` (e.g., `i in [0 .. 31]`), but fails when I try to quantify over the entire range.
Here's some relevant information that may be helpful:
- Frama-C installation mode: Opam
- Frama-C version: 28.0 (Nickel)
- Plug-in used: WPLoïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2688[wp] Failure: [Why3 Error] anomaly: Not_found2024-01-19T08:10:37ZJulia Lawall[wp] Failure: [Why3 Error] anomaly: Not_foundSee attached files. The output with the command line argument -wp-msg-key why3_api ends with the following. The attached directory contains a make file, so you can just run `make v1`.
```
> [wp:why3_api] of_term prop c_1.F1_cpumask_bi...See attached files. The output with the command line argument -wp-msg-key why3_api ends with the following. The attached directory contains a make file, so you can just run `make v1`.
```
> [wp:why3_api] of_term prop c_1.F1_cpumask_bits[0]=c_0.F1_cpumask_bits[0]
> [wp] Failure: [Why3 Error] anomaly: Not_found
> Raised at Qed__Term.Make.tau_of_arraysort in file
> "src/plugins/qed/term.ml", line 2831, characters 11-26
> Called from Wp__ProverWhy3.of_term in file "src/plugins/wp/ProverWhy3.ml", line 461, characters 14-29
> Called from Wp__ProverWhy3.of_term in file "src/plugins/wp/ProverWhy3.ml", line 450, characters 14-39
> Called from Wp__ProverWhy3.of_term.fold in file "src/plugins/wp/ProverWhy3.ml", line 453, characters 16-44
> Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
> Called from Wp__ProverWhy3.share in file "src/plugins/wp/ProverWhy3.ml", line 633, characters 10-33
> Called from Wp__ProverWhy3.successive_binders in file "src/plugins/wp/ProverWhy3.ml", line 669, characters 8-24
> Called from Wp__ProverWhy3.successive_binders in file "src/plugins/wp/ProverWhy3.ml", line 666, characters 23-49
> Called from Wp__ProverWhy3.successive_binders in file "src/plugins/wp/ProverWhy3.ml", line 666, characters 23-49
> Called from Wp__ProverWhy3.successive_binders in file "src/plugins/wp/ProverWhy3.ml", line 666, characters 23-49
> Called from Wp__ProverWhy3.successive_binders in file "src/plugins/wp/ProverWhy3.ml", line 666, characters 23-49
> Called from Wp__ProverWhy3.successive_binders in file "src/plugins/wp/ProverWhy3.ml", line 666, characters 23-49
> Called from Wp__ProverWhy3.successive_binders in file "src/plugins/wp/ProverWhy3.ml", line 666, characters 23-49
```
[files.tar.gz](/uploads/39c90bd26cf8493c15edcdffa8c55c24/files.tar.gz)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2685[WP] save / load not saving strategies2023-12-14T10:13:17ZTeo BERNIER[WP] save / load not saving strategies### Steps to reproduce the issue
On the attached examples :
[test.c](/uploads/8a2ca334a3a2ef8d696da2df986bdd45/test.c)
running the following command
`frama-c test.c -wp -wp-prover=tip -wp-prop post`
works perfectly, but when we u...### Steps to reproduce the issue
On the attached examples :
[test.c](/uploads/8a2ca334a3a2ef8d696da2df986bdd45/test.c)
running the following command
`frama-c test.c -wp -wp-prover=tip -wp-prop post`
works perfectly, but when we use the save / load features with the following command (and after removing the existing scripts)
`frama-c test.c -save tmp.sav ; frama-c -load tmp.sav -wp -wp-prover=tip -wp-prop post`
it does not work anymore and, when we add option
`-wp-strategy InstanceForall`,
Frama-C outputs
`[wp] Warning: Invalid -wp-strategy 'InstanceForall' (undefined strategy name)`
### Expected behaviour
We would expect save / load to keep strategies available.
### Actual behaviour
Strategies seems to not be correctly saved / loaded and when specified, they are declared `undefined` by WP.
### Contextual information
* Frama-C installation mode: opam install frama-c.28.0
* Frama-C version: 28.0
* Plug-in used: WP with why3 1.6.0 and Alt-Ergo 2.4.3
* OS name: Ubuntu
* OS version: 20.04
FYI: @nkosmatovhttps://git.frama-c.com/pub/frama-c/-/issues/2684[WP] crash observed with scripts and strategies2023-12-14T10:28:20ZNikolai Kosmatov[WP] crash observed with scripts and strategies### Expected behaviour
No crash
### Actual behaviour
Crash in some situations when running WP in the presence of existing scripts recorded via strategies.
Here is a screenshot (with a hidden full file name).
![crash_on_recorded_scri...### Expected behaviour
No crash
### Actual behaviour
Crash in some situations when running WP in the presence of existing scripts recorded via strategies.
Here is a screenshot (with a hidden full file name).
![crash_on_recorded_scripts](/uploads/11287a2731db4ea55108b4395f95b940/crash_on_recorded_scripts.png)
### Contextual information
- Frama-C installation mode: *Opam from public GIT*
- Frama-C version: *28.0+dev (Nickel)* commit cdd528, similar behavior observed on 28.0beta
- Plug-in used: *WP*
- OS name: *Ubuntu*
- OS version: *22.04*
FYI @tbernierhttps://git.frama-c.com/pub/frama-c/-/issues/2683[WP] non-matching of strategies with forall and implication2023-11-27T09:24:34ZTeo BERNIER[WP] non-matching of strategies with forall and implication### Steps to reproduce the issue
On the attached examples :
- [forall_pattern.c](/uploads/2df4b07af5737279a5d34001b7d10822/forall_pattern.c)
running the following command
`frama-c-gui forall_pattern.c -wp -wp-rte -wp-prover...### Steps to reproduce the issue
On the attached examples :
- [forall_pattern.c](/uploads/2df4b07af5737279a5d34001b7d10822/forall_pattern.c)
running the following command
`frama-c-gui forall_pattern.c -wp -wp-rte -wp-prover=tip -wp-prop post`
to apply a strategy with Instance does not seem to accept the pattern and to match the precondition using `\forall`.
```
strategy FastAltErgo: \prover("alt-ergo", 1); // run Alt-Ergo for 1 sec.
strategy InstanceForall:
\tactic("Wp.instance",
\pattern(\forall integer _; _), // fails to select the \forall (invalid pattern)
// \when(_), // works in this specific example
\goal(P_P(i)),
\param("P1", i),
\children(FastAltErgo)
);
proof InstanceForall: post;
```
- [implication_pattern.c](/uploads/8c4a42b5917b980ffe994189507fb7c6/implication_pattern.c)
running the following command
`frama-c-gui implication_pattern.c -wp -wp-rte -wp-prover=tip -wp-prop post`
to apply a strategy with Cut does not seem to accept the pattern and to match the precondition using `==>`.
```
strategy FastAltErgo: \prover("alt-ergo", 1); // run Alt-Ergo for 1 sec.
strategy CutImplication:
\tactic("Wp.cut",
\pattern(A ==> _), // fails to select the implication (invalid pattern)
// \incontext(A: _ <= 99), // works in this specifi example
\param("case", "CASES"),
\param("clause", A),
\children(FastAltErgo)
);
proof CutImplication: post;
```
### Expected behaviour
We would expect `\forall` and `==>` to be matched like other acsl expression.
### Actual behaviour
Syntax error is reported (Invalid pattern. Ignoring global annotation).
### Contextual information
- Frama-C installation mode: opam pin add frama-c https://git.frama-c.com/pub/frama-c.git#64438ed52f9af0052d6f3970202fc48dbc580dba
- Frama-C version: 28.0+dev (commit 64438ed52f9af0052d6f3970202fc48dbc580dba)
- Plug-in used: WP with why3 1.6.0 and Alt-Ergo 2.5.2
- OS name: Ubuntu
- OS version: 22.04
FYI: @nkosmatovLoïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2681[kernel] Conflicting types error for enum & typedef enum2024-01-17T11:25:46ZT-Gruber[kernel] Conflicting types error for enum & typedef enumI have encountered a problem that leads to an error when parsing. This occurs when an enum is defined multiple times as shown below. The expectation would be that it works as with the struct shown:
- forward declaration of struct/enum
- ...I have encountered a problem that leads to an error when parsing. This occurs when an enum is defined multiple times as shown below. The expectation would be that it works as with the struct shown:
- forward declaration of struct/enum
- introducing an alias via typedef
- both in one
```C
// test.c
// works
struct my_struct;
typedef struct my_struct my_struct;
typedef struct my_struct {
int val;
} my_struct;
// fails
enum my_enum;
typedef enum my_enum my_enum;
typedef enum my_enum {
VAL
} my_enum;
```
### Steps to reproduce the issue
Parse source file:
```
frama-c test.c
```
### Expected behaviour
Output:
```
[kernel] Parsing test.c
```
### Actual behaviour
Output:
```
[kernel] Parsing test.c
[kernel] test.c:14: User Error:
redefinition of type 'my_enum' in the same scope with conflicting type.
Previous declaration was at test.c:10
[kernel] User Error: stopping on file "test.c" that has errors.
[kernel] Frama-C aborted: invalid user input.
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 27.0 (Cobalt)
- OS: Ubuntu 22.04.2 LTS (WSL)https://git.frama-c.com/pub/frama-c/-/issues/2679\separated for stack-allocated variable length arrays2023-11-20T07:30:50ZAdharsh Kamath\separated for stack-allocated variable length arraysI have been trying to verify the following program with Frama-c (WP plugin).
```
#include <stdlib.h>
#define assume(e) if(!(e)) exit(-1);
extern int unknown_int(void);
int N;
int main()
{
N = unknown_int();
if(N <=0 )...I have been trying to verify the following program with Frama-c (WP plugin).
```
#include <stdlib.h>
#define assume(e) if(!(e)) exit(-1);
extern int unknown_int(void);
int N;
int main()
{
N = unknown_int();
if(N <=0 ) return 1;
int i;
int a[N];
int b[N];
a[0] = 0;
b[0] = 1;
//@ assert b[0] == 1;
//@ assert \separated(a,b);
//@ assert a[0] == 0;
return 1;
}
```
For which frama-c, outputs the following statuses for each assertion
```
Assertion 0 < sizeof(int) * N <= 18446744073709551615: Valid
Assertion 0 < sizeof(int) * N <= 18446744073709551615: Valid
Assertion *(b + 0) == 1: Valid
Assertion \separated(a + 0, b + 0): Unknown
Assertion *(a + 0) == 0: Partially proven
```
When I change one of the arrays to a constant-sized array, say b to int [100], the output changes to
```
Assertion 0 < sizeof(int) * N <= 18446744073709551615: Valid
Assertion b[0] == 1: Valid
Assertion \separated(a + 0, &b[0]): Valid
Assertion *(a + 0) == 0: Valid
```
Is it not fair to assume stack-allocated arrays don't alias? Why does Frama-c treat variable length arrays differently from constant-sized ones?Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2678Turn off implicit promotion of float and double2023-11-20T07:30:29ZAdharsh KamathTurn off implicit promotion of float and doubleI have a function `f` whose post-condition I want to verify. Following is the function `f` along with its ensures clause:
```c
/*@
ensures \result == x - (x*x*x)/6.0f;
*/
float f(float x)
{
return x - (x*x*x)/6.0f;
}
```
Frama-C, (wi...I have a function `f` whose post-condition I want to verify. Following is the function `f` along with its ensures clause:
```c
/*@
ensures \result == x - (x*x*x)/6.0f;
*/
float f(float x)
{
return x - (x*x*x)/6.0f;
}
```
Frama-C, (with WP only) returns "Unknown" as the status of this post-condition. Does this have anything to do with the implicit promotion of floats to reals?
From the ACSL Implementation document ([https://frama-c.com/download/frama-c-acsl-implementation.pdf](https://frama-c.com/download/frama-c-acsl-implementation.pdf), Section 2.2.5):
> Unlike the promotion of C integer types to mathematical integers, there are special float values that do not naturally map to a real number, namely the IEEE-754 special values for “not-a-number”, +∞ and −∞. See below for a detailed discussion on such special values. However, remember that ACSL’s logic has only total functions. Thus, there are implicit promotion functions `real_of_float` and `real_of_double` whose results on
the 3 values above is left unspecified.
Is there a way to turn off this implicit promotion of `float` to `real`?
**More importantly, is there a way to verify the post-condition of functions like `f` (given above), that involve floating point values?**Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2676E-ACSL : non-existent assigns clause in behavior2023-11-09T08:24:50ZYani ZIANIE-ACSL : non-existent assigns clause in behavior<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
Run the following code with E-ACSL using ``e-acsl-gcc.sh -c -O assigns_test.out assigns_test.c``:
```C
/* assigns_test.c */
#include <limits.h>
int global_int;
/*@
requires INT_MIN < global_int < INT_MAX;
assigns global_int;
*/
int abs_global(){
if(global_int < 0) {return -global_int;}
return global_int;
}
int main(){
global_int = 0;
int local_int = abs_global();
return local_int;
}
```
### Expected behaviour
Instrumentation happens without warning.
### Actual behaviour
The following warning ``[e-acsl] assigns_test.c:9: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported.`` is reported, despite the function contract of ``abs_global`` not featuring any behavior.
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: at least from 26, still there in 28~beta
- Plug-in used: E-ACSL
- OS name: Ubuntu (via WSL)
- OS version: 22.04.2 LTS
FYI @nkosmatov
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->Julien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/2675Unclear status for loop invariants in CSV report2023-11-06T08:45:05ZAdharsh KamathUnclear status for loop invariants in CSV reportThe meaning of the status for each loop invariant in the CSV file output by the report plugin is unclear. The WP plugin manual does not contain any details regarding the same.
What does "Unknown" or "Partially Proven" status mean for a l...The meaning of the status for each loop invariant in the CSV file output by the report plugin is unclear. The WP plugin manual does not contain any details regarding the same.
What does "Unknown" or "Partially Proven" status mean for a loop invariant?
Does "Unknown" mean the following?
> Under the hypothesis that the other invariants are inductive (established and preserved), this invariant could not be proven to be inductive (failed establishment or preservation, or both)
For example, consider the following program:
```c
extern int unknown_int(void);
int main() {
int i, m, n;
int j, k;
n = unknown_int();
i = unknown_int();
m = unknown_int();
if (!( n == i / 32 )) return 0;
/*@
loop invariant i1: 0 <= j <= i / 8;
loop invariant i2: 0 <= j <= m;
loop invariant i3: j * 4 <= i;
loop invariant i4: j <= n * 8;
*/
for (j = 0; (j < i / 8) && (j < m); j++) {
//@ assert( j/4 < n);
}
return 0;
}
```
Invoking Frama-C with the following command, results in a CSV file with the status for each property:
```
frama-c -wp -wp-verbose 100 -wp-debug 100 -wp-timeout 3 -wp-prover=z3,alt-ergo,cvc4 temp.c -then -report -report-csv frama_c_dump_.csv
```
The CSV output file contains the following:
```
directory file line function property kind status property
. temp.c 1 unknown_int assigns clause Unknown assigns \nothing;
. temp.c 1 unknown_int from clause Unknown assigns \result \from \nothing;
. temp.c 13 main loop invariant Unknown 0 ≤ j ≤ i / 8
. temp.c 14 main loop invariant Unknown 0 ≤ j ≤ m
. temp.c 15 main loop invariant Unknown j * 4 ≤ i
. temp.c 16 main loop invariant Partially proven j ≤ n * 8
. temp.c 19 main user assertion Unknown j / 4 < n
```
What does the status "Unknown" assigned to multiple invariants i1, i2, and i3 mean?
More specifically, **what does it mean to have multiple "Unknown" loop invariants?** Is there a formal description of the possible status values and their meanings? If so, could you please point me in that direction?Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2674Consistency of uses of \from clauses2023-10-25T16:54:47ZNikolai KosmatovConsistency of uses of \from clausesThis issue describes a certain inconsistency in usages of the `\from` clauses in different plugins.
WP relies on `\from` clauses to facilitate pointer analysis for correct memory model assumptions.
This feature is very helpful.
MetAcsl...This issue describes a certain inconsistency in usages of the `\from` clauses in different plugins.
WP relies on `\from` clauses to facilitate pointer analysis for correct memory model assumptions.
This feature is very helpful.
MetAcsl relies on (`assigns` and in particular) `\from` clauses to instantiate metaproperties
for callees based on their contracts. This can be used for undefined functions or in some cases
for defined functions for better performances of the global proof. This feature is also very helpful.
There is a certain inconsistency of both usages on the same code: only a base address is
necessary for the first usage, while a complete list of dependencies is expected in the second case.
It would be desirable to avoid the usage of the same clause in two different ways.
One suggestion can be to use another clause like `\from_ptr` or `\from_base` for the first case.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/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/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/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/2652Unproven validity of memory access2023-05-16T06:54:01ZYani ZIANIUnproven validity of memory access<!--
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]…
-->
### Description
According to the ACSL language implementation p.67 for Frama-C v26.0 and 26.1 (modulo potential alignment constraints), the ``valid {L}(p) <==> \valid{L}(((char *)p)+(0 .. sizeof(*p)-1))`` equivalence should hold true for any pointer ``p`` (and would be in line with C's behavior when trying to access any pointer as an array of bytes). But I've run into trouble trying to prove it in simple cases, be it using the ``Typed`` memory model, or its extension using ``+cast``.
### 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.
-->
Running Frama-C with WP on the minimal code inlined below, or running ``frama-c-gui char_ptr.c -wp `` and ``frama-c-gui char_ptr.c -wp -wp-model Typed+cast`` using the attachments.
```C
#include <stdio.h>
typedef struct {
int test_buffer[5];
} test_type;
int * test_ptr;
test_type * _test_type_ptr;
int dummy_valid()
{
/*@ check \valid(test_ptr) ==> \valid(((char *) test_ptr) + (0 .. (size_t) sizeof(*test_ptr) -
/*@ check \valid(((char *) test_ptr) + (0 .. (size_t) sizeof(*test_ptr) - 1)) ==> \valid(
/*@ check \valid(_test_type_ptr) ==> \valid(((char *) _test_type_ptr) + (0 .. (size_t) sizeof(*_test_type_ptr) -
/*@ check \valid((char *) _test_type_ptr + (0 .. (size_t) sizeof(*_test_type_ptr) - 1)) ==> \valid(_test_type_ptr);*/
return 0;
}
```
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
All check clauses should be proved when using the ``+cast`` variant of ``Typed``.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
None of the check clauses extending the validity of the original pointer to the validity of the corresponding byte array are proved.
My understanding/guess would be that it may be due to WP's ability to translate the cast to ``char *`` to byte accesses, but I'm really not clear on what's actually happening there.
```
```
### Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: 26.0 (Iron)
- Plug-in used: WP
- OS name: Ubuntu
- OS version: 20.04.4 LTS
### Additional information (optional)
- Alt-Ergo version : 2.4.2
<!--
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.
-->
FYI @nkosmatov
[char_ptr.c](/uploads/8ebaf1fac5f9a9c8de2e0367ef0cd628/char_ptr.c)Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2649[WP] no trivial separation of the allocation status of heap and local variabl...2023-02-15T07:38:06ZYani ZIANI[WP] no trivial separation of the allocation status of heap and local variables whose address are taken<!--
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]…
-->
### Description
I'm currently working on specifying and proving functions focused on linked list structures using previous works based on ACSL logic lists (cf this [paper](https://nikolai-kosmatov.eu/publications/blanchard_kl_sac_2019.pdf)), and I've encountered some issues proving relatively simple assertions when certain types of memory separation between pointers are involved.
### 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.
-->
Running Frama-C with WP on the minimal code inlined below, or running ``frama-c-gui linked_ll_dptr_proof.c -wp -wp-rte -wp-prover altergo,cvc4,cvc4-ce -wp-smoke-tests -wp-fct="dummyCaller, dummyCaller_bis" &`` using the attachments.
I've also taken the liberty of attaching an extended version of the code below in ``linked_ll_dptr_proof.c`` including all the logic definitions (modulo name changes) used in the "Logic against Ghosts" paper, as well as the corresponding lemmas in ``lemmas_list.h``, but I'm not really sure of their relevance, as the issue also occurs on variants of the original logic definitions of the paper that are not used by said lemmas.
```C
#include <stdlib.h>
typedef struct LIST {
int handle;
struct LIST * next;
} LIST;
/**** Logic definitions from the "Logic against Ghosts" paper (modulo renaming for node_to_ll) ****/
/*@
predicate ptr_separated_from_range{L}
(LIST* e, \list<LIST*> ll, integer beg, integer end) =
\forall integer n ; 0 <= beg <= n < end <= \length(ll) ==> \separated(\nth(ll, n), e);
predicate dptr_separated_from_range{L}
(LIST** e, \list<LIST*> ll, integer beg, integer end) =
\forall integer n ; 0 <= beg <= n < end <= \length(ll) ==> \separated(\nth(ll, n), e);
predicate ptr_separated_from_list{L}(LIST* e, \list<LIST*> ll) =
ptr_separated_from_range(e, ll, 0, \length(ll));
predicate dptr_separated_from_list{L}(LIST** e, \list<LIST*> ll) =
dptr_separated_from_range(e, ll, 0, \length(ll));
*/
/*@
predicate in_list{L}(LIST* e, \list<LIST*> ll) =
\exists integer n ; 0 <= n < \length(ll) && \nth(ll, n) == e ;
*/
/*@
inductive linked_ll{L}(LIST *bl, LIST *el, \list<LIST*> ll) {
case linked_ll_nil{L}:
\forall LIST *el ; linked_ll{L}(el, el, \Nil);
case linked_ll_cons{L}:
\forall LIST *bl, *el, \list<LIST*> tail ;
\separated(bl, el) ==> \valid(bl) ==>
linked_ll{L}(bl->next, el, tail) ==>
ptr_separated_from_list(bl, tail) ==>
linked_ll{L}(bl, el, \Cons(bl, tail)) ;
}
*/
/*@
axiomatic Node_To_ll {
logic \list<LIST*> node_to_ll{L}(LIST* beg_node, LIST* end_node)
reads { node->next | LIST* node ; \valid(node) && in_list(node, node_to_ll(beg_node, end_node)) } ;
axiom to_ll_nil{L}:
\forall LIST *node ; node_to_ll{L}(node, node) == \Nil ;
axiom to_ll_cons{L}:
\forall LIST *beg_node, *end_node ;
\separated(beg_node, end_node) ==>
\valid{L}(beg_node) ==>
ptr_separated_from_list{L}(beg_node, node_to_ll{L}(beg_node->next, end_node)) ==>
node_to_ll{L}(beg_node, end_node) == (\Cons(beg_node, node_to_ll{L}(beg_node->next, end_node))) ;
}
*/
/*******************************************************************/
/*@
requires node_separation_to_list : dptr_separated_from_list(out_node, node_to_ll(rsrc_list, NULL)); //if uncommented, linked_assert cannot be proved
assigns \nothing;
ensures \result == 616;
*/
int dummyCallee(LIST * rsrc_list, LIST ** out_node);
/*@
requires linked_ll(rsrc_list, NULL, node_to_ll(rsrc_list, NULL));
assigns \nothing;
ensures \result == 616;
*/
int dummyCaller(LIST * rsrc_list, LIST ** out_node)
{
/*@ assert linked_assert : linked_ll(rsrc_list, NULL, node_to_ll(rsrc_list, NULL));*/ // should be proved from the precondition
int r;
LIST *test_node;
r = dummyCallee(rsrc_list, &test_node);
return r;
}
```
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
The ``linked_assert`` assertion in dummyCaller (or dummyCaller_bis in the attached files) should be always proved, even when the ``node_separation_to_list`` (and/or ``int_separation_to_list`` in attachments) preconditions are uncommented.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
None of the linked_assert assertions are proved.
The situation depicted by ``dummyCaller`` and ``dummyCallee``, using ``node_separation_to_list`` as a precondition, is the closest to the code I'm currently working on.
In the code in attachments, I also tried using ``node_separation_to_nil`` as precondition to test whether the issue also occured using a ``\Nil`` logic list, and the ``dummyCaller_bis`` and ``dummyCallee_bis`` functions to test if eliminating lemmas, or changing the datatype used for separation in ``dummyCallees``, had any influence on the issue, but they don't seem to.
```
```
### Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: 26.0 (Iron) (As well as version 25.0)
- Plug-in used: WP and RTE
- OS name: Ubuntu
- OS version: 20.04.4 LTS
### Additional information (optional)
- Alt-Ergo version : 2.4.2
- CVC4 version : 1.7
<!--
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.
-->
FYI @nkosmatov @floulergue
Edit: I completely forgot to add those attachments earlier :
[linked_ll_dptr_proof.c](/uploads/dd969cc3ce822db1c89e21fa939d0d48/linked_ll_dptr_proof.c)
[lemmas_list.h](/uploads/a9620641f45aa49d32cf7234f2d4ccfd/lemmas_list.h)Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2646OPAM installation on macOS fails2023-05-16T06:53:50ZvarosiOPAM installation on macOS 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.
-->
### Expected behaviour
To install correctly using OPAM on macOS Ventura 13.2 on x64 following - https://frama-c.com/html/get-frama-c.html
### Actual behaviour
After running **opam install frama-c**, I got:
```
> <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
> -> removed conf-gtk2.1
> -> installed conf-gtk2.1
> -> retrieved frama-c.21.1 (cached)
> [ERROR] The compilation of frama-c.21.1 failed at "make -j11".
>
> #=== ERROR while compiling frama-c.21.1 =======================================#
> # context 2.1.4 | macos/x86_64 | ocaml-base-compiler.4.07.1 | https://opam.ocaml.org#0c15cf29
> # path ~/.opam/default/.opam-switch/build/frama-c.21.1
> # command ~/.opam/opam-init/hooks/sandbox.sh build make -j11
> # exit-code 2
> # env-file ~/.opam/log/frama-c-37505-febf41.env
> # output-file ~/.opam/log/frama-c-37505-febf41.out
> ### output ###
> # [...]
> # Ocamlc src/plugins/qed/hcons.cmo
> # Ocamlc src/plugins/qed/listmap.cmo
> # Ocamlc src/plugins/qed/listset.cmo
> # Ocamlc src/plugins/qed/intmap.cmo
> # Ocamlc src/plugins/qed/intset.cmo
> # File "src/plugins/markdown-report/sarif.ml", line 31, characters 17-30:
> # Error: Unbound type constructor Yojson.Safe.t
> # make: *** [src/plugins/markdown-report/sarif.cmo] Error 2
> # make: *** Waiting for unfinished jobs....
> # Ocamlc src/plugins/qed/idxmap.cmo
> # AR src/plugins/e-acsl/lib/libeacsl-dlmalloc.a
> # RANLIB src/plugins/e-acsl/lib/libeacsl-dlmalloc.a
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: not installed previously
- OS name: macOS
- OS version: Ventura 13.2 on x64Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2642Installing Frama-C with opam fails2023-03-12T22:26:44ZHugo GimbertInstalling Frama-C with opam failsHello,
several students of mine were struggling today to install frama-c on their Ubuntu.
Can someone provide some feedback on the following error.
Example on Ubuntu 20.04, standard installation.
```
sudo apt-get remove opam
rm -fr ~...Hello,
several students of mine were struggling today to install frama-c on their Ubuntu.
Can someone provide some feedback on the following error.
Example on Ubuntu 20.04, standard installation.
```
sudo apt-get remove opam
rm -fr ~/.opam
sudo apt-get install opam
opam init
eval $(opam env)
opam install frama-c
```
leads to the following error
```
#=== ERROR while compiling alt-ergo-lib.2.4.2 =================================#
# context 2.0.5 | linux/x86_64 | ocaml-system.4.08.1 | https://opam.ocaml.org#0cd336b3
# path ~/.opam/default/.opam-switch/build/alt-ergo-lib.2.4.2
# command ~/.opam/opam-init/hooks/sandbox.sh build dune build -p alt-ergo-lib -j 1
# exit-code 1
# env-file ~/.opam/log/alt-ergo-lib-66410-e6f851.env
# output-file ~/.opam/log/alt-ergo-lib-66410-e6f851.out
### output ###
# 639 | [@ocaml.ppwarning "TODO: detect when there are no changes "]
# [...]
# Warning 22: TODO: detect when there are no changes
# (cd _build/default && /usr/bin/ocamlc.opt -w -40 -bin-annot -g -bin-annot -I src/lib/.AltErgoLib.objs/byte -I /home/yussef/.opam/default/lib/ocplib-simplex -I /home/yussef/.opam/default/lib/seq -I /home/yussef/.opam/default/lib/stdlib-shims -I /home/yussef/.opam/default/lib/zarith -no-alias-deps -open AltErgoLib -o src/lib/.AltErgoLib.objs/byte/altErgoLib__Parsed.cmi -c -intf src/lib/structur[...]
# File "src/lib/structures/parsed.mli", line 32, characters 17-24:
# 32 | | ConstReal of Num.num
# ^^^^^^^
# Error: Unbound module Num
# (cd _build/default && /usr/bin/ocamlc.opt -w -40 -bin-annot -g -bin-annot -I src/lib/.AltErgoLib.objs/byte -I /home/yussef/.opam/default/lib/ocplib-simplex -I /home/yussef/.opam/default/lib/seq -I /home/yussef/.opam/default/lib/stdlib-shims -I /home/yussef/.opam/default/lib/zarith -no-alias-deps -open AltErgoLib -o src/lib/.AltErgoLib.objs/byte/altErgoLib__Typed.cmi -c -intf src/lib/structure[...]
# File "src/lib/structures/typed.mli", line 58, characters 13-20:
# 58 | | Treal of Num.num (** Real constant. *)
# ^^^^^^^
# Error: Unbound module Num
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
┌─ The following actions failed
│ λ build alt-ergo-lib 2.4.2
└─
```Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2641can't parse __int1282023-05-16T06:53:28ZYurii Rashkovskiican't parse __int128<!--
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.
-->
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
Expect this to be processed:
```c
__int128 i;
```
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
Get a syntax error:
```
syntax error:
Location: between <unknown> and 1:9, before or at token: v
1 __int128 v;
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 26
- Plug-in used: WP
- OS name: macOS
- OS version: 13.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.
-->Allan BlanchardAllan Blanchard