frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T12:52:03Zhttps://git.frama-c.com/pub/frama-c/-/issues/55z3 ERROR: unknown parameter 'model_compress'2021-02-22T12:52:03Zrwmjonesz3 ERROR: unknown parameter 'model_compress'ID0002509:
**This issue was created automatically from Mantis Issue 2509. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002509:
**This issue was created automatically from Mantis Issue 2509. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002509 | Frama-C | Plug-in > wp | public | 2020-10-15 | 2020-10-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | rwmjones | **Assigned To** | correnson | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Apparently z3 dropped this parameter and replaced it with "model.compact" without bothering with backward compatibility: https://github.com/Z3Prover/z3/issues/2704#issuecomment-554489258
### Steps To Reproduce :
Use z3 4.8.9, turn on debugging.
<6.827036,call_prover>Call_provers: actual command is:
z3 -smt2 -t:10000 sat.random_seed=42
model_compress=false nlsat.randomize=false
smt.random_seed=42 -st
/tmp/why_b9efc2_zilch-T-wp_goal.smt2
ERROR: unknown parameter 'model_compress'https://git.frama-c.com/pub/frama-c/-/issues/27[GUI] Configuration is not permanent2021-02-22T13:09:20ZVeenstra[GUI] Configuration is not permanentThank 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 confirm (by adding a X...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 confirm (by adding a X in the [ ]):
- [X] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [X] the issue has not yet been reported on our [BTS](https://bts.frama-c.com);
- [X] you installed Frama-C as prescribed in the [instructions](INSTALL.md).
# Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *21.1 (Scandium)*
- Plug-in used: *WP*
- OS name: *Ubuntu 20.04.1 LTS (Focal)*
- OS version: *Linux xxxxx 5.4.0-47-generic #51-Ubuntu SMP Fri Sep 4 19:50:52 UTC 2020 x86_64 x86_64 x86_64 GNU/Linux*
*Please add specific information deemed relevant with regard to this issue.*
# Steps to reproduce the issue
## Setup
Open an almost empty file (not that the contents really matter):
```
//@ ensures \result == 0;
int main() {
return 0;
}
```
Use the following command to launch the GUI:
`frama-c-gui -wp -wp-rte -wp-status-all -wp-par 8 almost_empty.c`
Open the `WP Goals` tab to see one surely valid goal.
## Behaviour in question
Two ways to reproduce. First with the reparse button:
1. Click `Configure and run analyses`, select the `-wp` tickbox, and press `Cancel`.
2. Click `Configure and run analyses`, and note that the `-wp` tickbox is still checked even though we pressed `Cancel`. Press `Cancel` again.
3. Press `Reparse source files, and replay analyses`. The `WP Goals` tab still/again shows the surely valid goal.
4. Press `Reparse source files, and replay analyses`. The `WP Goals` tab now shows nothing.
And now with the execute button.
1. Click `Configure and run analyses`, select the `-wp` tickbox, and press `Execute`.
2. The `WP Goals` tab still/again shows the surely valid goal.
3. Click `Configure and run analyses`, and note that the `-wp` tickbox is not checked anymore.
# Expected behaviour
1. Configuring should be something you do once. This would include the commandline arguments. There should be no need to turn on the WP plugin again and again.
2. The `Cancel` button should cancel, so NOT save the changes.
3. The `Reparse source files, and replay analyses` button should not undo configuration.
4. The `Execute` button should not undo configuration.
5. There should be an additional button in the configuration dialog to save the configuration.
# Actual behaviour
1. Commandline configuration is a one time deal. Not all options are still selected after startup.
2. The `Cancel` button does not actually cancel. It saves the changes and closes the dialog. It currently behaves as a `Save and close` button.
3. The `Reparse source files, and replay analyses` button reparses, replays the analyses, and undoes configuration.
4. The `Execute` button replays the analyses, and undoes configuration.
# Fix ideas
The current work-around is to reconfigure each time I make a change to the source file (which is a little annoying).
There are two ways to fix this:
1. Have the buttons do exactly what they promise to do and nothing more.
2. Change the text of the buttons to reflect the actual behaviour.https://git.frama-c.com/pub/frama-c/-/issues/26How to install frama-c in ubuntu step by step2021-02-22T13:09:20ZbjsswaroopHow to install frama-c in ubuntu step by stephttps://git.frama-c.com/pub/frama-c/-/issues/23[wp] crash when using a type invariant in place of a predicate2021-02-22T13:09:20ZJakub Szabelewski[wp] crash when using a type invariant in place of a predicate- [X] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [X] the issue has not yet been reported on our [BTS](https://bts.frama-c.com);
- [X] you installed Frama-C as prescribed in the [instruc...- [X] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [X] the issue has not yet been reported on our [BTS](https://bts.frama-c.com);
- [X] you installed Frama-C as prescribed in the [instructions](INSTALL.md).
# Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 21.1 (Scandium)
- Plug-in used: WP
- OS name: Ubuntu
- OS version: 18.04.4 LTS
# Steps to reproduce the issue
Define a type invariant and use it in place of a predicate in an expression (in an assertion, an ensures clause, a requires clause, etc.). Run `frama-c -wp`
[type_invariant_crash.c](/uploads/ff065c967e730c80f825f1070d6e3765/type_invariant_crash.c)
# Expected behaviour
WP should report an error and probably ignore the invalid clause.
# Actual behaviour
WP prints an error message
`[wp] Failure: Logic '<invariant name>' undefined)`
and then crashes printing a backtrace (aborts due to an internal error).
# Fix ideas
NoneAllan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/21No Why3 libraries compiled for PVS2022-09-28T11:35:52ZMariano MoscatoNo Why3 libraries compiled for PVSI have been using Why3 1.3.1 (through Frama-C 21.1/WP dev) to generate verification conditions in PVS.
Today I tried to install Why3 in a different computer (both are Macs) via Opam.
```shell
$ opam install why3
The following actions ...I have been using Why3 1.3.1 (through Frama-C 21.1/WP dev) to generate verification conditions in PVS.
Today I tried to install Why3 in a different computer (both are Macs) via Opam.
```shell
$ opam install why3
The following actions will be performed:
∗ install why3 1.3.1
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><> 🐫
[why3.1.3.1] downloaded from cache at https://opam.ocaml.org/cache
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><> 🐫
∗ installed why3.1.3.1
Done.
```
The installation goes smoothly but it seems that something is missing in order to be able to use PVS.
```shell
$ why3 config --detect
Found prover Alt-Ergo version 2.3.1, OK.
Found prover PVS version 6.0, but no Why3 libraries were compiled for it
1 prover(s) added
Save config to /Users/niauser/.why3.conf
```
When I try to use it, I get
```shell
$ frama-c test.c -wp -wp-prover pvs
[kernel] Parsing test.c (with preprocessing)
[wp] User Error: Prover 'pvs' not found in why3.conf
[wp] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Plug-in wp aborted: invalid user input.
```
I've also tried `why3 config --full-config` with the same result.
```shell
$ why3 config --full-config
Found prover Alt-Ergo version 2.3.1, OK.
Found prover PVS version 6.0, but no Why3 libraries were compiled for it
1 prover(s) added
Generating strategies:
Prover Alt-Ergo 2.3.1 will be used in Auto level >= 1
Save config to /Users/niauser/.why3.conf
$ frama-c -wp-detect
[wp] Prover Alt-Ergo 2.3.1 [alt-ergo|altergo|Alt-Ergo:2.3.1]
$
```
I don’t remember performing any special step during the installation on my other Mac.
Is there something else I should do in order to be able to use Why3 with PVS?Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/20coq reports an error for a hypothesis involving 'region'2021-02-22T13:09:20ZJens Gerlachcoq reports an error for a hypothesis involving 'region'- [x] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [x] the issue has not yet been reported on our [BTS](https://bts.frama-c.com);
- [x] you installed Frama-C as prescribed in the [instruc...- [x] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [x] the issue has not yet been reported on our [BTS](https://bts.frama-c.com);
- [x] you installed Frama-C as prescribed in the [instructions](INSTALL.md).
# Contextual information
- Frama-C installation mode: *Homebrew*
- Frama-C version: *21.0 (Scandium)*
- Plug-in used: *WP*
- OS name: *macOS*
- OS version: *10.15.5*
*Please add specific information deemed relevant with regard to this issue.*
When trying to proof an obligation with coq, an error is reported w.r.t. to a **`region`** hypothesis.
# Steps to reproduce the issue
*Here is a small example (`b.c`) of a not particularly expressive function contract*
```
/*@
requires \valid_read(a + (0..n-1));
requires \valid(b + (0..n-1));
assigns b[0..n-1];
*/
void copy(int* a, unsigned int n, int* b)
{
/*@
loop assigns i, b[0..n-1];
*/
for(unsigned int i = 0; i < n; ++i)
b[i] = a[i];
}
```
When calling it with the command line
```
frama-c-gui -wp -wp-rte -wp-prover alt-ergo -wp-prover native:coq b.c
```
everything is verified by `qed or `alt-ergo`.
The problem I want to report is related to the generated `Coq` proof obligations.
When one adds a simple `intros` to **Loop assigns (file b.c, line 10)** in the Coq IDE, as in
```
Goal
forall (i_1 i : Z),
forall (t : array Z),
forall (a_1 a : addr),
let a_2 := (shift_sint32 a 0%Z) in
let a_3 := (shift_sint32 a i_1%Z) in
((i_1 < i)%Z) ->
((((region ((base a_1))%Z)) <= 0)%Z) ->
((((region ((base a))%Z)) <= 0)%Z) ->
((linked t)) ->
((is_uint32 i_1%Z)) ->
((is_uint32 i%Z)) ->
((valid_rd t ((shift_sint32 a_1 0%Z)) i%Z)) ->
((valid_rd t ((shift_sint32 a_1 i_1%Z)) 1%Z)) ->
((valid_rw t a_2 i%Z)) ->
((valid_rw t a_3 1%Z)) ->
(~((invalid t a_3 1%Z))) ->
((included a_3 1%Z a_2 i%Z)).
Proof.
intros.
Qed.
````
then the following error message is shown
```
Illegal application (Non-functional construction):
The expression "region" of type "array int" cannot be applied to the term
"base a_1" : "int"
```
I conclude from this that the generated coq obligation is syntactically not correct.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/19suspicious Coq code for ACSL lemma in Frama-C 212023-06-05T07:47:25ZJens Gerlachsuspicious Coq code for ACSL lemma in Frama-C 21Thank 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 confirm (by adding a X...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 confirm (by adding a X in the [ ]):
- [x] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [x] the issue has not yet been reported on our [BTS](https://bts.frama-c.com);
- [x] you installed Frama-C as prescribed in the [instructions](INSTALL.md).
# Contextual information
- Frama-C installation mode: opam
- Frama-C version: *21.0 (Scandium)*
- Plug-in used: *WP*
- OS name: *macOS*
- OS version: *10.15.5*
*Please add specific information deemed relevant with regard to this issue.*
# Steps to reproduce the issue
The following ACSL lemma in file `a.c`
```
/*@
lemma C_Division_Two:
\forall integer a; 0 <= a ==> 0 <= a/2 <= a;
*/
```
is verified by Alt-Ergo when calling it with
```
frama-c-gui -wp -wp-prover alt-ergo -wp-prover native:coq a.c
```
However, in Frama-C 21, the **coq representation** of the lemma looks wrong to me since it reads
```
Goal
forall (i : Z),
((0 <= i)%Z) ->
(((((Cdiv i 2)) <= i)%Z) /\ (((-1) <= i)%Z)).
```
The `-1` does not seem to be right.
In `Frama-C 20`, on the other hand, the coq representation looks like this
```
Goal
forall (i : Z),
let x := ((Cdiv i 2))%Z in
((0 <= i)%Z) ->
(((x <= i)%Z) /\ ((0 <= x)%Z)).
```
Am I missing something here?https://git.frama-c.com/pub/frama-c/-/issues/18WP: Incorrect assigns global/static handling2021-02-22T14:00:16ZAlex CoffinWP: Incorrect assigns global/static handling
View all of the following goals succeed for the following program:
```
#include <assert.h>
unsigned int number = 0;
/*@
assigns number;
ensures \valid(\result);
*/
unsigned int* a_num(void) {
++number;
return &number;
}
void...
View all of the following goals succeed for the following program:
```
#include <assert.h>
unsigned int number = 0;
/*@
assigns number;
ensures \valid(\result);
*/
unsigned int* a_num(void) {
++number;
return &number;
}
void test_a_num(void) {
unsigned int* a = a_num();
unsigned int copy = *a;
assert(copy == *a);
unsigned int* b = a_num();
assert(copy == *a);
}
int main(int argc, char** argv) {
test_a_num();
return 0;
}
```
compiled with `frama-c-gui -wp -wp-rte -wp-smoke-tests test.c`
# Expected behaviour
The second assert function call fails when run, and therefore WP should not be able to prove its preconditions.
# Actual behaviour
It claims that it has proven (incorrectly) that the assert function call will be successful. Of course the `assert` calls may be replaced with `/*@ assert */` statements instead, and it still claims that they pass.
# Fix ideas
Check handling of static/global variables with assigns?Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/17Linux Mint depext packages2021-02-22T13:09:20ZAlex CoffinLinux Mint depext packagesThe depext packages are for Linux Mint 19 Tara:
```
libgmp-dev
libgtk2.0-dev
libgtksourceview2.0-dev
libgnomecanvas2-dev
```
Possibly useful information according to depext:
`arch=x86_64, os=linux, os-distribution=linuxmint, os-family=...The depext packages are for Linux Mint 19 Tara:
```
libgmp-dev
libgtk2.0-dev
libgtksourceview2.0-dev
libgnomecanvas2-dev
```
Possibly useful information according to depext:
`arch=x86_64, os=linux, os-distribution=linuxmint, os-family=ubuntu`
I believe these packages are the same as Ubuntu's, but I haven't validated this.https://git.frama-c.com/pub/frama-c/-/issues/16[wp] unsoundness for base-offset2021-02-22T14:00:48ZLoïc Correnson[wp] unsoundness for base-offsetComputation of WP for `\offset()` in MemTyped is actually using a function `base_offset(idx)` that max index of cells in memory to their actual offset in bytes. Example:
```
struct S {
int f; // index 0, offset 0
long g; // in...Computation of WP for `\offset()` in MemTyped is actually using a function `base_offset(idx)` that max index of cells in memory to their actual offset in bytes. Example:
```
struct S {
int f; // index 0, offset 0
long g; // index 1, offset 4
int h; // index 2, offset 12
}; // size,=3, sizeof=16
```
This function is left mostly unspecified, and is required to be monotonic.
This prevent WP from computing exact offsets, but is _not_ a problem, this is just an under-specification.
Moreover, the index-offset correspondance _could_ be formally specified for each known base-address from its type (if it does not changed, as it is assumed in MemTyped).
However, this function is currently the _same_ for all base address, which is certainly incorrect and might cause unsoundness when asking WP for computing `\offset()` within variables of different types.
It **shall** be modelled as `base_offset(base, index)`.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/15Eva: Differs from C specification on pointer arithmetic2021-02-22T13:33:11ZAlex CoffinEva: Differs from C specification on pointer arithmetic
- [X] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [X] the issue has not yet been reported on our [BTS](https://bts.frama-c.com);
- [ ] you installed Frama-C as prescribed in the [instru...
- [X] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [X] the issue has not yet been reported on our [BTS](https://bts.frama-c.com);
- [ ] you installed Frama-C as prescribed in the [instructions](INSTALL.md).
I believe I have followed the third bullet, but it isn't clear if that means just making sure to properly install with Opam, or if I am expected to manually compile the newest version, and test it (which I haven't done).
# Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 20.0 (Calcium)
- Plug-in used: Eva
- OS name: Linux Mint
- OS version: Linux 4.15.0-99-generic #100~16.04.1-Ubuntu SMP
*Please add specific information deemed relevant with regard to this issue.*
# Steps to reproduce the issue
Run the following test function through the Eva plugin:
```
void test(void) {
int a[] = (const int[]) { 5 };
int* b = &a;
/*@ assert \offset(b) == 0; */
int* c = b + 1;
/*@ assert \offset(c) == 1; */
}
```
# Expected behaviour
For both of the assertions to succeed as the C89, and C99 specification taking a pointer one past the end of a C array is allowed (dereferencing that pointer is not). Therefore both checks should succeed from what I can tell.
# Actual behaviour
It claims that the second assertion fails as it is invalid:
```
[eva:alarm] src/test_array.c:6: Warning:
assertion got status invalid (stopping propagation).
```
# Fix ideas
I assume it is a bug with Eva, and not with the core Frama-C system, but I could be mistaken. **Please note** that the idea of one past an array also applies to non-array objects.
```
For the purposes of these operators. a pointer to a nonarray object behaves the same as a pointer to the first element of an array of length one with the type of the object as its element type.
```
Meaning the following should also succeed:
```
void test(void) {
int a = 5;
int* b = &a;
/*@ assert \offset(b) == 0; */
int* c = b + 1;
/*@ assert \offset(c) == 1; */
}
```David BühlerDavid Bühlerhttps://git.frama-c.com/pub/frama-c/-/issues/14Assertion failure non detected after E-ACSL with -g option2021-02-22T14:00:48ZNikolai KosmatovAssertion failure non detected after E-ACSL with -g optionAs far as I know,
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- the issue has not yet been reported on our [BTS](https://bts.frama-c.com);
- I installed Frama-C as prescribed in the [in...As far as I know,
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- the issue has not yet been reported on our [BTS](https://bts.frama-c.com);
- I installed Frama-C as prescribed in the [instructions](INSTALL.md).
# Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *20.0 (Calcium)* (as reported by `frama-c -version`)
- Plug-in used: *E-ACSL*
- OS name: *Ubuntu*
- OS version: *19.10*
# Steps to reproduce the issue
Run with:
e-acsl-gcc.sh -omonitored_test3.c -g -c test3.c ; ./a.out.e-acsl
See the attached file for a minimal example.
[test3.c](/uploads/177455ba4d592a6d26083d41cf5c6c0e/test3.c)
# Expected behaviour
The assertion failure should be detected, as it is without the -g option.
# Actual behaviour
An assertion failure not detected after the E-ACSL plugin with -g option.
It seems that the assertion cheking code is not included into the intrumented file.Julien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/13Compilation fails after E-ACSL plugin with -g option2023-06-05T07:47:25ZNikolai KosmatovCompilation fails after E-ACSL plugin with -g optionAs far as I know,
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- the issue has not yet been reported on our [BTS](https://bts.frama-c.com);
- I installed Frama-C as prescribed in the [in...As far as I know,
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- the issue has not yet been reported on our [BTS](https://bts.frama-c.com);
- I installed Frama-C as prescribed in the [instructions](INSTALL.md).
# Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *20.0 (Calcium)* (as reported by `frama-c -version`)
- Plug-in used: *E-ACSL*
- OS name: *Ubuntu*
- OS version: *19.10*
# Steps to reproduce the issue
Run with:
e-acsl-gcc.sh -omonitored_test.c -g -c test.c
See the attached file for a minimal example.
# Expected behaviour
The generation file is compiled and executed.
[test.c](/uploads/ff66f5d6118a8406a8cdab1d09686a5f/test.c)
# Actual behaviour
A compilation failure of the file generated file by the E-ACSL plugin.Julien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/56Frama-C reports “invalid ghost in extern linkage specification” while loading...2021-02-22T12:52:05Zmantis-gitlab-migrationFrama-C reports “invalid ghost in extern linkage specification” while loading filesID0002507:
**This issue was created automatically from Mantis Issue 2507. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002507:
**This issue was created automatically from Mantis Issue 2507. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002507 | Frama-C | Kernel | public | 2020-06-06 | 2020-10-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dgenin | **Assigned To** | AllanBlanchard | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | have not tried |
| **Platform** | x86 | **OS** | Ubuntu | **OS Version** | 19.10 |
| **Product Version** | Frama-C 20-Calcium | **Target Version** | - | **Fixed in Version** | - |
### Description :
As I try to load my project files Frama-C reports the following error in the Console window and stops processing
[kernel] FRAMAC_SHARE/libc/__fc_alloc_axiomatic.h:30:
invalid ghost in extern linkage specification:
Location: between lines 30 and 45, before or at token: }
28 #include "__fc_define_wchar_t.h"
29
30 __BEGIN_DECLS
31
32 /*@ ghost extern int __fc_heap_status __attribute__((FRAMA_C_MODEL)); */
33
34 /*@ axiomatic dynamic_allocation {
35 @ predicate is_allocable{L}(integer n) // Can a block of n bytes be allocated?
36 @ reads __fc_heap_status;
37 @ // The logic label L is not used, but it must be present because the
38 @ // predicate depends on the memory state
39 @ axiom never_allocable{L}:
40 @ \forall integer i;
41 @ i < 0 || i > __FC_SIZE_MAX ==> !is_allocable(i);
42 @ }
43 */
44
45 __END_DECLS
46
47 __POP_FC_STDLIB
### Steps To Reproduce :
not surehttps://git.frama-c.com/pub/frama-c/-/issues/64Unable to right-click on MacOS to drive GUI2021-02-22T12:52:17Zmantis-gitlab-migrationUnable to right-click on MacOS to drive GUIID0002506:
**This issue was created automatically from Mantis Issue 2506. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002506:
**This issue was created automatically from Mantis Issue 2506. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002506 | Frama-C | Graphical User Interface | public | 2020-06-03 | 2020-06-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | markrtuttle | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | have not tried |
| **Platform** | MacOS | **OS** | MacOS | **OS Version** | 10.14 |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | - |
### Description :
I'm unable to use the GUI on MacOS.
I have installed Frama-C on MacOS 10.14 with opam using the instructions in Section 2.2.2.2 of the tutorial https://allan-blanchard.fr/publis/frama-c-wp-tutorial-en.pdf. The only exception is that the instructions say "brew install gtk+ --with-jasper" and brew says --with-jasper is no longer supported.
I can start the gui with "frama-c-gui main.c" with the abs function from the tutorial, I can browse the abs function, but I'm unable to right click (control click) on anything in the function to start the verification. I'm following the instructions described in Section 2.2.3 of the tutorial.
Can you give me any guidance on how to proceed or how to debug?
Running frama-c from the command line works just fine.https://git.frama-c.com/pub/frama-c/-/issues/12Frama-C/WP (21 Beta) does not recognise provers2023-06-05T07:47:25ZJens GerlachFrama-C/WP (21 Beta) does not recognise proversI have install Frama-C 21 (Beta) including `Why3 1.3.1`.
I also called `why3 config --detect` but when running WP on an example I receive the following messages
```
[kernel] Parsing find.c (with preprocessing)
[rte] annotating function ...I have install Frama-C 21 (Beta) including `Why3 1.3.1`.
I also called `why3 config --detect` but when running WP on an example I receive the following messages
```
[kernel] Parsing find.c (with preprocessing)
[rte] annotating function find
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] User Error: Prover 'z3' not found in why3.conf
[wp] User Error: Prover 'cvc3' not found in why3.conf
[wp] User Error: Prover 'cvc4' not found in why3.conf
[wp] User Error: Prover 'alt-ergo' not found in why3.conf
```
Attached is my `why3.conf` file
[why3.conf](/uploads/4027dedd8b95842f6e9e37b1a39e8184/why3.conf)Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/3[wp] shall use per-behaviour assigns at call sites2021-08-05T08:49:16ZNikolai Kosmatov[wp] shall use per-behaviour assigns at call sites# Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *20.0 (Calcium)* (as reported by `frama-c -version`)
- Plug-in used: *WP*
- OS name: *Ubuntu*
- OS version: *19.10*
*Please add specific information deemed...# Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *20.0 (Calcium)* (as reported by `frama-c -version`)
- Plug-in used: *WP*
- OS name: *Ubuntu*
- OS version: *19.10*
*Please add specific information deemed relevant with regard to this issue.*
# Steps to reproduce the issue
frama-c-gui -wp behavior_assigns.c
*Please indicate here steps to follow which reproduce the issue.*
See the attached file for a minimal example. [behavior_assigns.c](/uploads/b4eaee1cce8750d4749d64794e79883c/behavior_assigns.c)
# Expected behaviour
The assigns clause of caller can be proved.
# Actual behaviour
The assigns clause of caller is not proved.
The assigns clauses specific for particular behaviors in a callee cannot be used in the caller
under specific conditions falling into such behavior(s) to prove a more restrictive assigns clause
in the caller, rather than the most general assigns taking into account all behaviors of the callee.
# Fix ideas
Obvious workarounds include additional postconditions, that make the specifications more complex and
make the proof with WP less powerful. Matching the callee's behaviors to prove stronger assigns clauses
in the caller could be helpful.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2[wp] non-provable local typing constraints in lemmas2021-05-28T09:30:55ZJens Gerlach[wp] non-provable local typing constraints in lemmas# Steps to reproduce the issue
The attached archive contains the ACSL function `Count` together with several lemma.
Also contained are
- a Makefile
- a coq proof in file `wp0.script.20` for lemma `CountBounds` that works for Frama-C 20...# Steps to reproduce the issue
The attached archive contains the ACSL function `Count` together with several lemma.
Also contained are
- a Makefile
- a coq proof in file `wp0.script.20` for lemma `CountBounds` that works for Frama-C 20
- an attempt of a coq proof in file `wp0.script.21` for lemma `CountBounds` that fails for Frama-C 21
- The files `CountBounds.v.20` and `CountBounds.v.21` contain the coq code as extracted from CoqIde
# Expected behaviour
My problem is that I am unable to adapt the coq proof that worked fro Frama-C 20 to the newer version of Frama-C.
# Actual behaviour
I suspect that this is related to changes in the generated Coq code of the VC of lemma `CountBounds`
This can be best seen when calling `diff CountBounds.v.20 CountBounds.v.21`.
```
$ diff CountBounds.v.20 CountBounds.v.21
39,40c39,40
< (((t.[ (shift_sint32 a x) ]) <> i_2)%Z) -> ((i < i_1)%Z) ->
< ((is_sint32 i_2%Z)) ->
---
> let x_1 := (t.[ (shift_sint32 a x) ])%Z in ((x_1 <> i_2)%Z) ->
> ((i < i_1)%Z) -> ((is_sint32 i_2%Z)) -> ((is_sint32 x_1)) ->
```
# Fix ideas
I think the issue is caused by the condition `((is_sint32 x_1))` for the newly introduced term `x_1 := (t.[ (shift_sint32 a x) ])%Z`. I haven't found a way to satisfy the condition `((is_sint32 x_1))` and I suspect that it is not possible.
If it is possible, then I apologise and ask for a hint.
Regards
Jens Gerlach
[CoqFramac21.tar](/uploads/e95b883ad30f134748c5a7289fa6902d/CoqFramac21.tar)Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/65WP manual: hyperlink in table of contents sometimes one off2022-09-28T12:51:12ZJens GerlachWP manual: hyperlink in table of contents sometimes one offID0002505:
**This issue was created automatically from Mantis Issue 2505. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002505:
**This issue was created automatically from Mantis Issue 2505. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002505 | Frama-C | Documentation > manuals | public | 2020-04-16 | 2020-05-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | maroneze | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 20-Calcium | **Target Version** | - | **Fixed in Version** | - |
### Description :
In the WP manual at http://frama-c.com/download/wp-manual-20.0-Calcium.pdf,
Section 2.4.8 ("Generated Proof Obligations") starts at Page 37.
However, the link in the table of contents points to Page 36.
### Additional Information :
Just a guess: You are probably using the package hyperref. I have read several times (and experienced it myself) that it is a good idea to include this packet at the end.
https://tex.stackexchange.com/questions/1863/which-packages-should-be-loaded-after-hyperref-instead-of-beforeAndre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/62development version2021-02-22T12:52:13Zmantis-gitlab-migrationdevelopment versionID0002502:
**This issue was created automatically from Mantis Issue 2502. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002502:
**This issue was created automatically from Mantis Issue 2502. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002502 | Frama-C | Plug-in > Eva | public | 2020-03-12 | 2020-06-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | puccetti2 | **Assigned To** | buhler | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | MacOS X | **OS** | - | **OS Version** | 10.15.3 |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | Frama-C 21-Scandium |
### Description :
Running EVA on the small example leads to a cash
### Additional Information :
<pre>
$ frama-c max_array2.c -val
[kernel] Parsing max_array2.c (with preprocessing)
[kernel:parser:decimal-float] max_array2.c:26: Warning:
Floating-point constant 4.6 is not represented exactly. Will use 0x1.2666666666666p2.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
[eva:alarm] max_array2.c:28: Warning:
function max_array: precondition ∀ ℤ j;
0 ≤ j < n ⇒ \valid_read(t + j) got status unknown.
[kernel] Current source was: max_array2.c:15
The full backtrace is:
Raised at file "src/plugins/value/legacy/eval_terms.ml", line 1264, characters 9-21
Called from file "src/plugins/value/legacy/eval_terms.ml", line 1030, characters 13-41
Called from file "src/plugins/value/legacy/eval_terms.ml", line 2127, characters 18-66
Called from file "src/plugins/value/legacy/eval_terms.ml", line 2308, characters 4-20
Called from file "src/plugins/value/domains/cvalue/cvalue_domain.ml", line 284, characters 10-49
Called from file "src/plugins/value/engine/transfer_logic.ml", line 663, characters 25-61
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/transfer_logic.ml", line 660, characters 10-488
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/iterator.ml", line 377, characters 8-69
Called from file "src/plugins/value/engine/iterator.ml", line 381, characters 17-61
Called from file "src/plugins/value/engine/partition.ml", line 481, characters 29-34
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/iterator.ml", line 469, characters 8-57
Called from file "src/plugins/value/engine/iterator.ml", line 556, characters 12-45
Called from file "list.ml", line 110, characters 12-15
Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 542, characters 4-31
Called from file "src/plugins/value/engine/iterator.ml", line 604, characters 6-22
Called from file "src/plugins/value/engine/iterator.ml", line 774, characters 20-39
Called from file "src/plugins/value/engine/compute_functions.ml", line 210, characters 8-45
Called from file "src/plugins/value/engine/compute_functions.ml", line 230, characters 26-36
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 307, characters 10-43
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 445, characters 22-60
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 749, characters 26-75
Called from file "src/kernel_services/abstract_interp/bottom.ml" (inlined), line 31, characters 18-21
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 745, characters 10-447
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 760, characters 24-59
Called from file "src/kernel_services/abstract_interp/bottom.ml" (inlined), line 31, characters 18-21
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 733, characters 6-1023
Called from file "src/plugins/value/engine/iterator.ml", line 277, characters 6-47
Called from file "src/plugins/value/engine/partition.ml", line 481, characters 29-34
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/iterator.ml", line 430, characters 15-71
Called from file "src/plugins/value/engine/iterator.ml", line 496, characters 18-35
Called from file "list.ml", line 92, characters 20-23
Called from file "src/plugins/value/engine/iterator.ml", line 498, characters 18-60
Called from file "src/plugins/value/engine/iterator.ml", line 545, characters 13-31
Called from file "list.ml", line 110, characters 12-15
Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 542, characters 4-31
Called from file "src/plugins/value/engine/iterator.ml", line 604, characters 6-22
Called from file "src/plugins/value/engine/iterator.ml", line 774, characters 20-39
Called from file "src/plugins/value/engine/compute_functions.ml", line 210, characters 8-45
Called from file "src/plugins/value/engine/compute_functions.ml", line 343, characters 25-75
Called from file "src/libraries/project/state_builder.ml", line 994, characters 9-13
Re-raised at file "src/libraries/project/state_builder.ml", line 1002, characters 9-18
Called from file "src/plugins/value/register.ml", line 39, characters 46-66
Called from file "queue.ml", line 121, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 792, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 822, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 229, characters 4-8
Unexpected error (File "src/plugins/value/legacy/eval_terms.ml", line 1264, characters 9-15: Assertion failed).
</pre>
### Steps To Reproduce :
frama-c-gui max_array2.c -val
## Attachments
- [max_array2.c](/uploads/c74e3cd843af6300cad5464a4aa9d6cc/max_array2.c)