frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-05-28T09:30:55Zhttps://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/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/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/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/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/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/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/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/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/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/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/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/22[Frama-Clang] Cannot refer to variables declared within a block in assertions...2021-02-22T14:00:29ZJakub Szabelewski[Frama-Clang] Cannot refer to variables declared within a block in assertions placed just before the closing brace.- [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: Frama_Clang
- OS name: Ubuntu
- OS version: 18.04.4 LTS
# Steps to reproduce the issue
Write an assertion at the end of a block:
```
int main() {
{
int x = 3;
//@ assert x == 3;
}
return 0;
}
````
# Expected behaviour
The file should be processed without errors. When using the WP plugin, a goal for the assertion should be generated.
# Actual behaviour
Frama-C reports an unknown identifier error and no goal is generated.
# Fix ideas
- The issue does not happen with C files.
- The issue disappears after inserting some code below the assertion, but before the `}`. Even a null statement (a single semicolon) is enough.[assertion_at_the_end_of_a_block.cpp](/uploads/7f69487dfe52375d056d3bbb67fa27f3/assertion_at_the_end_of_a_block.cpp)Virgile PrevostoVirgile Prevostohttps://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/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/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/28[wp] Infinite loop related to WP cache.2020-10-22T07:22:50ZVeenstra[wp] Infinite loop related to WP cache.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...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
* Extract the attached zip file: [pillow_src.zip](/uploads/37620f35fc603a9347a7748c54263389/pillow_src.zip)
* Run the following command in the root of the extracted folder: `rm -rf .frama-c/wp/cache; frama-c-gui -verbose 5 -debug 5 -wp -wp-rte -wp-out wp_out -wp-log a:wp.log -wp-timeout 10 -wp-cache update -wp-status-all -wp-par 8 -wp-model "+cast" -wp-prover coq,cvc4,alt-ergo,z3,script,tip "-cpp-extra-args=-I .frama-c-build " libImaging/FliDecode.c`
* Wait for the verification to run.
* In the file list, scroll down to `libImaging/FLIDecode.c` and open it. (maybe also click on a contract in the left source pane)
* Click `Configure and run analyses`.
* Activate the `WP` plugin.
* Click `Cancel`.
* Click `Reparse source files, and replay anayses`.
* The progress bar should appear and disappear right after.
* Check the `Console` tab and scroll down for the repeating messages. Example contents: [console_contents.txt](/uploads/7ba7ee5e95e74948b9412bd6a6605021/console_contents.txt)
* Bonus steps:
* Wait. Check out all those messages!
* Wait longer. Get bored by all the messages.
* Now click the `Console` tab contents, press `ctrl+a`, and press `ctrl+c`.
* If nothing happens wait for more text to appear and try again (work within a minute for me).
* The terminal states something like:
```
The program 'frama-c-gui' received an X Window System error.
This probably reflects a bug in the program.
The error was 'BadWindow (invalid Window parameter)'.
(Details: serial 19490411 error_code 3 request_code 18 minor_code 0)
(Note to programmers: normally, X errors are reported asynchronously;
that is, you will receive the error a while after causing it.
To debug your program, run it with the --sync command line
option to change this behavior. You can then get a meaningful
backtrace from your debugger if you break on the gdk_x_error() function.)
```
It is quite hard to reproduce this consistently, so let me know if I need to try harder to create a proper example.
# Expected behaviour
The analyses upon opening should be executed again upon hitting the replay button.
It should however be faster as most results should be cached.
# Actual behaviour
The verifier goes into an infinite loop after solving a few problems.
Not sure if the bonus steps are related to Frama-C, GTK, or my WM.
# Fix ideas
None, sorry.
I suspect the WP cache is at fault, because deleting that made the crash more consistent.
Also there might be a difference between the `Configure and run analyses` + `Execute` and the `Reparse source files, and replay analyses`, as the program only seems to crash when running the analyses using the reparse button. Also the number of goals generally differs between the two.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/30Wanted features related to Why3-Coq2020-10-02T11:00:15ZAllan BlanchardWanted features related to Why3-CoqThis is a follow up on frama-c/frama-c#956 and discussion we had with Jens on the ACSL by Example GitLab about Coq via Why3 in Frama-C.
At least two features could be added to make it easier to use (in particular for ACSL by Example):
...This is a follow up on frama-c/frama-c#956 and discussion we had with Jens on the ACSL by Example GitLab about Coq via Why3 in Frama-C.
At least two features could be added to make it easier to use (in particular for ACSL by Example):
1. drivers that are only applied to Coq (or any prover), an that can be verified,
2. user defined (restricted) context for the proof of lemmas in Coq.
### Drivers
This shall be the job of the driver. We probably need to a way to refine the why3 context *per prover*. Then, it is easy to enrich the Task generated by `ProverWhy3`, which is already « prepared » in a specific way for each prover.
Currently, the supported import directives for WP drivers are:
```
why3.file="mydir/foo.why"
why3.file="mydir/foo.why:Bar"
why3.file="mydir/foo.why:Bar:T"
why3.import="foo.Bar"
why3.import="foo.Bar:T"
```
@lcorrenson suggests to reformulate all of them into something fully understandable from why3 users:
```
[for "myProver",...] loadpath "path/to/dir";
[for "myProver",...] import foo.Bar [as T];
```
This is indeed more flexible than using our custom `meta` directives.
### Restricted context
If we have two files like:
```c
lemma Foo: // ...
lemma To_Prove: // uses Foo
```
```c
lemma Bar: // ...
lemma Foo: // ...
lemma To_Prove: // uses Foo
```
The two files generate different proof contexts for lemmas, because even if `To_Prove` only needs `Foo`, WP collects all lemmas that appear before `To_Prove`. This is why I suggest to provide the user with a way to specify precisely the proof context so that it can remain the same from a file to another.
I think we could create an ACSL extension like:
```c
/*@
lemma Foo: ...
lemma Bar: ...
lemma Proved_with_Coq: ...
lemma_dependencies Proved_with_Coq: Foo ;
*/
```
So that the user can restrict the proof context of the lemma can be as simple and predictable as possible. Note that we should check that it compatible with the `RefUsage` analysis.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/32Known WP limitation: Dynamic allocation is not supported2023-07-21T13:06:10ZBob RubbensKnown WP limitation: Dynamic allocation is not supportedHello everyone,
A colleague of mine tried to use variables as a length argument for an array:
```c
int const n = 4;
int main() {
int xs[n];
}
```
This yielded the following frama-c output:
```bash
[nix-shell:~]$ frama-c -wp program...Hello everyone,
A colleague of mine tried to use variables as a length argument for an array:
```c
int const n = 4;
int main() {
int xs[n];
}
```
This yielded the following frama-c output:
```bash
[nix-shell:~]$ frama-c -wp program.c
[kernel] Parsing program.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] program.c:4: Warning:
Cast with incompatible pointers types (source: sint32*) (target: sint8*)
[wp] program.c:4: Warning:
Cast with incompatible pointers types (source: sint8*) (target: sint32*)
[wp] 1 goal scheduled
[wp] Proved goals: 1 / 1
Qed: 1
```
Frama-c version (for completeness, I'm using the version from nixpkgs unstable):
```bash
[nix-shell:~]$ frama-c --version
21.1 (Scandium)
```
The warning seems strange, as I use only ints in this program. With my limited knowledge of C, I'd say this program does no such casting. Is this a bug or is this somehow a subtle edge case in C? Or is it benign and can it be ignored?Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/33z3 ERROR: unknown parameter 'model_compress'2021-02-22T12:52:03Zlibguestfsz3 ERROR: unknown parameter 'model_compress'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
Use z3 4.8.9, turn on debugging.
```
<6.827036,ca...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
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/34Frama-C should exit with non-zero if proving failed2020-10-15T08:53:29ZlibguestfsFrama-C should exit with non-zero if proving failed```
$ frama-c -wp -wp-rte snippets/range_size.c
[kernel] Parsing snippets/range_size.c (with preprocessing)
[rte] annotating function range_size
[wp] 4 goals scheduled
[wp] [Alt-Ergo 2.2.0] Goal typed_range_size_ensures : Timeout (Qed:2...```
$ frama-c -wp -wp-rte snippets/range_size.c
[kernel] Parsing snippets/range_size.c (with preprocessing)
[rte] annotating function range_size
[wp] 4 goals scheduled
[wp] [Alt-Ergo 2.2.0] Goal typed_range_size_ensures : Timeout (Qed:2ms) (10s)
[wp] Proved goals: 3 / 4
Qed: 1 (0.50ms-0.78ms)
Alt-Ergo 2.2.0: 2 (13ms-15ms) (80) (interrupted: 1)
```
Proving failed, but frama-c still exits with a zero exit code:
```
$ echo $?
0
```
This problem makes it harder to use frama-c from automated CI systems.https://git.frama-c.com/pub/frama-c/-/issues/35Frama-C --version lacks \n2022-12-08T16:40:58ZlibguestfsFrama-C --version lacks \nMinor but annoying detail:
```
$ frama-c --version
21.1 (Scandium)$
```Minor but annoying detail:
```
$ frama-c --version
21.1 (Scandium)$
```https://git.frama-c.com/pub/frama-c/-/issues/36non-compilable slice produced by frama-c2023-06-05T07:47:25ZIvan Postolskinon-compilable slice produced by frama-cHello, I've testing some unstructured programs to study how frama-c slicing plugin works, and I've found that the following code snippet produces a wrong (non-compilable) slice.
Program:
```C
#include <stdio.h> /* printf, scanf, ...Hello, I've testing some unstructured programs to study how frama-c slicing plugin works, and I've found that the following code snippet produces a wrong (non-compilable) slice.
Program:
```C
#include <stdio.h> /* printf, scanf, NULL */
#include <stdlib.h>
int main(int argc, char **argv) {
int x = 1;
int i = 0;
for (; i < x; i = i + 2){
switch (i){
case 6:
L:
x++;
}
}
if (x + 1 == i) {goto L;};
return x;
}
```
Frama-c Command:
`frama-c code.c -then -eva -then -slice-return main -slicing-level 1 -slicing-keep-annotations -then-on 'Slicing export' -print -ocode slice.c`
Output slice:
```C
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
int main(void)
{
int x = 1;
int i = 0;
while (i < x) {
L: case 6: x ++;
i += 2;
}
if (x + 1 == i) goto L;
return x;
}
```
I would love to understand what went wrong in the slicing analysis, and if you got any references to the algorithm/technique in which the slicer plugin is based upon also would be highly appreciated.Patrick BaudinPatrick Baudinhttps://git.frama-c.com/pub/frama-c/-/issues/40installing Frama-C 22 beta on Ubuntu 20.04 fails2021-04-13T17:49:41ZJens Gerlachinstalling Frama-C 22 beta on Ubuntu 20.04 failsThank 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: *Frama-C version* (as reported by `frama-c -version`) https://git.frama-c.com/pub/frama-c/-/wikis/downloads/frama-c-22.0-beta-Titanium.tar.gz
- Plug-in used: ~~*Plug-in used*~~
- OS name: Xubuntu
- OS version: 20.04
*Please add specific information deemed relevant with regard to this issue.*
When installing Frama-C 22 (beta) I received the following error message
```
[ERROR] The compilation of frama-c failed at "/home/jens/.opam/opam-init/hooks/sandbox.sh build
make -j7".
#=== ERROR while compiling frama-c.22.0-beta ==================================#
# context 2.0.5 | linux/x86_64 | ocaml-base-compiler.4.09.1 | pinned(https://git.frama-c.com/pub/frama-c/-/wikis/downloads/frama-c-22.0-beta-Titanium.tar.gz)
# path ~/.opam/4.09.1/.opam-switch/build/frama-c.22.0-beta
# command ~/.opam/opam-init/hooks/sandbox.sh build make -j7
# exit-code 2
# env-file ~/.opam/log/frama-c-1555-de8c6b.env
# output-file ~/.opam/log/frama-c-1555-de8c6b.out
### output ###
# [...]
# Ocamlopt src/kernel_services/ast_data/alarms.cmx
# Ocamlopt src/kernel_services/ast_data/statuses_by_call.cmx
# Ocamlopt src/plugins/gui/gui_printers.cmx
# Ocamlopt src/plugins/e-acsl/tests/print.cmx
# File "./src/plugins/wp/share/coqwp/Vlist.v", line 403, characters 8-11:
# Error:
# In nested Ltac calls to "lia" and "xlia (tactic)", last call failed.
# Tactic failure: Cannot find witness.
#
# Coqc src/plugins/wp/share/coqwp/ArcTrigo.v
# make: *** [src/plugins/wp/share/Makefile.coqwp:39: src/plugins/wp/share/coqwp/Vlist.vo] Error 1
# make: *** Waiting for unfinished jobs....
```
# 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.*
Here are my installation steps:
- `opam init --yes --comp=4.09.1`
- `opam install --yes depext`
- `opam depext --yes frama-c`
- `opam install --yes alt-ergo why3`
- `opam install --yes why3-coq`
- `opam pin add --yes https://git.frama-c.com/pub/frama-c/-/wikis/downloads/frama-c-22.0-beta-Titanium.tar.gz`
The final step failed with the message shown abovehttps://git.frama-c.com/pub/frama-c/-/issues/41Z3 and CVC4 working for Frama-C 22 (Titanium) beta after some initial problems2021-04-13T17:49:41ZJens GerlachZ3 and CVC4 working for Frama-C 22 (Titanium) beta after some initial problems**I updated the title after figuring out a solution**
- [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);
- ...**I updated the title after figuring out a solution**
- [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: *22.0-beta (Titanium)*
- Plug-in used: *WP*
- OS name: *Xubuntu*
- OS version: *Ubuntu 20.04.1 LTS*
*Please add specific information deemed relevant with regard to this issue.*
I am able to use the options `-wp-prover Alt-Ergo -wp-prover native:coq ` with *ACSL by Example*.
However when using either `-wp-prover Z3` or `-wp-prover z3` I receive the following error message.
(Note that `z3` (4.8.6) has been installed and that it has been successfully registered with `why3 config --full-config`)
```
[kernel] Parsing find.c (with preprocessing)
[rte] annotating function find
[wp] User Error: Prover 'z3' not found in why3.conf
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 25 goals scheduled
[wp] Proved goals: 25 / 25
Qed: 16 (2ms-6ms-20ms)
Alt-Ergo 2.3.3: 9 (5ms-12ms) (87)
[wp] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Plug-in wp aborted: invalid user input.
```
Similar with `CVC4` and `cvc4`.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/43Frama-C 22 beta also runs on macOS 11.0.1 Beta ("Big Sur")2021-04-15T11:37:39ZJens GerlachFrama-C 22 beta also runs on macOS 11.0.1 Beta ("Big Sur")This might be of minor interest but Titanium beta also runs on the latest beta-version
of Apple's upcoming macOS 11.0 release.
I only checked WP.
RegardsThis might be of minor interest but Titanium beta also runs on the latest beta-version
of Apple's upcoming macOS 11.0 release.
I only checked WP.
Regardshttps://git.frama-c.com/pub/frama-c/-/issues/45Crash on subdivided evaluation by inout for an unsatisfiable guard2021-02-22T13:34:22ZKarine EMCrash on subdivided evaluation by inout for an unsatisfiable guardThank 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 [ ]):
opam 2.0.5
- [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 old
[BTS](https://bts.frama-c.com) (*note: the old BTS is deprecated*);
- [x] you installed Frama-C as prescribed in the [instructions](INSTALL.md).
# Contextual information
- Frama-C installation mode: ***Opam**, Homebrew, package from distribution, from source, ...*
(for Ubuntu 20+21.1 (Scandium)): Opam 2.0.5, why3 1.3.3
- Frama-C version: *Frama-C version* (as reported by `frama-c -version`): I tried two versions 20.0 and 21.1
- Plug-in used: -eva -eva-precision 5
- OS name: Ubuntu (64 bit)
- OS version: tried two versions Ubuntu LTS 18 and 20 (LTS 18 I ran with Frama-c 20.0 and LTS 20 I ran with Frama-c 21.1)
in Oracle virtual box
*Please add specific information deemed relevant with regard to this issue.*
I got this error:
Unexpected error (File "src/plugins/value/engine/subdivided_evaluation.ml", line 238, characters 39-45: Assertion failed).
I have several programs that produce this crash. One of them is this:
```c
#include <stdint.h>
struct {
uint32_t a;
} b, c;
int32_t *d[][4][8] = {&b};
uint16_t e() {
for (;; c.a++) {
uint8_t f = 6;
d[0][c.a][c.a] == 0 && f;
}
}
void main() { e(); }
```
# Steps to reproduce the issue
frama-c -eva -slevel 100 -plevel 255 -eva-precision 5 -val-warn-undefined-pointer-comparison pointer -no-val-alloc-returns-null -warn-signed-overflow -warn-unsigned-overflow -val -no-val-show-progress -machdep x86_64 reduce_5.c
*Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.*
It is enough to run eva only:
frama-c -eva -eva-precision 5 reduce_5.c
# Expected behaviour
Not to crash
*Please explain here what is the expected behaviour.*
# Actual behaviour
**In Frama-c 20.0:**
The full backtrace is:
```
Raised at file "src/plugins/value/engine/subdivided_evaluation.ml", line 238, characters 39-51
Called from file "src/plugins/value/engine/subdivided_evaluation.ml", line 461, characters 16-67
Called from file "src/plugins/value/engine/subdivided_evaluation.ml", line 476, characters 11-22
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/subdivided_evaluation.ml", line 622, characters 21-74
.
.
.
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/engine/subdivided_evaluation.ml", line 238, characters 39-45: Assertion failed).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is 20.0 (Calcium).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
```
**In Frama-c 21.1:**
```
The full backtrace is:
Raised at file "src/plugins/value/engine/subdivided_evaluation.ml", line 234, characters 39-51
Called from file "src/plugins/value/engine/subdivided_evaluation.ml", line 455, characters 16-67
Called from file "src/plugins/value/engine/subdivided_evaluation.ml", line 470, characters 11-22
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/subdivided_evaluation.ml", line 618, characters 23-76
.
.
.
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 803, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 833, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 229, characters 4-8
Unexpected error (File "src/plugins/value/engine/subdivided_evaluation.ml", line 234, characters 39-45: Assertion failed).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is 21.1 (Scandium).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
```
*Please explain here what is the actual (faulty) behaviour.*
# Fix ideas
None.
*Please tell us if you already tried some work-arounds or have some ideas to solve this issue.*
I don't have any.David BühlerDavid Bühlerhttps://git.frama-c.com/pub/frama-c/-/issues/46Question: Dump why3 file generated by frama-c2023-06-05T07:47:25ZLeo ViezensQuestion: Dump why3 file generated by frama-cHey, <br>
if I proove a file with the wp plugin, the C code gets transpiled into WhyML, is that right? <br>
If so, is it already possible, to dump the generated WhyML into a file? <br>
Thank you for your help.Hey, <br>
if I proove a file with the wp plugin, the C code gets transpiled into WhyML, is that right? <br>
If so, is it already possible, to dump the generated WhyML into a file? <br>
Thank you for your help.https://git.frama-c.com/pub/frama-c/-/issues/47Why3 configuration for Frama-C2021-03-31T10:31:21ZAllan BlanchardWhy3 configuration for Frama-C#### Why3 configuration
We should clarify how we should produce the Why3 configuration file in the case of Frama-C. For opam installation we have added a message at the end of the installation but it is easy to ignore (or miss) this mes...#### Why3 configuration
We should clarify how we should produce the Why3 configuration file in the case of Frama-C. For opam installation we have added a message at the end of the installation but it is easy to ignore (or miss) this message. Furthermore, it is not applicable for Linux distribution packages.
One possibility for us could be to generate a Why3 configuration for Frama-C, that would always be used (unless some environment variable or option is set for example).
#### How to get a prover?
Currently, we use:
- `Why3.Whyconf.parse_filter_prover`
- `Why3.Whyconf.filter_one_prover`
However we currently can call them 3 times *for each* prover. One of them is due to the fact that we can have a composed name like "shortname,version,other_info", but for the two others we have a first call with the received name and the second for this same name but in lower case, and both are necessary (see: https://git.frama-c.com/pub/frama-c/-/issues/41#note_99186).
This shoul be simpler on both Frama-C and Why3 sides.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/48select()'s contract assigns {read,write,error}fds arguments even if they are ...2021-02-22T13:34:44Zfx-cartonselect()'s contract assigns {read,write,error}fds arguments even if they are NULL pointersMy understanding is that `select()` accepts `NULL` pointers for any of the `fd_set*` argument.
[POSIX 2008 states](https://pubs.opengroup.org/onlinepubs/9699919799.2008edition/functions/select.html) "If the `name` argument is not a null ...My understanding is that `select()` accepts `NULL` pointers for any of the `fd_set*` argument.
[POSIX 2008 states](https://pubs.opengroup.org/onlinepubs/9699919799.2008edition/functions/select.html) "If the `name` argument is not a null pointer," for name in {`readfds`, `writefds`, `errorfds`}. The manual page for select on my system also states this is allowed: "Each of the `fd_set` arguments may be specified as `NULL` if no file descriptors are to be watched for the corresponding class of events."
The `select()` contract in Frama-C's libc has an unconditional `assigns` clause for these arguments:
```
assigns *readfds, *writefds, *errorfds, *timeout, \result
```
This means that a function calling `select()` with a `NULL` pointer for any of the `fd_set*` argument, is unable to prove an `assigns` clause, unless it contains `*(fd_set*)0`.
Could the `select()` contract be updated to reflect this case?Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/50[Why3 Error] Type mismatch between ieee float.Float32.t and real2021-01-07T13:14:10ZBaptistePollien[Why3 Error] Type mismatch between ieee float.Float32.t and real# Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *22.0 (Titanium)*
- Plug-in used: *WP*
- OS name: *Ubuntu*
- OS version: *Ubuntun 20.04.1 LTS*
*Please add specific information deemed relevant with regard...# Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *22.0 (Titanium)*
- Plug-in used: *WP*
- OS name: *Ubuntu*
- OS version: *Ubuntun 20.04.1 LTS*
*Please add specific information deemed relevant with regard to this issue.*
# Steps to reproduce the issue
1. Downloads the [test_frama-c.c](/uploads/b740dd6546da025a730cb737d15ea96b/test_frama-c.c) file. This file contains 3 functions
(`test_1, test2` and `test_3`) which are functionally identical but
differ by the added asserts.
2. Run the command : `frama-c-gui -wp -wp-model real -wp-prover alt-ergo,z3-ce,cvc4-strings-ce -rte test_frama-c.c`
# Expected behaviour
All the goals should be proved.
# Actual behaviour
Only the function `test_2` is verified, but the functions `test_1` and `test_3` are not verified and I get from Why3 the error:
`[Why3 Error] Type mismatch between ieee_float.Float32.t and real`
I also tested with the `-wp-prover native:alt-ergo` and `-wp-model` with the same result.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/51Unexpected behavior when using shift and multiplication2021-02-22T14:00:34ZBaptistePollienUnexpected behavior when using shift and multiplication# Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *22.0 (Titanium)*
- Plug-in used: *WP*
- OS name: *Ubuntu*
- OS version: *Ubuntun 20.04.1 LTS*
*Please add specific information deemed relevant with regard...# Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *22.0 (Titanium)*
- Plug-in used: *WP*
- OS name: *Ubuntu*
- OS version: *Ubuntun 20.04.1 LTS*
*Please add specific information deemed relevant with regard to this issue.*
# Steps to reproduce the issue
1. Get the following C file ([issue_shift.c](/uploads/86e1cfc40c8fc092007e5e64d13a73f0/issue_shift.c)):
```C
#include <limits.h>
/*@
requires 0 <= a <= 16;
assigns \nothing;
*/
int test(int a){
int tmp = (a * a) >> 2;
//@ assert assert_tmp: 0 <= tmp <= 64;
//@ assert assert_mult: 0 <= tmp * tmp <= INT_MAX;
return a * a;
}
```
2. Run the command : `frama-c-gui -wp -wp-prover alt-ergo,z3-ce,cvc4-strings-ce -rte issue_shift.c`
# Expected behaviour
All the goals should be proved.
# Actual behaviour
The assertion `assert_mult` is not verified. Indeed, when a variable is the result of a shift, the multiplication of this variable cannot be bound.
However, if we test with:
```C
int tmp = 32;
//@ assert 0 <= tmp * tmp <= INT_MAX
```
The assertion is proved.
I tried to define the following lemma to help the provers but without success.
```C
/*@ lemma bound_mult:
\forall int a;
0 <= a <= 64
==> 0 <= a * a <= INT_MAX;
*/
```https://git.frama-c.com/pub/frama-c/-/issues/53Documentation for Report plug-in is not correct2021-03-29T11:50:09ZvarosiDocumentation for Report plug-in is not correct- [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 old
[BTS](https://bts.frama-c.com) (*note: the old BTS is deprecated*);
- [X] you insta...- [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 old
[BTS](https://bts.frama-c.com) (*note: the old BTS is deprecated*);
- [X] you installed Frama-C as prescribed in the [instructions](INSTALL.md).
# Contextual information
- Frama-C installation mode: Docker: framac/frama-c:22.0
- Frama-C version: 22.0 (Titanium)
- Plug-in used: Report
- OS name: macOS
- OS version: 11.1
# Steps to reproduce the issue
1. I open the Documentation from Frama-C official page: https://frama-c.com/download/frama-c-user-manual.pdf
2. Paragraph: **10.3.2 Rules**
3. I see a JSON there. This JSON is in curly brackets "{ ... }". And there is a "plugin" property.
4. I run:
`frama-c -report-rules report_rules.json src/main.c -wp -wp-rte -then -report -then -report-classify`
with report_rules.json file:
```
{
"plugin": "wp" ;
["unknown"]: "[a-zA-Z0-9]*_ensures"
}
```
as it is on the documentation.
4. I got:
> [report] report_rules.json:2: User Error: un-recognised token (at ";")
So first I need to change ";" for ",".
5. Then I got:
> [report] report_rules.json:3: User Error: missing name (at "[")
Then I added square brackets "[ {...} ]" gave another error:
> [report] report_rules.json:3: User Error: missing name (at "[")
5. It has problems with "plugin" property also.
6. With lots of experimentation and time lost I got to some version that works:
```
[
{"unknown": "[a-zA-Z0-9]*_ensures"}
]
```
Paragraph 10.3.2 Rules of the documentation is not correct in my point of view. It would be great if there is a tested and working example there. This will save user's time. Currently I still don't know how to structure this JSON so it work with all of its features.
# Expected behaviour
Documentation to meet actual JSON format.https://git.frama-c.com/pub/frama-c/-/issues/54An option to return error code if there are any problems with the analysis, s...2021-03-29T11:49:28ZvarosiAn option to return error code if there are any problems with the analysis, so that frama-c is easier to be used in CI/CD workflowsFeature Request
- [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 old
[BTS](https://bts.frama-c.com) (*note: the old BTS is deprecated*...Feature Request
- [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 old
[BTS](https://bts.frama-c.com) (*note: the old BTS is deprecated*);
- [X] you installed Frama-C as prescribed in the [instructions](INSTALL.md).
# Contextual information
- Frama-C installation mode: Docker: framac/frama-c:22.0
- Frama-C version: 22.0
- Plug-in used: WP and EVA
- OS name: macOS
- OS version: 11.1
# Steps to reproduce the issue
I put frama-c in a BitBucket CI pipeline. With calling directly frama-c executable. CI pipelines fail when error code returned from executables is different than 0. That way it stops you from pushing erroneous code.
# Expected behaviour
It would be great if there is an option so that frama-c executable return non-zero error code if in EVA found any error in my code, or in WP not all conditions are met.
# Actual behaviour
frama-c return 0 even if EVA show errors from the analysed code. It returns 0 if WP have found non correct behaviour also.https://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/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/57cabs2cil fails with statements in expression in a question2021-02-22T12:52:05Zmantis-gitlab-migrationcabs2cil fails with statements in expression in a questionID0002508:
**This issue was created automatically from Mantis Issue 2508. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002508:
**This issue was created automatically from Mantis Issue 2508. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002508 | Frama-C | Kernel | public | 2020-06-10 | 2020-10-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | JoGi | **Assigned To** | AllanBlanchard | **Resolution** | open |
| **Priority** | low | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Linux | **OS** | Ubuntu | **OS Version** | 18.04 LTS |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | - |
### Description :
When you have a statement in expression ( https://gcc.gnu.org/onlinedocs/gcc/Statement-Exprs.html ) in a question expression for example « 0 ? ({ printf("1"); }): ({ printf("1"); }); », the type-checker fails.
### Additional Information :
If the question expression is not a statement itself (but, for example, a right-value) then the type checking doesn't fail.
### Steps To Reproduce :
frama-c ex_stmt_exp.c -kernel-debug 1
Should do the trick.
## Attachments
- [ex_stmt_expr.c](/uploads/2d4741c184558b10f5cdc5845bea5ed8/ex_stmt_expr.c)Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/58Wp crashes on a recursive function2021-02-22T13:34:36ZFrédéric LoulergueWp crashes on a recursive functionID0002420:
**This issue was created automatically from Mantis Issue 2420. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002420:
**This issue was created automatically from Mantis Issue 2420. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002420 | Frama-C | Plug-in > wp | public | 2018-12-28 | 2020-09-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | frederic.loulergue@nau.edu | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Mac | **OS** | macOS | **OS Version** | Mojave 10.14.1 |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
frama-c -wp tmp.c give the following trace. If the recursive call in e_get is removed, no crash.
[kernel] Parsing tmp.c (with preprocessing)
[wp] Running WP plugin...
[kernel] Current source was: tmp.c:14
The full backtrace is:
Raised by primitive operation at file "src/kernel_services/ast_data/statuses_by_call.ml", line 198, characters 11-65
Called from file "list.ml", line 82, characters 20-23
Called from file "src/kernel_services/ast_data/statuses_by_call.ml", line 231, characters 6-150
Called from file "src/plugins/wp/cil2cfg.ml", line 859, characters 6-35
Called from file "src/plugins/wp/cil2cfg.ml", line 821, characters 21-51
Called from file "src/plugins/wp/cil2cfg.ml", line 890, characters 20-52
Called from file "src/plugins/wp/cil2cfg.ml", line 821, characters 21-51
Called from file "src/plugins/wp/cil2cfg.ml", line 821, characters 21-51
Called from file "src/plugins/wp/cil2cfg.ml", line 821, characters 21-51
Called from file "src/plugins/wp/cil2cfg.ml", line 890, characters 20-52
Called from file "src/plugins/wp/cil2cfg.ml", line 821, characters 21-51
Called from file "src/plugins/wp/cil2cfg.ml", line 890, characters 20-52
Called from file "src/plugins/wp/cil2cfg.ml", line 821, characters 21-51
Called from file "src/plugins/wp/cil2cfg.ml", line 1216, characters 13-47
Called from file "src/plugins/wp/cil2cfg.ml", line 1248, characters 6-30
Called from file "src/libraries/project/state_builder.ml", line 565, characters 17-22
Called from file "src/plugins/wp/cil2cfg.ml" (inlined), line 1288, characters 13-33
Called from file "src/plugins/wp/wpAnnot.ml", line 1291, characters 12-26
Called from file "src/plugins/wp/wpAnnot.ml", line 1307, characters 12-28
Called from file "src/plugins/wp/wpAnnot.ml", line 1320, characters 16-68
Called from file "src/plugins/wp/Generator.ml", line 109, characters 4-67
Called from file "map.ml", line 291, characters 20-25
Called from file "src/plugins/wp/Generator.ml", line 137, characters 4-39
Called from file "src/plugins/wp/register.ml", line 686, characters 15-40
Called from file "src/libraries/stdlib/extlib.ml", line 332, characters 14-17
Re-raised at file "src/libraries/stdlib/extlib.ml", line 332, characters 41-48
Called from file "src/libraries/stdlib/extlib.ml", line 333, characters 2-12
Called from file "src/libraries/stdlib/extlib.ml", line 333, characters 2-12
Called from file "queue.ml", line 105, 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 (Stack overflow).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is 18.0 (Argon).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
## Attachments
- [tmp.c](/uploads/db0023943b4d5bc953e110a335fcc7c7/tmp.c)https://git.frama-c.com/pub/frama-c/-/issues/59error in generated proof obligation2021-02-22T12:52:08ZJens Gerlacherror in generated proof obligationID0002501:
**This issue was created automatically from Mantis Issue 2501. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002501:
**This issue was created automatically from Mantis Issue 2501. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002501 | Frama-C | Plug-in > wp | public | 2020-03-10 | 2020-06-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | AllanBlanchard | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | Linux, macOS | **OS Version** | - |
| **Product Version** | Frama-C 20-Calcium | **Target Version** | - | **Fixed in Version** | Frama-C 21-Scandium |
### Description :
The attached file 'issue.c' contains a simplified (but still not very small) example of an issue I have within ACSL by Example.
There is lemma R_2 for the logic function R.
The definition of R uses the logic function F contained in the axiomatic block A.
When trying to verify R_2 with the command line below I obtain the message
[Why3 Error] anomaly: Failure("Can't find 'L_F' in why3 namespace")
frama-c -wp -wp-prover alt-ergo -wp-prover native:coq issue.c
[kernel] Parsing issue.c (with preprocessing)
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 2 goals scheduled
[wp] [Failed] Goal typed_lemma_R_2
Alt-Ergo 2.3.1: Failed
[Why3 Error] anomaly: Failure("Can't find 'L_F' in why3 namespace")
Coq: Unknown
[wp] [Cache] found:1
[wp] Proved goals: 1 / 2
Qed: 0
Coq: 0 (unknown: 1)
Alt-Ergo 2.3.1: 1 (10ms) (23) (cached: 1) (failed: 1)
When looking at the generated verification condition with Coq I found the following:
The generated hypothesis 'FixL_R' uses of course the function 'L_F'.
However, the necessary import clause 'Require Import A_A.' comes only AFTER the definition of 'FixL_R'.
### Additional Information :
There is a work-around by calling the helper function 'Fix' in the definition of R (see the comment in the code).
The problem also "disappears' if lemma 'R_1' is removed (but I don't have this option).
While looking at this problem, I noticed that in general coq definitions and import clauses are interspersed in the verification conditions...
## Attachments
- [issue.c](/uploads/e4b3b207592281459b4d9e552d904f4a/issue.c)https://git.frama-c.com/pub/frama-c/-/issues/60Invalid label with spaghetti code and E-ACSL full mmodel2021-02-22T13:34:28Zmantis-gitlab-migrationInvalid label with spaghetti code and E-ACSL full mmodelID0002417:
**This issue was created automatically from Mantis Issue 2417. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002417:
**This issue was created automatically from Mantis Issue 2417. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002417 | Frama-C | Plug-in > E-ACSL | public | 2018-12-12 | 2020-06-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | rmalak | **Assigned To** | bdesloges | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Linux 4.18 OCaml 4.07.0 | **OS Version** | Debian Sid |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | Frama-C 21-Scandium |
### Description :
Hi,
Don't know if this should go in E-ACSL or Kernel category.
/////////////////// spaghetti.c
int check(void)
{
return 0;
}
int main(void)
{
if( !check() || check() ) {
goto mylabel;
}
mylabel:
return 0;
}
////////////////////////
### Additional Information :
There is no problem in the following cases :
* remove -e-acsl-full-mmodel
* remove bracket
* substitution "!check()" with "check()"
* substitution "goto mylabel;" with "(void)0;"
### Steps To Reproduce :
$ frama-c spaguetti.c -e-acsl -e-acsl-full-mmodel -then-last -print -ocode spaguetti.e-acsl.c
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing spaguetti.c (with preprocessing)
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[kernel] User Error: Cannot find label for target of goto: _LOR:
__e_acsl_store_block_duplicate((void *)(& tmp_0),
(size_t)4);
__e_acsl_delete_block((void *)(& tmp_0));
goto mylabel;
## Attachments
- [spaguetti.c](/uploads/44b3cead438b8831534ab1b6ff6d6a15/spaguetti.c)https://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)https://git.frama-c.com/pub/frama-c/-/issues/63unistd.h declares __fc_ttyname but it has no definition2021-02-22T12:52:15Zmantis-gitlab-migrationunistd.h declares __fc_ttyname but it has no definitionID0002489:
**This issue was created automatically from Mantis Issue 2489. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002489:
**This issue was created automatically from Mantis Issue 2489. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002489 | Frama-C | Kernel > libc | public | 2020-01-08 | 2020-06-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | vkraus | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | opam | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 21-Scandium |
### Description :
When compiling __fc_runtime.c, I get
/usr/bin/ld: __fc_runtime.o:(.data.rel+0x0): undefined reference to `__fc_ttyname'
collect2: error: ld returned 1 exit status
### Additional Information :
gcc version 8.3.0 (debian buster)
frama-c version 20.0 (Calcium)
### Steps To Reproduce :
gcc -I$(frama-c -print-share-path)/libc -nostdinc -D__FC_MACHDEP_X86_64 -o __fc_runtime.o -c $(frama-c -print-share-path)/libc/__fc_runtime.c
(ignore the warnings)
echo "int main () { return 0; }" > main.c
gcc main.c __fc_runtime.o
You should get the error.https://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/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/66more precise error message for missing closing } of axiomatic block2021-02-22T13:35:01ZJens Gerlachmore precise error message for missing closing } of axiomatic blockID0002504:
**This issue was created automatically from Mantis Issue 2504. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002504:
**This issue was created automatically from Mantis Issue 2504. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002504 | Frama-C | Kernel | public | 2020-03-26 | 2020-05-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 20-Calcium | **Target Version** | - | **Fixed in Version** | - |
### Description :
The attached example lacks the closing '}' of the axiomatic block.
Frama-C's error message says
[kernel:annot-error] ax.c:5: Warning: unexpected token ''
In a more complex setting I have spent some time to figure out what is wrong in line 5 (where 'bar' is defined).
A more precise error message that explicitly mentions the axiomatic block would be helpful.
## Attachments
- [ax.c](/uploads/143e163e821c428dbfad9ab2b22f974b/ax.c)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/68unbound logic variable warning for local variable2021-02-22T13:35:41ZJens Gerlachunbound logic variable warning for local variableID0002500:
**This issue was created automatically from Mantis Issue 2500. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002500:
**This issue was created automatically from Mantis Issue 2500. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002500 | Frama-C | Kernel > ACSL implementation | public | 2020-03-10 | 2020-03-20 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | high | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | linux, macOS | **OS Version** | - |
| **Product Version** | Frama-C 20-Calcium | **Target Version** | - | **Fixed in Version** | - |
### Description :
When processing the following lines
/*@
requires 0 < n;
requires \valid(a + (0..n-1));
*/
void foo(int* a, int n)
{
int m = 0;
//@ assert a[m] == \at(a[m],Pre);
}
with 'frama-c -wp label_pointer.c ', I obtain the following error message for the assertion.
[kernel] Parsing label_pointer.c (with preprocessing)
[kernel:annot-error] label_pointer.c:9: Warning:
unbound logic variable m. Ignoring code annotation
[kernel] User Error: warning annot-error treated as fatal error.
[kernel] User Error: stopping on file "label_pointer.c" that has errors. Add '-kernel-msg-key pp'
for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
To me this looks like a bug or am I missing something crucial here?
(The message does NOT appear when 'Pre' is replaced by 'Here'.)
## Attachments
- [label_pointer.c](/uploads/ef51b56f81d231eaedc46a0d2aea401e/label_pointer.c)https://git.frama-c.com/pub/frama-c/-/issues/70munmap() breaks WP analysis2023-07-21T13:28:43Zmantis-gitlab-migrationmunmap() breaks WP analysisID0002498:
**This issue was created automatically from Mantis Issue 2498. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002498:
**This issue was created automatically from Mantis Issue 2498. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002498 | Frama-C | Plug-in > wp | public | 2020-02-10 | 2020-02-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | adbq | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | amd64 | **OS** | Linux Debian | **OS Version** | Buster (10) |
| **Product Version** | Frama-C 20-Calcium | **Target Version** | - | **Fixed in Version** | - |
### Description :
When using unmap() glib function, WP stops analysis with a fatal error "User Error: Invalid infinite range p_1+(0..)".
### Steps To Reproduce :
make frama-c, with appended code snippet.
## Attachments
- [Makefile](/uploads/b3d3d3c48e97cef222db70c65ef942aa/Makefile)
- [test4.c](/uploads/0aa351f38d2e0b1d6c56ae148a58164a/test4.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/71Outdated -rte-all option in RTE manual2021-02-22T12:52:26Zmantis-gitlab-migrationOutdated -rte-all option in RTE manualID0002418:
**This issue was created automatically from Mantis Issue 2418. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002418:
**This issue was created automatically from Mantis Issue 2418. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002418 | Frama-C | Documentation > manuals | public | 2018-12-14 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jaseg | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | low | **Severity** | trivial | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 18-Argon | **Target Version** | Frama-C 20-Calcium | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
The frama-c v18.0 RTE manual[1] linked from the RTE website[0] in ch. 3 claims RTE has options -rte-all and -rte-no-all that the actual command line tool does not seem to recognize. I guess this is just outdated info. Note that the option is also mentioned in the text which I guess would have to be updated as well.
Thanks for the great work,
jaseg
[0] https://frama-c.com/rte.html
[1] https://frama-c.com/download/frama-c-rte-manual.pdf
### Steps To Reproduce :
(this is one of the example command lines from the manual)
> dev~/r/l/src <3 frama-c -rte -rte-select f,g -rte-all -rte-mem
> [kernel] User Error: option `-rte-all' is unknown.
> use `frama-c -help' for more information.
> [kernel] Frama-C aborted: invalid user input.
> dev~/r/l/src <3 frama-c -v
> 18.0 (Argon)https://git.frama-c.com/pub/frama-c/-/issues/72opam fails to install frama-c2021-02-22T12:52:32Zmantis-gitlab-migrationopam fails to install frama-cID0002468:
**This issue was created automatically from Mantis Issue 2468. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002468:
**This issue was created automatically from Mantis Issue 2468. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002468 | Frama-C | Opam | public | 2019-07-26 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | abutterfield | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Macbook Pro | **OS** | OS X Mojave | **OS Version** | 10.14.5 |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
~> opam install frama-c
The following dependencies couldn't be met:
- frama-c → frama-c-base → ocaml < 4.06
base of this switch (use `--unlock-base' to force)
- frama-c → ocaml < 4.08.0
base of this switch (use `--unlock-base' to force)
No solution found, exiting
### Steps To Reproduce :
Followed instructions on https://frama-c.com/install-19.0-Potassium.html#installing-frama-c-on-macos
after doing update/upgraders for both brew and opam - opam and Ocaml already installed.
Attached file shows complete OS X Terminal transcript
## Attachments
- [2019-07-26-frama-c-install-fail.txt](/uploads/bb0f2fb68238e4c4f015d85ff29bf381/2019-07-26-frama-c-install-fail.txt)
- [2019-07-26-retry-after-switch-4-06-1.txt](/uploads/6bbe1ed0e8dd2a9c8eaa9fd01def1538/2019-07-26-retry-after-switch-4-06-1.txt)
- [2019-07-26-retry-after-caveats.txt](/uploads/92013a1d30bfb430a9d76f2ed50e289c/2019-07-26-retry-after-caveats.txt)https://git.frama-c.com/pub/frama-c/-/issues/73Bytecode only compilation fails when linking to stdlib2021-02-22T12:52:37Zmantis-gitlab-migrationBytecode only compilation fails when linking to stdlibID0002378:
**This issue was created automatically from Mantis Issue 2378. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002378:
**This issue was created automatically from Mantis Issue 2378. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002378 | Frama-C | ptests | public | 2018-06-18 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | madroach | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | bytecode-only | **OS** | OpenBSD | **OS Version** | 6.3 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
Compiling bytecode only fails with this error:
ocamlfind ocamlc -I ptests -dtypes -vmthread -g -o bin/ptests.byte unix.cma threads.cma str.cma dynlink.cma ptests/ptests_config.ml ptests/ptests.ml
File "ptests/ptests.ml", line 1:
Error: Required module `Uchar' is unavailable
### Steps To Reproduce :
Compile OCaml >=4.03 without optimizing compilers.
Use this compiler to build frama-c
## Attachments
- [patch-configure_in](/uploads/bf282dbc3c08065b0ff2a13f4fb83464/patch-configure_in)
- [patch-Makefile](/uploads/8465ce62432109e8765f692552e038a5/patch-Makefile)
- [patch-configure_in_2](/uploads/0fc49374e72889fac876d95a3de5dd71/patch-configure_in_2)
- [patch-Makefile_2](/uploads/568208604221bf782f915ed5f2ccf1b0/patch-Makefile_2)
- [patch-Makefile_3](/uploads/c238c03a2a9a0c54e559a994b4448f87/patch-Makefile_3)https://git.frama-c.com/pub/frama-c/-/issues/75Failure to detect qed libraries when running wp2021-02-22T12:52:46Zmantis-gitlab-migrationFailure to detect qed libraries when running wpID0002389:
**This issue was created automatically from Mantis Issue 2389. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002389:
**This issue was created automatically from Mantis Issue 2389. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002389 | Frama-C | Plug-in > wp | public | 2018-07-17 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | timourf | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Linux | **OS Version** | - |
| **Product Version** | - | **Target Version** | Frama-C 17-Chlorine | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
This is not a problem with this particular code, but I will include it anyways for the sake of completeness and reproducibility.
With the following C code "average.c"
=============================================
/*@ ensures \result == \abs(x); */
double abs(double x) {
if (x >= 0) return x;
else return (-x);
}
/*@ requires 0x1p-967 <= C <= 0x1p970;
@ ensures \result == \round_double(\NearestEven, (x+y)/2);
@ */
double average(double C, double x, double y) {
if (C <= abs(x)) return x/2+y/2;
else return (x+y)/2;
}
=============================================
running the command
>frama-c -wp -wp-model +float -wp-prover "why3:coq" -wp-print average.c
produces the following output
=============================================
[kernel] Parsing average.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] average.c:9: Warning:
Builtin \NearestEven not defined
[wp] 2 goals scheduled
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /home/timourf/.opam/default/share/frama-c/wp/why3/why3.conf
Fatal error while loading driver file '/home/timourf/.opam/default/share/why3/drivers/coq.drv':
File "/home/timourf/.opam/default/share/frama-c/wp/why3/coq.drv", line 24, characters 7-14:
Library file not found: qed
------------------------------------------------------------
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /home/timourf/.opam/default/share/frama-c/wp/why3/why3.conf
Fatal error while loading driver file '/home/timourf/.opam/default/share/why3/drivers/coq.drv':
File "/home/timourf/.opam/default/share/frama-c/wp/why3/coq.drv", line 24, characters 7-14:
Library file not found: qed
... (less relevant output) ...
=============================================
the line referenced in coq.drv is
"theory qed.Qed meta "realized_theory" "qed.Qed", "Qed" end
### Additional Information :
Product Version: Frama-C-Chlorine-20180501 **not an option in reporting tool**
I reported this here because the error seems to be with the configurations files generated by frama-c in the frama-c/wp directory, but I can't be sure that the problem isn't with why3 itself. I'm still very new to using these tools.
Note: the "Builtin \NearestEven not defined" seems to be a separate bug, referenced here: https://lists.gforge.inria.fr/pipermail/frama-c-discuss/2016-July/005117.html
### Steps To Reproduce :
Installed the following via OPAM
coq 8.8.0 (because 8.8.1+ reports not supported by why3)
why3-coq 1.0.0
frama-c-chlorine-20180501
error persists after uninstalling and re-installing all of the above
## Attachments
- [coq.drv](/uploads/7d46c6d1e6ee9a9a0ee6e60e0dbb72f7/coq.drv)
- [wp.driver](/uploads/9801629381f7c222b5f698622a1d6551/wp.driver)https://git.frama-c.com/pub/frama-c/-/issues/76conditional input annotations result in why3 type errors2021-02-22T12:52:48Zmantis-gitlab-migrationconditional input annotations result in why3 type errorsID0002394:
**This issue was created automatically from Mantis Issue 2394. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002394:
**This issue was created automatically from Mantis Issue 2394. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002394 | Frama-C | Plug-in > wp | public | 2018-08-23 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | timourf | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | GNU/Linux | **OS Version** | Debian 9 |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
I am trying to put conditions on my function specification that specify return values conditioned on special input values. A minimal example is as follows:
/*@ requires 0 <= t <= 1;
@ ensures t == 1.f ==> \result == b;
@ assigns \nothing
*/
float interpolate(float a, float b, float t) { ... }
Why3 (stderr) reports:
===================================================================================
File "/tmp/wp0a3ed9.dir/typed/interpolate_Why3_ide.why", line 20, characters 11-26:
This term has type real -> real, but is expected to have type real
===================================================================================
The "problem line" is "ensures t == 1.f ==> \result == b;"
This seems to be a problem between wp and why3. The error persists with every external prover I use with why3. The list of provers I've tried is [Z3,CVC3,CVC4,Alt-Ergo,Gappa], and the only exception is why3:coq (see issue 0002389).
### Additional Information :
why3 0.88.3
frama-c chlorine 20180502
### Steps To Reproduce :
see attached file "buggy.c"
run:
> frama-c -wp -wp-prover "why3:XXX" buggy.c
where XXX is any prover installed with why3
## Attachments
- [buggy.c](/uploads/323bd028ec39d43d549eae1d88957797/buggy.c)https://git.frama-c.com/pub/frama-c/-/issues/77suggest to provide results of commandl-line "-wp-prop" evaluation in a file i...2021-02-22T12:52:49ZJens Gerlachsuggest to provide results of commandl-line "-wp-prop" evaluation in a file in the wp-out directoryID0002371:
**This issue was created automatically from Mantis Issue 2371. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002371:
**This issue was created automatically from Mantis Issue 2371. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002371 | Frama-C | Plug-in > wp | public | 2018-03-22 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | none | **Severity** | feature | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.10 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
I ran
"frama-c -wp -wp-out without_lemma -wp-gen -wp-prover why3 -wp-prop=-@lemma aaa.c"
and then
"frama-c -wp -wp-out with_lemma -wp-gen -wp-prover why3 aaa.c"
on the attached file.
After that, "diff -r without_lemma with_lemma" reports no difference between both generated directories.
It is clear that Frama-C needs to generate why3 code for the lemma in both cases, since it might be *used* in some proof.
However, as a consequence, there is no information in the generated directories about which lemmas should be proven. It would be nice if in the long run such information could be provided, e.g. in a separate file.
### Additional Information :
Our application scenario is the following:
We run (one of) the above command(s) on a local computer to generate why3 files; then we transfer them to a more powerful remote computer, and run the provers there. On the remote computer, we would like to have the list of lemmas-to-be-proven available.
Note that arbitrarily complex combinations of "-wp-prop" could exclude some lemmas from being proven and include others. Therefore, we don't want to perform the evaluation of command-line args "-wp-prop=..." ourselves again (this is difficult, anyway, cf. #2285).
## Attachments
- [aaa.c](/uploads/ef6c959b3687621110ddcbd77ab2b906/aaa.c)https://git.frama-c.com/pub/frama-c/-/issues/78ill-typed alt-ergo proof obligation2021-02-22T14:01:05ZVirgile Prevostoill-typed alt-ergo proof obligationID0001484:
**This issue was created automatically from Mantis Issue 1484. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001484:
**This issue was created automatically from Mantis Issue 1484. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001484 | Frama-C | Plug-in > wp | public | 2013-09-25 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
Using WP with RTE enabled on the attached file results in proof obligations rejected as ill-typed by Alt-Ergo.
### Additional Information :
Without rte, everything is fine. With RTE, the resulting proof obligation is the following:
forall x_0 : int.
let x_1 = to_sint32(neqb(0, x_0)) : int in
let x_2 = to_uint8(x_0 - (ite((eqb(0, x_0)), 0, 1))) : int in
is_uint8(x_0) ->
(x_1 <= (2147483648 + x_0)) ->
(x_0 <= (2147483647 + x_1)) ->
is_uint8(x_2) ->
(x_2 <= x_0)
the definition of x_1 is lacking an ite(_,0,1) conversion, as shown in the definition of x_2. x_1 does not appear in the PO without RTE, as it is only used in the (x<=2147483648 + x_0) and x_0 <= (2147483647 + x_1) hypotheses reflecting the RTE-generated hypotheses.
Note that writing the RTE-generated hypotheses in the code (and launching WP without -wp-rte) results in warning cast from (boolean) not yet implemented, and degenerated goals.
### Steps To Reproduce :
frama-c -wp -wp-rte t.c
## Attachments
- [t.c](/uploads/085bb97c670f033ea923101dfd6b3a57/t.c)https://git.frama-c.com/pub/frama-c/-/issues/80known, but inferrable, yet not inferred, property not given as precodition to...2021-02-22T12:52:55ZJochen Burghardtknown, but inferrable, yet not inferred, property not given as precodition to proversID0002330:
**This issue was created automatically from Mantis Issue 2330. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002330:
**This issue was created automatically from Mantis Issue 2330. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002330 | Frama-C | Plug-in > wp | public | 2017-10-26 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Phosphorus-20170501 | **OS** | - | **OS Version** | xubuntu 17.04 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
Running "frama-c -wp foo.c -wp-out wp-out -wp-prop=D" on the attached program fails to prove the property D, although it follows immediately from A and C.
A look at the generated file "foo_assert_D_Alt-Ergo.mlw" reveals that the condition "y<=15" from C is not given to Alt-Ergo, while "0<=y" is.
If the former is inserted into the mlw file, Alt-Ergo proves the goal without problems.
Probably, "y<=15" is considered a trivial consequence of "y==(x&0xf)" by Qed; however, it shouldn't, since (e.g.) Alt-Ergo is unable to to infer this: goal C cannot be proven by Alt-Ergo.
### Steps To Reproduce :
Name translation c -> mlw for convenience:
x -> i
y -> x
z -> x_1
## Attachments
- [foo.c](/uploads/2114c61520580b96d2b67fca503e569d/foo.c)https://git.frama-c.com/pub/frama-c/-/issues/81Error in coq code generated by wp2021-02-22T13:34:31Zmantis-gitlab-migrationError in coq code generated by wpID0001806:
**This issue was created automatically from Mantis Issue 1806. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001806:
**This issue was created automatically from Mantis Issue 1806. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001806 | Frama-C | Plug-in > wp | public | 2014-06-12 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | davyg | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
There is a typing error with some code generated by wp.
For example this script :
_Bool g()
{
return 0;
}
//@ensures x == (!!\result == !!x);
_Bool f(_Bool x)
{
return g();
}
When using prover coq from wp generates :
Goal
forall (f_0 x_0 : Z),
((is_uint32 f_0%Z)) ->
((is_uint32 x_0%Z)) ->
((((Zneq_bool 0 x_0))
= ((Zeq_bool ((Zneq_bool 0 f_0)) ((Zneq_bool 0 x_0)))))%Z)%Z.
Proof.
(* auto with zarith. *)
Qed.
which produce this coq error on "Zneq_bool 0 f_0":
Error: In environment
f_0 : int
x_0 : int
The term "Zneq_bool 0 f_0" has type "bool" while it is expected to have type
"int".
### Steps To Reproduce :
Just use the C example with wp/coq as prover (with the gui for example because else wp consider that the script fails and does not print the error)https://git.frama-c.com/pub/frama-c/-/issues/82\false provable from recursive logic definition2021-02-22T14:01:06ZJochen Burghardt\false provable from recursive logic definitionID0002338:
**This issue was created automatically from Mantis Issue 2338. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002338:
**This issue was created automatically from Mantis Issue 2338. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002338 | Frama-C | Plug-in > wp | public | 2017-12-18 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | Ubuntu 17.04 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
Running "frama-c -wp foo.c -wp-prover alt-ergo -wp-prover eprover" on the attached file proves all goals, including a lemma "Check" which just says "\false", from nothing but a recursive definition of a logic int function.
The latter is well-founded since its only recursive call uses a parameter value n==0 which immediately employs the base case.
The problem disappears
(1) when "integer" is used as result type and as 3rd parameter type,
(2) when "a[]" is omitted,
(3) when lemma "Alpha" is renamed to a name lexicographically after "Check", or
(4) when "cvc3" or "cvc4-15" is used instead of "eprover".
The problem remains, however, when "z3" is used.
## Attachments
- [foo.c](/uploads/340c077780845d501a0ff97285b34e30/foo.c)
- [diff.txt](/uploads/2fe9c477a8a70ef0a92fbd1b0e09d964/diff.txt)
- [eprover.input](/uploads/ad8ebe320b201413c34ff6998234e1e0/eprover.input)https://git.frama-c.com/pub/frama-c/-/issues/83wrong test path given in Compiling from source - Quick Start"2021-02-22T13:07:21Zmantis-gitlab-migrationwrong test path given in Compiling from source - Quick Start"ID0002469:
**This issue was created automatically from Mantis Issue 2469. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002469:
**This issue was created automatically from Mantis Issue 2469. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002469 | Frama-C | Documentation > website | public | 2019-08-07 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | abutterfield | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
In
https://frama-c.com/install-19.0-Potassium.html#compiling-from-source
step 6 suggests a test involving "tests/misc/CruiseControl*.c".
In the Potassium distribution, that needs to be "tests/value/CruiseControl*.c".
I installed from source as a non-superuser, which works
### Steps To Reproduce :
Follow the Quick Start instructions - or simple look at the contents of tests/misc and tests/value in the source distribution.https://git.frama-c.com/pub/frama-c/-/issues/84Can't build from source using opam2021-02-22T13:34:34Zmantis-gitlab-migrationCan't build from source using opamID0002466:
**This issue was created automatically from Mantis Issue 2466. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002466:
**This issue was created automatically from Mantis Issue 2466. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002466 | Frama-C | Opam | public | 2019-07-25 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sshankar | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | block | **Reproducibility** | always |
| **Platform** | - | **OS** | Ubuntu | **OS Version** | 18.04 |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
Argon doesn't build, presumably due to config related bugs in opam/opam. I am guessing its due to inconsistency with opam semantics of "|" (used under conflicts in $FRAMAC/opam/opam).
### Additional Information :
If possible, I'd appreciate a patch I could do locally instead of waiting for the official fix. Thanks.
### Steps To Reproduce :
When I try to install it using the prescribed method
opam init
eval `opam config env`
opam install depext
opam depext frama-c
opam install --deps-only frama-c
cd ~/src (where argon is)
opam pin add --kind=path frama-c frama-c-18.0-Argon/
I get the following error (and no frama-c):
frama-c needs to be installed.
[ERROR] why3-base (< 0.88 | >= 1.0.0) & coq < 8.4.6 & lablgtk < 2.18.2 &
frama-c-e-acsl & frama-c-base is not a valid conjunction
[NOTE] Pinning command successful, but your installed packages may be out of
sync.https://git.frama-c.com/pub/frama-c/-/issues/85Potassium does not install on the given Mac version from opam2021-02-22T13:55:37ZDavid CokPotassium does not install on the given Mac version from opamID0002464:
**This issue was created automatically from Mantis Issue 2464. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002464:
**This issue was created automatically from Mantis Issue 2464. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002464 | Frama-C | Opam | public | 2019-07-11 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | davidcok | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | high | **Severity** | major | **Reproducibility** | always |
| **Platform** | MAC | **OS** | OSX | **OS Version** | 10.12.6 (SIERRA) |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
opam install frama-c
on Mac wants to downgrade alt-ergo to version 2.1.0 (instead of 2.3.0)
but 2.1.0 fails to build with the error
# Error: Unbound module Zip
# make: *** [lib/util/myZip.cmx] Error 2
### Steps To Reproduce :
opam install frama-chttps://git.frama-c.com/pub/frama-c/-/issues/86WP warning not clear2021-02-22T12:53:10ZJens GerlachWP warning not clearID0002482:
**This issue was created automatically from Mantis Issue 2482. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002482:
**This issue was created automatically from Mantis Issue 2482. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002482 | Frama-C | Plug-in > wp | public | 2019-10-22 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Linux, macOS | **OS Version** | - |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
When I run
frama-c -wp -wp-rte -wp-model Typed f.c
on the attached file, I obtain the warning
[wp] Warning: Memory model hypotheses for function 'f':
/*@ behavior typed: requires \separated(p+(..),a); */
void f(int *a);
However, when I add this requirement by removing the corresponding comment in the contract,
then the warning still occurs.
What can I do to make this warning disappear?
## Attachments
- [f.c](/uploads/bec418c0cc734cf361d31b115a8835b1/f.c)https://git.frama-c.com/pub/frama-c/-/issues/87frama-c/wp generates invalid why32021-02-22T13:35:23Zmantis-gitlab-migrationframa-c/wp generates invalid why3ID0002471:
**This issue was created automatically from Mantis Issue 2471. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002471:
**This issue was created automatically from Mantis Issue 2471. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002471 | Frama-C | Plug-in > wp | public | 2019-08-13 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | abakst | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | macOS | **OS Version** | 10.14 |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
There appears to be an issue with some of the `why3` files that get generated from user axiomatic definitions. I've installed `frama-c` using the `nix-pkgs` on the master branch, and hence have version `19.0`, and `why3` version `1.2.0`.
```c
/*@ axiomatic maps { type model_digit = octet | sextet;
logic integer foo(model_digit i);
}
*/
int foo() {
//@assert \forall int i; i == foo(octet);
return 0;
}
```
Given the (silly) program above in `simple.c`, I get the following behavior
```bash
$ frama-c -wp -wp-prover z3-ce simple.c
[kernel] Parsing simple.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] WPOUT/typed/A_maps.why:13: User Error: why3 syntax error
[wp] [z3-ce] Goal typed_foo_assert : Failed
why3 syntax error
[wp] Proved goals: 0 / 1
Why3 (z3-ce): 0 (failed: 1)
[wp] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Plug-in wp aborted: invalid user input.
```
The A_maps.why file contains:
```
(* ---------------------------------------------------------- *)
(* --- Axiomatic 'maps' --- *)
(* ---------------------------------------------------------- *)
theory A_maps
use bool.Bool
use int.Int
use int.ComputerDivision
use real.RealInfix
use Qed.Qed
use int.Abs as IAbs
use map.Map
type a_model_digit | c_octet | c_sextet
function l_foo a_model_digit : int
end
```
The error seems to be on the line (I'd imagine there should be an '=' but I am not a why3 user)
```
type a_model_digit | c_octet | c_sextet
```
### Steps To Reproduce :
Copy the C source into a new file, simple.c, and attempt to run the command:
frama-c -wp -wp-prover z3-ce simple.c
## Attachments
- [bug.c](/uploads/8df040c765825ec3d66d84e371757e44/bug.c)https://git.frama-c.com/pub/frama-c/-/issues/88explicitly mention operator precedences when referring to Fig.2.1 "Grammar of...2021-02-22T12:53:14ZJochen Burghardtexplicitly mention operator precedences when referring to Fig.2.1 "Grammar of terms" in the acsl-implementation manualID0002200:
**This issue was created automatically from Mantis Issue 2200. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002200:
**This issue was created automatically from Mantis Issue 2200. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002200 | Frama-C | Documentation > ACSL | public | 2016-01-04 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | text | **Reproducibility** | N/A |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
Running "frama-c xac2.c" on the attached program results in an error message:
xac.c:20:[kernel] user error: unexpected token ':'
The message disappears if the named subterm "A:1" is put in parantheses.
However, from Fig.2.1 "Grammar of terms" (p.16) in the manual "acsl-implementation-Sodium-20150201.pdf" the derivation
term -----> unary-op term -----> unary-op id : term -----> - A : 1
seems to be perfectly valid.
I suggest that, when referring to Fig.2.1, a note should be added that the grammar should be taken cum grano salis rather than literally, and that operator precedences (probably those shown in Fig.2.4, p.19) apply that aren't reflected in Fig.2.1. A similar note could be added for Fig.2.2 "Grammar of predicates", and maybe also at later places in the manual.
## Attachments
- [xac2.c](/uploads/94352314f819785ca8f8423b18c9805b/xac2.c)https://git.frama-c.com/pub/frama-c/-/issues/90formatting problem in acsl-implementation-18.0-Argon.pdf2021-02-22T13:42:53Zmantis-gitlab-migrationformatting problem in acsl-implementation-18.0-Argon.pdfID0002450:
**This issue was created automatically from Mantis Issue 2450. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002450:
**This issue was created automatically from Mantis Issue 2450. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002450 | Frama-C | Documentation > manuals | public | 2019-06-09 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kiniry | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
See page 45 of the manual. There is a formatting error pushing at least a paragraph about statement contracts off the lower right hand corner of the page.https://git.frama-c.com/pub/frama-c/-/issues/91quantifiers over logic types do not restrict to valid instances2021-04-15T09:37:11Zmantis-gitlab-migrationquantifiers over logic types do not restrict to valid instancesID0002497:
**This issue was created automatically from Mantis Issue 2497. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002497:
**This issue was created automatically from Mantis Issue 2497. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002497 | Frama-C | Plug-in > wp | public | 2020-01-30 | 2020-02-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | amosr | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 20-Calcium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi,
When I quantify over an unsigned char, the resulting formula uses the is_uint8 predicate to ensure that it only considers valid uint8s. However, if I define a logic type that contains an unsigned char, there is no corresponding is_ predicate for the logic type:
> //@ type logic_type_with_u8 = value(unsigned char);
This type is represented in the generated formula as an unbounded int rather than an unsigned char. This means that quantifying over the logic type includes more values than are allowed - for example, `\forall logic_type_with_u8 l` has to prove that the predicate is true even for values that won't fit in a u8.
As a concrete example, I expect the following to hold, but it does not:
> lemma u8_is_valid: \forall logic_type_with_u8 n; \exists unsigned char u; n == value(u);
Thanks,
Amos
### Additional Information :
PS. I could not test on the latest version from git - how do I get (read-only) access to the git repository?
### Steps To Reproduce :
Download file logic_type_is_valid.c and run with WP:
> frama-c -wp logic_type_is_valid.c
The lemma in this file should hold, but does not.
## Attachments
- [logic_type_is_valid.c](/uploads/ec550b694fa472b8bd9d08dc35a76d72/logic_type_is_valid.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/97incompatibilité de libc/math.h ??2021-02-22T12:53:24ZNicky Williamsincompatibilité de libc/math.h ??ID0002491:
**This issue was created automatically from Mantis Issue 2491. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002491:
**This issue was created automatically from Mantis Issue 2491. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002491 | Frama-C | Plug-in > clang | public | 2020-01-22 | 2020-01-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | nicky | **Assigned To** | fvedrine | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
l'instruction
#include <math.h>
provoque les messages d'erreur:
/usr/local/share/frama-c/libc/math.h:134:40: unknown identifier '\is_infinite'
/usr/local/share/frama-c/libc/math.h:148:40: unknown identifier '\is_infinite'
/usr/local/share/frama-c/libc/math.h:158:38: No suitable candidate found for function \is_finite.
/usr/local/share/frama-c/libc/math.h:176:40: unknown identifier '\is_infinite'
/usr/local/share/frama-c/libc/math.h:190:40: unknown identifier '\is_infinite'
/usr/local/share/frama-c/libc/math.h:200:38: No suitable candidate found for function \is_finite.
/usr/local/share/frama-c/libc/math.h:225:39: No suitable candidate found for function \is_finite.
/usr/local/share/frama-c/libc/math.h:233:45: calls to C++ functions/methods like 'atan2' are not allowed in ACSL++
/usr/local/share/frama-c/libc/math.h:240:52: calls to C++ functions/methods like 'atan2f' are not allowed in ACSL++
/usr/local/share/frama-c/libc/math.h:262:39: No suitable candidate found for function \is_finite.
/usr/local/share/frama-c/libc/math.h:283:39: No suitable candidate found for function \is_finite.
/usr/local/share/frama-c/libc/math.h:301:48: unknown identifier '\is_plus_infinity'
/usr/local/share/frama-c/libc/math.h:319:48: unknown identifier '\is_plus_infinity'
/usr/local/share/frama-c/libc/math.h:333:38: No suitable candidate found for function \is_finite.
/usr/local/share/frama-c/libc/math.h:420:39: No suitable candidate found for function \is_finite.
/usr/local/share/frama-c/libc/math.h:441:39: No suitable candidate found for function \is_finite.
/usr/local/share/frama-c/libc/math.h:466:39: No suitable candidate found for function \is_finite.
/usr/local/share/frama-c/libc/math.h:509:39: No suitable candidate found for function \is_finite.
/usr/local/share/frama-c/libc/math.h:522:46: calls to C++ functions/methods like 'pow' are not allowed in ACSL++
/usr/local/share/frama-c/libc/math.h:529:47: calls to C++ functions/methods like 'powf' are not allowed in ACSL++
/usr/local/share/frama-c/libc/math.h:553:39: No suitable candidate found for function \is_finite.
/usr/local/share/frama-c/libc/math.h:590:39: No suitable candidate found for function \is_finite.
/usr/local/share/frama-c/libc/math.h:608:39: No suitable candidate found for function \is_finite.
/usr/local/share/frama-c/libc/math.h:642:39: No suitable candidate found for function \is_finite.
/usr/local/share/frama-c/libc/math.h:668:39: No suitable candidate found for function \is_finite.
/usr/local/share/frama-c/libc/math.h:675:50: calls to C++ functions/methods like 'fmod' are not allowed in ACSL++
/usr/local/share/frama-c/libc/math.h:682:51: calls to C++ functions/methods like 'fmodf' are not allowed in ACSL++
/usr/local/share/frama-c/libc/math.h:719:42: No suitable candidate found for function \is_NaN.
/usr/local/share/frama-c/libc/math.h:759:56: unknown identifier '\plus_infinity'
/usr/local/share/frama-c/libc/math.h:765:48: unknown identifier '\is_plus_infinity'
### Additional Information :
parsing partiellement réussi, voici op_test_math:
[kernel] Parsing test_math.cpp (external front-end)
Now output intermediate result
/* Generated by Frama-C */
/*@
axiomatic MemCmp {
logic ℤ memcmp{L1, L2}(char *s1, char *s2, ℤ n)
reads \at(*(s1 + (0 .. n - 1)),L1), \at(*(s2 + (0 .. n - 1)),L2);
axiom memcmp_zero{L1, L2}:
∀ char *s1, char *s2;
∀ ℤ n;
memcmp{L1, L2}(s1, s2, n) ≡ 0 ⇔
(∀ ℤ i; 0 ≤ i < n ⇒ \at(*(s1 + i),L1) ≡ \at(*(s2 + i),L2));
}
*/
/*@
axiomatic MemChr {
logic 𝔹 memchr{L}(char *s, ℤ c, ℤ n)
reads *(s + (0 .. n - 1));
logic ℤ memchr_off{L}(char *s, ℤ c, ℤ n)
reads *(s + (0 .. n - 1));
axiom memchr_def{L}:
∀ char *s;
∀ ℤ c;
∀ ℤ n;
memchr(s, c, n) ≢ (0 ≢ 0) ⇔
(∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
}
*/
/*@
axiomatic MemSet {
logic 𝔹 memset{L}(char *s, ℤ c, ℤ n)
reads *(s + (0 .. n - 1));
axiom memset_def{L}:
∀ char *s;
∀ ℤ c;
∀ ℤ n;
memset(s, c, n) ≢ (0 ≢ 0) ⇔
(∀ ℤ i; 0 ≤ i < n ⇒ *(s + i) ≡ c);
}
*/
/*@
axiomatic StrLen {
logic ℤ strlen{L}(char *s)
reads *(s + (0 ..));
axiom strlen_pos_or_null{L}:
∀ char *s;
∀ ℤ i;
0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (char)0) ∧
*(s + i) ≡ (char)0 ⇒ strlen(s) ≡ i;
axiom strlen_neg{L}:
∀ char *s;
(∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (char)0) ⇒ strlen(s) < 0;
axiom strlen_before_null{L}:
∀ char *s;
∀ ℤ i; 0 ≤ i < strlen(s) ⇒ *(s + i) ≢ (char)0;
axiom strlen_at_null{L}:
∀ char *s; 0 ≤ strlen(s) ⇒ *(s + strlen(s)) ≡ (char)0;
axiom strlen_not_zero{L}:
∀ char *s;
∀ ℤ i;
0 ≤ i ≤ strlen(s) ∧ *(s + i) ≢ (char)0 ⇒ i < strlen(s);
axiom strlen_zero{L}:
∀ char *s;
∀ ℤ i;
0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)0 ⇒ i ≡ strlen(s);
axiom strlen_sup{L}:
∀ char *s;
∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
axiom strlen_shift{L}:
∀ char *s;
∀ ℤ i; 0 ≤ i ≤ strlen(s) ⇒ strlen(s + i) ≡ strlen(s) - i;
axiom strlen_create{L}:
∀ char *s;
∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ (char)0 ⇒ 0 ≤ strlen(s) ≤ i;
axiom strlen_create_shift{L}:
∀ char *s;
∀ ℤ i;
∀ ℤ k;
0 ≤ k ≤ i ∧ *(s + i) ≡ (char)0 ⇒
0 ≤ strlen(s + k) ≤ i - k;
axiom memcmp_strlen_left{L}:
∀ char *s1, char *s2;
∀ ℤ n;
memcmp{L, L}(s1, s2, n) ≡ 0 ∧ strlen(s1) < n ⇒
strlen(s1) ≡ strlen(s2);
axiom memcmp_strlen_right{L}:
∀ char *s1, char *s2;
∀ ℤ n;
memcmp{L, L}(s1, s2, n) ≡ 0 ∧ strlen(s2) < n ⇒
strlen(s1) ≡ strlen(s2);
axiom memcmp_strlen_shift_left{L}:
∀ char *s1, char *s2;
∀ ℤ k, ℤ n;
memcmp{L, L}(s1, s2 + k, n) ≡ 0 ≤ k ∧ strlen(s1) < n ⇒
0 ≤ strlen(s2) ≤ k + strlen(s1);
axiom memcmp_strlen_shift_right{L}:
∀ char *s1, char *s2;
∀ ℤ k, ℤ n;
memcmp{L, L}(s1 + k, s2, n) ≡ 0 ≤ k ∧ strlen(s2) < n ⇒
0 ≤ strlen(s1) ≤ k + strlen(s2);
}
*/
/*@
axiomatic StrCmp {
logic ℤ strcmp{L}(char *s1, char *s2)
reads *(s1 + (0 .. strlen(s1))), *(s2 + (0 .. strlen(s2)));
axiom strcmp_zero{L}:
∀ char *s1, char *s2;
strcmp(s1, s2) ≡ 0 ⇔
strlen(s1) ≡ strlen(s2) ∧
(∀ ℤ i; 0 ≤ i ≤ strlen(s1) ⇒ *(s1 + i) ≡ *(s2 + i));
}
*/
/*@
axiomatic StrNCmp {
logic ℤ strncmp{L}(char *s1, char *s2, ℤ n)
reads *(s1 + (0 .. n - 1)), *(s2 + (0 .. n - 1));
axiom strncmp_zero{L}:
∀ char *s1, char *s2;
∀ ℤ n;
strncmp(s1, s2, n) ≡ 0 ⇔
(strlen(s1) < n ∧ strcmp(s1, s2) ≡ 0) ∨
(∀ ℤ i; 0 ≤ i < n ⇒ *(s1 + i) ≡ *(s2 + i));
}
*/
/*@
axiomatic StrChr {
logic 𝔹 strchr{L}(char *s, ℤ c)
reads *(s + (0 .. strlen(s)));
axiom strchr_def{L}:
∀ char *s;
∀ ℤ c;
strchr(s, c) ≢ (0 ≢ 0) ⇔
(∃ ℤ i; 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)((int)c));
}
*/
/*@
axiomatic WMemChr {
logic 𝔹 wmemchr{L}(int *s, int c, ℤ n)
reads *(s + (0 .. n - 1));
logic ℤ wmemchr_off{L}(int *s, int c, ℤ n)
reads *(s + (0 .. n - 1));
axiom wmemchr_def{L}:
∀ int *s;
∀ int c;
∀ ℤ n;
wmemchr(s, c, n) ≢ (0 ≢ 0) ⇔
(∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
}
*/
/*@
axiomatic WcsLen {
logic ℤ wcslen{L}(int *s)
reads *(s + (0 ..));
axiom wcslen_pos_or_null{L}:
∀ int *s;
∀ ℤ i;
0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ (int)0) ∧
*(s + i) ≡ (int)0 ⇒ wcslen(s) ≡ i;
axiom wcslen_neg{L}:
∀ int *s;
(∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ (int)0) ⇒ wcslen(s) < 0;
axiom wcslen_before_null{L}:
∀ int *s;
∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ (int)0;
axiom wcslen_at_null{L}:
∀ int *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ (int)0;
axiom wcslen_not_zero{L}:
∀ int *s;
∀ int i;
0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ (int)0 ⇒ i < wcslen(s);
axiom wcslen_zero{L}:
∀ int *s;
∀ int i;
0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ (int)0 ⇒ i ≡ wcslen(s);
axiom wcslen_sup{L}:
∀ int *s;
∀ int i; 0 ≤ i ∧ *(s + i) ≡ (int)0 ⇒ 0 ≤ wcslen(s) ≤ i;
axiom wcslen_shift{L}:
∀ int *s;
∀ int i; 0 ≤ i ≤ wcslen(s) ⇒ wcslen(s + i) ≡ wcslen(s) - i;
axiom wcslen_create{L}:
∀ int *s;
∀ int i; 0 ≤ i ∧ *(s + i) ≡ (int)0 ⇒ 0 ≤ wcslen(s) ≤ i;
axiom wcslen_create_shift{L}:
∀ int *s;
∀ int i;
∀ int k;
0 ≤ k ≤ i ∧ *(s + i) ≡ (int)0 ⇒ 0 ≤ wcslen(s + k) ≤ i - k;
}
*/
/*@
axiomatic WcsCmp {
logic ℤ wcscmp{L}(int *s1, int *s2)
reads *(s1 + (0 .. wcslen(s1))), *(s2 + (0 .. wcslen(s2)));
axiom wcscmp_zero{L}:
∀ int *s1, int *s2;
wcscmp(s1, s2) ≡ 0 ⇔
wcslen(s1) ≡ wcslen(s2) ∧
(∀ ℤ i; 0 ≤ i ≤ wcslen(s1) ⇒ *(s1 + i) ≡ *(s2 + i));
}
*/
/*@
axiomatic WcsNCmp {
logic ℤ wcsncmp{L}(int *s1, int *s2, ℤ n)
reads *(s1 + (0 .. n - 1)), *(s2 + (0 .. n - 1));
axiom wcsncmp_zero{L}:
∀ int *s1, int *s2;
∀ ℤ n;
wcsncmp(s1, s2, n) ≡ 0 ⇔
(wcslen(s1) < n ∧ wcscmp(s1, s2) ≡ 0) ∨
(∀ ℤ i; 0 ≤ i < n ⇒ *(s1 + i) ≡ *(s2 + i));
}
*/
/*@
axiomatic WcsChr {
logic 𝔹 wcschr{L}(int *wcs, ℤ wc)
reads *(wcs + (0 .. wcslen(wcs)));
axiom wcschr_def{L}:
∀ int *wcs;
∀ ℤ wc;
wcschr(wcs, wc) ≢ (0 ≢ 0) ⇔
(∃ ℤ i; 0 ≤ i ≤ wcslen(wcs) ∧ *(wcs + i) ≡ (int)((int)wc));
}
*/
/*@ logic ℤ minimum(ℤ i, ℤ j) = i < j? i: j;
*/
/*@ logic ℤ maximum(ℤ i, ℤ j) = i < j? j: i;
*/
/*@
predicate valid_string{L}(char *s) =
0 ≤ strlen(s) ∧ \valid(s + (0 .. strlen(s)));
*/
/*@
predicate valid_read_string{L}(char *s) =
0 ≤ strlen(s) ∧ \valid_read(s + (0 .. strlen(s)));
*/
/*@
predicate valid_read_nstring{L}(char *s, ℤ n) =
(\valid_read(s + (0 .. n - 1)) ∧ \initialized(s + (0 .. n - 1))) ∨
valid_read_string(s);
*/
/*@
predicate valid_string_or_null{L}(char *s) = s ≡ \null ∨ valid_string(s);
*/
/*@
predicate valid_wstring{L}(int *s) =
0 ≤ wcslen(s) ∧ \valid(s + (0 .. wcslen(s)));
*/
/*@
predicate valid_read_wstring{L}(int *s) =
0 ≤ wcslen(s) ∧ \valid_read(s + (0 .. wcslen(s)));
*/
/*@
predicate valid_read_nwstring{L}(int *s, ℤ n) =
(\valid_read(s + (0 .. n - 1)) ∧ \initialized(s + (0 .. n - 1))) ∨
valid_read_wstring(s);
*/
/*@
predicate valid_wstring_or_null{L}(int *s) =
s ≡ \null ∨ valid_wstring(s);
*/
int __fc_errno;
char *program_invocation_name;
char *program_invocation_short_name;
/*@ assigns \result;
assigns \result \from x;
behavior nan:
assumes is_nan: \is_NaN(x);
ensures fp_nan: \result ≡ 0;
behavior inf:
assumes is_infinite: ¬\is_NaN(x) ∧ ¬\is_finite(x);
ensures fp_infinite: \result ≡ 1;
behavior zero:
assumes is_a_zero: x ≡ 0.0;
ensures fp_zero: \result ≡ 2;
behavior subnormal:
assumes is_finite: \is_finite(x);
assumes
is_subnormal:
(x > 0.0 ∧ x < 0x1p-126) ∨ (x < 0.0 ∧ x > -0x1p-126);
ensures fp_subnormal: \result ≡ 3;
behavior normal:
assumes is_finite: \is_finite(x);
assumes not_subnormal: x ≤ -0x1p-126 ∨ x ≥ 0x1p-126;
ensures fp_normal: \result ≡ 4;
complete behaviors normal, subnormal, zero, inf, nan;
disjoint behaviors normal, subnormal, zero, inf, nan;
*/
int __fc_fpclassifyf(float x);
/*@ assigns \result;
assigns \result \from x;
behavior nan:
assumes is_nan: \is_NaN(x);
ensures fp_nan: \result ≡ 0;
behavior inf:
assumes is_infinite: ¬\is_NaN(x) ∧ ¬\is_finite(x);
ensures fp_infinite: \result ≡ 1;
behavior zero:
assumes is_a_zero: x ≡ 0.0;
ensures fp_zero: \result ≡ 2;
behavior subnormal:
assumes is_finite: \is_finite(x);
assumes
is_subnormal:
(x > 0.0 ∧ x < 0x1p-1022) ∨ (x < 0.0 ∧ x > -0x1p-1022);
ensures fp_subnormal: \result ≡ 3;
behavior normal:
assumes is_finite: \is_finite(x);
assumes not_subnormal: x ≤ -0x1p-1022 ∨ x ≥ 0x1p-1022;
ensures fp_normal: \result ≡ 4;
complete behaviors normal, subnormal, zero, inf, nan;
disjoint behaviors normal, subnormal, zero, inf, nan;
*/
int __fc_fpclassify(double x);
/*@ assigns __fc_errno, \result;
assigns __fc_errno \from x;
assigns \result \from x;
behavior normal:
assumes in_domain: \is_finite(x) ∧ \abs(x) ≤ 1;
ensures positive_result: \is_finite(\result) ∧ \result ≥ 0;
assigns \result;
assigns \result \from x;
behavior domain_error:
*/
double acos(double x);
/*@ assigns __fc_errno, \result;
assigns __fc_errno \from x;
assigns \result \from x;
behavior normal:
assumes in_domain: \is_finite(x) ∧ \abs(x) ≤ 1;
ensures positive_result: \is_finite(\result) ∧ \result ≥ 0;
assigns \result;
assigns \result \from x;
behavior domain_error:
*/
float acosf(float x);
/*@ assigns __fc_errno, \result;
assigns __fc_errno \from x;
assigns \result \from x;
behavior normal:
*/
long double acosl(long double x);
/*@ assigns __fc_errno, \result;
assigns __fc_errno \from x;
assigns \result \from x;
behavior normal:
assumes in_domain: \is_finite(x) ∧ \abs(x) ≤ 1;
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x;
behavior domain_error:
*/
double asin(double x);
/*@ assigns __fc_errno, \result;
assigns __fc_errno \from x;
assigns \result \from x;
behavior normal:
assumes in_domain: \is_finite(x) ∧ \abs(x) ≤ 1;
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x;
behavior domain_error:
*/
float asinf(float x);
/*@ assigns __fc_errno, \result;
assigns __fc_errno \from x;
assigns \result \from x;
behavior normal:
*/
long double asinl(long double x);
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
ensures result_domain: -1.571 ≤ \result ≤ 1.571;
assigns \result;
assigns \result \from x;
*/
float atanf(float x);
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
ensures result_domain: -1.571 ≤ \result ≤ 1.571;
assigns \result;
assigns \result \from x;
*/
double atan(double x);
/*@ requires finite_args: \is_finite(x) ∧ \is_finite(y); */
double atan2(double y, double x);
/*@ requires finite_args: \is_finite(x) ∧ \is_finite(y); */
float atan2f(float y, float x);
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
ensures result_domain: -1. ≤ \result ≤ 1.;
assigns \result;
assigns \result \from x;
*/
double cos(double x);
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
ensures result_domain: -1. ≤ \result ≤ 1.;
assigns \result;
assigns \result \from x;
*/
float cosf(float x);
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
ensures result_domain: -1. ≤ \result ≤ 1.;
assigns \result;
assigns \result \from x;
*/
double sin(double x);
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
ensures result_domain: -1. ≤ \result ≤ 1.;
assigns \result;
assigns \result \from x;
*/
float sinf(float x);
/*@ assigns __fc_errno, \result;
assigns __fc_errno \from x;
assigns \result \from x;
behavior normal:
assumes in_domain: \is_finite(x) ∧ x ≥ 1;
ensures positive_result: \is_finite(\result) ∧ \result ≥ 0;
assigns \result;
assigns \result \from x;
behavior infinite:
*/
double acosh(double x);
/*@ assigns __fc_errno, \result;
assigns __fc_errno \from x;
assigns \result \from x;
behavior normal:
assumes in_domain: \is_finite(x) ∧ x ≥ 1;
ensures positive_result: \is_finite(\result) ∧ \result ≥ 0;
assigns \result;
assigns \result \from x;
behavior infinite:
*/
float acoshf(float x);
/*@ assigns __fc_errno, \result;
assigns __fc_errno \from x;
assigns \result \from x;
behavior normal:
*/
long double acoshl(long double x);
/*@ requires finite_arg: \is_finite(x);
requires finite_domain: x ≤ 0x1.62e42fefa39efp+9;
ensures res_finite: \is_finite(\result);
ensures positive_result: \result > 0.;
assigns \result;
assigns \result \from x;
*/
double exp(double x);
/*@ requires finite_arg: \is_finite(x);
requires res_finite: x ≤ 0x1.62e42ep+6;
ensures res_finite: \is_finite(\result);
ensures positive_result: \result > 0.;
assigns \result;
assigns \result \from x;
*/
float expf(float x);
/*@ requires finite_arg: \is_finite(x);
requires arg_positive: x > 0;
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x;
*/
double log(double x);
/*@ requires finite_arg: \is_finite(x);
requires arg_positive: x > 0;
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x;
*/
float logf(float x);
/*@ requires finite_arg: \is_finite(x);
requires arg_positive: x > 0;
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x;
*/
double log10(double x);
/*@ requires finite_arg: \is_finite(x);
requires arg_positive: x > 0;
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x;
*/
float log10f(float x);
/*@ requires finite_arg: \is_finite(x);
requires arg_positive: x > 0;
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x;
*/
double log2(double x);
/*@ requires finite_arg: \is_finite(x);
requires arg_positive: x > 0;
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x;
*/
float log2f(float x);
/*@ requires finite_arg: \is_finite(x);
ensures res_finite: \is_finite(\result);
ensures positive_result: \result ≥ 0.;
ensures
equal_magnitude_result: \result ≡ \old(x) ∨ \result ≡ -\old(x);
assigns \result;
assigns \result \from x;
*/
double fabs(double x);
/*@ requires finite_arg: \is_finite(x);
ensures res_finite: \is_finite(\result);
ensures positive_result: \result ≥ 0.;
ensures
equal_magnitude_result: \result ≡ \old(x) ∨ \result ≡ -\old(x);
assigns \result;
assigns \result \from x;
*/
float fabsf(float x);
/*@ requires finite_args: \is_finite(x) ∧ \is_finite(y); */
double pow(double x, double y);
/*@ requires finite_args: \is_finite(x) ∧ \is_finite(y); */
float powf(float x, float y);
/*@ requires finite_arg: \is_finite(x);
requires arg_positive: x ≥ -0.;
ensures finite_result: \is_finite(\result);
ensures positive_result: \result ≥ -0.;
assigns \result;
assigns \result \from x;
*/
double sqrt(double x);
/*@ requires finite_arg: \is_finite(x);
requires arg_positive: x ≥ -0.;
ensures finite_result: \is_finite(\result);
ensures positive_result: \result ≥ -0.;
assigns \result;
assigns \result \from x;
*/
float sqrtf(float x);
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x;
*/
double ceil(double x);
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x;
*/
float ceilf(float x);
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x;
*/
double floor(double x);
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x;
*/
float floorf(float x);
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x;
*/
double round(double x);
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x;
*/
float roundf(float x);
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x;
*/
double trunc(double x);
/*@ requires finite_arg: \is_finite(x);
ensures finite_result: \is_finite(\result);
assigns \result;
assigns \result \from x;
*/
float truncf(float x);
/*@ requires finite_args: \is_finite(x) ∧ \is_finite(y); */
double fmod(double x, double y);
/*@ requires finite_args: \is_finite(x) ∧ \is_finite(y); */
float fmodf(float x, float y);
/*@ requires tagp_valid_string: valid_read_string(tagp);
ensures result_is_nan: \is_NaN(\result);
assigns \result;
assigns \result \from (indirect: *(tagp + (0 ..)));
*/
double nan(char const *tagp);
/*@ requires tagp_valid_string: valid_read_string(tagp);
ensures result_is_nan: \is_NaN(\result);
assigns \result;
assigns \result \from (indirect: *(tagp + (0 ..)));
*/
float nanf(char const *tagp);
/*@ requires tagp_valid_string: valid_read_string(tagp);
assigns \result;
assigns \result \from (indirect: *(tagp + (0 ..)));
*/
long double nanl(char const *tagp);
/*@ ensures result_is_nan: \is_NaN(\result);
assigns \result;
assigns \result \from \nothing;
*/
float __fc_nan(int x);
### Steps To Reproduce :
frama-c test_math.cpp -print > op_test_math
## Attachments
- [test_math.cpp](/uploads/bce7c18e055ca2e12eb308736c0934fb/test_math.cpp)Franck VedrineFranck Vedrinehttps://git.frama-c.com/pub/frama-c/-/issues/100Left pan (file tree and plugin views) inaccessible upon resize in frama-c-gui2022-09-28T11:26:03Zmantis-gitlab-migrationLeft pan (file tree and plugin views) inaccessible upon resize in frama-c-guiID0002486:
**This issue was created automatically from Mantis Issue 2486. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002486:
**This issue was created automatically from Mantis Issue 2486. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002486 | Frama-C | Graphical User Interface | public | 2019-11-16 | 2019-11-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Nanoboss | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | immediate | **Severity** | major | **Reproducibility** | always |
| **Platform** | Mac | **OS** | MacOS | **OS Version** | 10.15 (19A583) |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
I tried to remove the file tree and the plugin view using the slider (the little dots on the left) to have more space. But impossible to access it again as it's positioned really close from the border. Can't click and drag anymore.
Tested on 2 Macs, rebooting the laptop, restarting Frama-c-gui, a complete reinstallation of opam and brew didn't solve the issue. The windows keeps the same dimensions when we restart frama-c. Might come from gtk, but can't find where the windows properties are stored.
### Steps To Reproduce :
Click on the dots on the left pan, drag to the left until it disappears completely and try to drag it back. I suspect that the issue might be similar for the right pan
## Attachments
- ![Capture_d_____cran_2019-11-16____09.13.42](/uploads/18ce155f416a4ce1efb041889022bb08/Capture_d_____cran_2019-11-16____09.13.42.png)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/101-wp-out missing output for Why3 provers in Frama-C 20 beta2023-07-21T13:31:03ZJens Gerlach-wp-out missing output for Why3 provers in Frama-C 20 betaID0002485:
**This issue was created automatically from Mantis Issue 2485. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002485:
**This issue was created automatically from Mantis Issue 2485. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002485 | Frama-C | Plug-in > wp | public | 2019-11-08 | 2019-11-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | Linux | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
When the attached programme is processed with
frama-c -wp -wp-rte -wp-prover native:alt-ergo -wp-out abs.wp abs.c
then the output directory 'abs.wp/typed' contains three files
abs_ensures_3_Alt-Ergo.mlw
abs_ensures_3_Alt-Ergo.out
abs_ensures_3.ergo
When using the command line
frama-c -wp -wp-rte -wp-prover alt-ergo -wp-out abs.wp abs.c
then the output directory 'abs.wp/typed' contains only the generated proof obligation
abs_ensures_3_Why3_Alt_Ergo_2_3_0.why
(similiarly when using another Why3 prover, such as cvc4)
Is there a way to output also the result for Why3 provers?
## Attachments
- [abs.c](/uploads/9fd4b3dcc0cf8490758da51b696be918/abs.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/102alt-ergo support in Frama-C 20 beta2021-04-14T07:30:38ZJens Gerlachalt-ergo support in Frama-C 20 betaID0002484:
**This issue was created automatically from Mantis Issue 2484. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002484:
**This issue was created automatically from Mantis Issue 2484. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002484 | Frama-C | Plug-in > wp | public | 2019-11-08 | 2019-11-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | Linux | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
This is a hint to (better) describe the transition from using alt-ergo in Frama-C 19 and 20.
If it is already described, then I apologize.
In Frama-C 19 and before one uses
-wp-prover alt-ergo for the native interface and
-wp-prover why3:alt-ergo for the Why3 interface
In Frama-C 20 the respective options are
-wp-prover native:alt-ergo for the native interface and
-wp-prover alt-ergo
I propose that it is described with other things in a short transition document.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/103Eprover in Frama-C 20 beta2021-04-15T09:36:20ZJens GerlachEprover in Frama-C 20 betaID0002483:
**This issue was created automatically from Mantis Issue 2483. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002483:
**This issue was created automatically from Mantis Issue 2483. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002483 | Frama-C | Plug-in > wp | public | 2019-11-08 | 2019-11-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Linux | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
I played a bit with various automatic provers in the beta
alt-ergo (2.3.0), native:alt-ergo (2.3.0), cvc4 (1.6), cvc3 (2.4.1), z3 (4.8.6) are recognized.
Eprover (2.4), on the other hand, is not recognized.
To be honest, Eprover is not such a great prover, but it has helped us discovering inconsistencies in our specifications.
Is there a specific reason, Eprover is not supported?
Attached is the error message.
### Steps To Reproduce :
$ frama-c -wp -wp-rte -wp-prover eprover -wp-out abs.wp abs.c
[kernel] Parsing abs.c (with preprocessing)
[rte] annotating function abs_int
[wp] 6 goals scheduled
[wp] [Eprover 2.4] Goal typed_abs_int_ensures_3 : Failed
[Why3 Error] Unknown printer 'tptp-fof'
[wp] [Cache] not used
[wp] Proved goals: 5 / 6
Qed: 5 (0.60ms-3ms-6ms)
Eprover 2.4: 0 (failed: 1)
## Attachments
- [abs.c](/uploads/07380fd95e05b2515b8f7dec3a1bad41/abs.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/104readability of coq(?) names2021-02-22T14:01:08ZJens Gerlachreadability of coq(?) namesID0002100:
**This issue was created automatically from Mantis Issue 2100. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002100:
**This issue was created automatically from Mantis Issue 2100. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002100 | Frama-C | Plug-in > wp | public | 2015-03-31 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Consider the following ACSL lemma:
/*@
lemma X : \forall integer a, b; (a+b)*(a-b) == a*a - b*b;
*/
which is automatically discharged by alt-ergo.
When I open the proof obligation in Coq, the lemma looks like follows:
Goal
forall (i_1 i : Z),
(((i_1 * i_1) = ((i * i) + ((i + i_1) * (i_1 - i))))%Z)%Z.
Under Neon the proof coq representation preserves the original names much better
Goal
forall (a_0 b_0 : Z),
(((a_0 * a_0) = ((b_0 * b_0) + ((a_0 + b_0) * (a_0 - b_0))))%Z)%Z.
The problem gets worse with more parameters.
### Steps To Reproduce :
frama-c-gui -wp lemma.c
## Attachments
- [lemma.c](/uploads/61fcccb55ed44434e03f68ed4e4963af/lemma.c)https://git.frama-c.com/pub/frama-c/-/issues/105suggest boolean expressions for "-wp-prop" arguments2021-02-22T12:53:37ZJochen Burghardtsuggest boolean expressions for "-wp-prop" argumentsID0002285:
**This issue was created automatically from Mantis Issue 2285. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002285:
**This issue was created automatically from Mantis Issue 2285. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002285 | Frama-C | Plug-in > wp | public | 2017-02-27 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | won't fix |
| **Priority** | low | **Severity** | feature | **Reproducibility** | always |
| **Platform** | Silicon-20161101 | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Currently, the semantics of "-wp-prop" arguments is unexplained and difficult to understand, when negation and more than one label is used.
For example, using the attached file, "-wp=prop=A,B,-C" selects l4,l5,l6, whereas "-wp-prop=-C,B,A" selects all but l3, and so does "-wp-prop=A,B,c" (although the set of "C"-labelled lemmas is the complement of that of the "c"-labelled lemmas).
I think, parsing arbitrary boolean expressions (built from "!", "&&", "||") isn't more difficult that the current mechanism, but is easier to describe in the manual and to understand.
Alternatively, "-" could be kept as negation, "," could be used for cunjunction only, and the results of multiple args "-wp-prop=X -wp-prop=Y" could be or-ed together; this would at least allow to express arbitrary sets in disjunctive normal form.
### Additional Information :
Complex set expressions arise when labels are used during proof development to attach prover names (and even options) to properties. Using calls like "frama-c -wp -wp-prop=PROVE_WITH_CVC4 -wp-prover=cvc4 ..." can save a lot of proving time that is normally wasted by unsuccessful attempts by unsuitable provers. Other labels that can save time are "TODO", "NEEDS_LONG_TIMEOUT", etc. This way, boolean expressions arise in a natural way; and the user needs to be sure about their semantics, in order not to overlook proof obligations due to splitting by prover.
## Attachments
- [proptest.c](/uploads/969a6dcaeb4f45e418845f21976d9cb7/proptest.c)
- [bbb.c](/uploads/5672cfb09ff165d83ff4c8efc35aacbd/bbb.c)https://git.frama-c.com/pub/frama-c/-/issues/106suggest unique term normalization for lemmas and goals2021-02-22T12:53:39ZJochen Burghardtsuggest unique term normalization for lemmas and goalsID0002329:
**This issue was created automatically from Mantis Issue 2329. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002329:
**This issue was created automatically from Mantis Issue 2329. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002329 | Frama-C | Plug-in > wp | public | 2017-10-09 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | Phosphorus-20170501 | **OS** | - | **OS Version** | xubuntu 17.04 |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-prop g aaa.c" on the attached file fails to prove the assertion "g", although it obviously follows from "f" by applying lemma "lem". One reason for that is of course the inherent incompleteness of SMT provers like Alt-Ergo and Cvc4. However, another reason is that Frama-C's term normalization(1) swaps some arguments of "+", and
(2) performs swaps in the lemma that differ from those performed in the goal.
As a result, in the attached mlw file,
"(L_Foo(a,b+c)=true) -> (L_Bar(a,c+d)=true)"
appears in the lemma, while "(L_Foo(a,i_1+i_2)=true) -> (L_Bar(a,i+i_1)=true)" appears in the goal. The latter is equivalent to
"(L_Foo(a,c+b)=true) -> (L_Bar(a,d+c)=true)"
when expressed in a notation closer to the source-code. Variable "c" is common to L_Foo and L_Bar; note its different positions in the lemma vs. in the goal.
If the goal is changed to "(L_Foo(a,i_2+i_1)=true) -> (L_Bar(a,i_1+i)=true)", it syntactically matches the lemma, and Alt-Ergo proves it in a few milliseconds.
Unless there are good reasons to swap the arguments of "+", they should be kept in their source-code order; this way, the user has a chance to control what is given to the provers.
However, if there *are* good reasons to include argument swapping in term normalization, it should be performed in the same way both in lemmas and in goals.
A possible explanation for the above behavior of Frama-C is that, for some
reason, source-code variable names are transformed to unrelated internal names
in goals, but not in lemmas, and that term normalization just orders arguments
of commutative functions lexicographically (cf. issue #2100).
## Attachments
- [aaa.c](/uploads/86f4cf4ef5586dff6d49e1d6d35ff66e/aaa.c)
- [main_assert_g_Alt-Ergo.mlw](/uploads/4875bf8644ee1246e06bb880e675a7ad/main_assert_g_Alt-Ergo.mlw)https://git.frama-c.com/pub/frama-c/-/issues/107Information on C type of array is not present (in Coq)2021-02-22T13:48:11ZJens GerlachInformation on C type of array is not present (in Coq)ID0002332:
**This issue was created automatically from Mantis Issue 2332. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002332:
**This issue was created automatically from Mantis Issue 2332. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002332 | Frama-C | Plug-in > wp | public | 2017-11-22 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Linux, macOS | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
In the attached file 'array.c' there are two simple predicates 'AllEqual' and 'Constant' that involve int arrays.
There are also two lemmas that relate both predicate.
While it can automatically verified that "Constant" implies "AllEqual" the proof of the "converse" statement fails. When looking at the Coq presentation of "AllEqual" it becomes apparent that Coq only sees an "integer array"; the specific C type (represented by the predicate 'is_sint32') is NOT present at all.
### Additional Information :
The error also occurs in the beta release of Frama-C 16 (Sulfur).
### Steps To Reproduce :
Run the command:
frama-c-gui -no-unicode -wp -wp-prover alt-ergo -wp-prover coq -wp-script 'wp0.script' array.c
## Attachments
- [array.c](/uploads/9ffd5dc713b956ec02a3457ddc3b71c6/array.c)
- [wp0.script](/uploads/eb44100130d8efee641d5565ee82857b/wp0.script)https://git.frama-c.com/pub/frama-c/-/issues/108suggest to supply previous "ensures" as hypotheses in proof obligation of nex...2021-02-22T12:53:43ZJochen Burghardtsuggest to supply previous "ensures" as hypotheses in proof obligation of next "ensures"ID0002336:
**This issue was created automatically from Mantis Issue 2336. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002336:
**This issue was created automatically from Mantis Issue 2336. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002336 | Frama-C | Plug-in > wp | public | 2017-12-08 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | suspended |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.04 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-rte foo.c -wp-out wp-out" on the attached file fails to prove clauses "E1" (as expected) and "E2". The latter is provable from "E1" by axiom "a2". A look at file "main_post_E2_Alt-Ergo.mlw" reveals that "E1" isn't given as hypothesis, and hence axiom "a2" can't be applied.
I cannot judge whether there is good reason for this behavior of Frama-C/Wp. If there isn't, I suggest that "E1" should be given as hypothesis to the proof obligation for "E2", similar to Frama-C/Wp's behavior on consecutive "assigns" clauses. The same applies to statement contracts.
## Attachments
- [foo.c](/uploads/5ad3994f41ed8b1f3aec521fbbf78ded/foo.c)https://git.frama-c.com/pub/frama-c/-/issues/109Crash on loop with global assigns and per-behavior assigns2021-02-22T13:47:26ZBoris YakobowskiCrash on loop with global assigns and per-behavior assignsID0002180:
**This issue was created automatically from Mantis Issue 2180. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002180:
**This issue was created automatically from Mantis Issue 2180. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002180 | Frama-C | Plug-in > wp | public | 2015-10-19 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | correnson | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
frama-c -wp crashes on the following program
/*@ behavior foo:
*/
void main(void)
{
int i;
int t[10];
i = 0;
/*@ loop assigns t[0 .. i];
for foo: loop assigns t[0 .. i]; */
while (i < 10) {
t[i] = 0;
i ++;
}
return;
}https://git.frama-c.com/pub/frama-c/-/issues/111Coq translation of predicate name changes when additional files are processed...2021-02-22T14:00:22ZJochen BurghardtCoq translation of predicate name changes when additional files are processed by Frama-CID0002340:
**This issue was created automatically from Mantis Issue 2340. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002340:
**This issue was created automatically from Mantis Issue 2340. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002340 | Frama-C | Plug-in > wp | public | 2018-01-04 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | Ubuntu | **OS Version** | Ubuntu 17.04 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-script wp0.script -wp-model Typed+ref -wp-prover coq -wp-prop LowerBoundShift equal_range2_cpp.c" succeeds in proving the lemma in line 16 of "equal_range2_cpp.c", using the Coq proof in file "wp0.script".
However, when "lower_bound_cpp.c" is appended as another command line argument to the same call, the lemma is no longer proven.
Using "wp-out" arguments and running a "diff -r" on the resulting directories reveals that the ACSL predicate name "LowerBound" is translated as "P_LowerBound_1_" for the first (succeeding) run, but as "P_LowerBound_2_" for the second (failing) run.
Note that the definitions of the "LowerBound" predicates literally agree in both C files.
The problem disappears when the overloaded 3-argument version of predicate "LowerBound" is omitted in both C files, or when the contract (i.e. the only use of "LowerBound" in that file) is omitted in file "lower_bound_cpp.c".
## Attachments
- [equal_range2_cpp.c](/uploads/a7f339a24fa1ad2c67458331246b61a8/equal_range2_cpp.c)
- [lower_bound_cpp.c](/uploads/1b5c79b560a67c3ba096b9ce8462c3fc/lower_bound_cpp.c)
- [wp0.script](/uploads/a549eb877d73af8f17c7be0a3cad6d0c/wp0.script)https://git.frama-c.com/pub/frama-c/-/issues/112alt-ergo goals generated directly / via why3 differ in provability2021-02-22T12:53:52ZJochen Burghardtalt-ergo goals generated directly / via why3 differ in provabilityID0002353:
**This issue was created automatically from Mantis Issue 2353. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002353:
**This issue was created automatically from Mantis Issue 2353. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002353 | Frama-C | Plug-in > wp | public | 2018-02-01 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.04 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
I generated an Alt-Ergo proof obligation for the ensures clause "xxx" (line 1140) of the attached program "search_n_standalone.c" (which was obtained from "search_n" in "Acsl by example" by "gcc -E -C"). When I did this directly (see attached script "fd"), it was proven without problems. However, when I did this via Why3 (see script "fw"), Alt-Ergo responded "Don't know" after 0.1 seconds.
In order to compare both mlw files given to Alt-Ergo, I moved the goal of the via-Why3 file into the direct file; it became provable there. Removing as many axioms and definitions as possible while keeping the (non-)provability, I obtained the files "xxx_direct.mlw" and "xxx_via_why3.mlw". It seems that the former defines and uses "shift_sint32", while the latter does not (it uses "shift" instead). Probably, this is the reason for the different outcomes of Alt-Ergo.
Although the observed issue may not be bug (both mlw files may be semanically equivalent), it might be desirable to unify the proof obligations given to Alt-Ergo on different pathways.
## Attachments
- [search_n_standalone.c](/uploads/79defa5986c7ebb10060cb2d8013dd27/search_n_standalone.c)
- [fd](/uploads/2325b1feb2a0e2c6bc2768f1552ecbf9/fd)
- [fw](/uploads/ade985efb5f8ea0601fa91f90ec1f340/fw)
- [xxx_direct.mlw](/uploads/49efc095c1124c4e87c110c2b7a10bb7/xxx_direct.mlw)
- [xxx_via_why3.mlw](/uploads/28204d54407af26ed64d8841005b5cef/xxx_via_why3.mlw)https://git.frama-c.com/pub/frama-c/-/issues/113Auto-generated assigns clause for a void* argument crashes wp2021-02-22T13:34:40Zmantis-gitlab-migrationAuto-generated assigns clause for a void* argument crashes wpID0002385:
**This issue was created automatically from Mantis Issue 2385. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002385:
**This issue was created automatically from Mantis Issue 2385. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002385 | Frama-C | Plug-in > wp | public | 2018-07-05 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | schollet | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
When using an unspecified function with an void* argument from an external file, the default generated assigns clause for that argument crashes frama-c and WP miss-attributes the error to the user.
Specifically, for an unspecified function foo(void* p), the auto generated assigns clause states that the function assigns *((char *)p+(0 .. )), which is then picked up by WP as an invalid user input.
Version : Frama-C 17 Chlorine
### Additional Information :
The command run :
frama-c -wp test2.c
Error log :
[kernel] Parsing test2.c (with preprocessing)
[kernel:annot:missing-spec] test2.c:7: Warning:
Neither code nor specification for function foo, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] test2.c:11: User Error: Invalid infinite range i_0+(0..)
[kernel] Plug-in wp aborted: invalid user input.
The auto-generated assigns clause (found with frama-c-gui):
/*@ assigns *((char *)thing + (0 ..));
assigns *((char *)thing + (0 ..)) \from *((char *)thing + (0 ..));
*/
Removing the assigns clause for create stops WP from crashing
### Steps To Reproduce :
run `frama-c -wp test2.c` with those 3 provided files
OR:
Write a function and its specification with at least an assigns clause.
Write in it a call to another function.
Write in another file that 2nd function which takes as an argument an void*.
Write the header and include it in the first file.
For the header and the 2nd file, do not write any specification for the function.
run frama-c -wp on the first file
## Attachments
- [assigns.tar.gz](/uploads/7d8c7280dce8dde42f8cce1f86cbef35/assigns.tar.gz)https://git.frama-c.com/pub/frama-c/-/issues/114Newer releases of FramaC produce apparent WP plug-in bug2021-02-22T14:01:18Zmantis-gitlab-migrationNewer releases of FramaC produce apparent WP plug-in bugID0002401:
**This issue was created automatically from Mantis Issue 2401. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002401:
**This issue was created automatically from Mantis Issue 2401. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002401 | Frama-C | Plug-in > wp | public | 2018-10-01 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jmaytac | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
The code in the attached example models a reactive program which interacts with peripherals via memory mapped I/O through an address defined by a constant. While an older version of frama-C (Phosphorus) successfully produced Altergo axiomatizations of boolean logic functions like the "logic boolean isAMessage(mac_t mac)" defined in mac.h,
"
logic boolean isAMessage(mac_t mac) = ((mac->mac_packet.object_high == 0x0A) && (mac->mac_packet.object_low == 0x0A) && (mac->\
mac_packet.payload_length == 0x00));
"
the newer versions produce as AltErgo axiomatization (see out/typed/Axiomatic11.ergo in the attached)
"
function L_isAMessage
() :
bool =
andb(eqb(#{w_0}, 0), andb(eqb(#{w_1}, 10), eqb(#{w_2}, 10)))
"
Note that the argument to the boolean logic function is absent and the mac_t fields referenced in the ACSL definition of the logic function have. become "#{w_i}" - this malformed AltErgo (# is illegal in AltErgo) seems to originates from WP's QED module's pretty printer, whose find_var_env function returns these malformed names when it fails to find a given name in its environment.
### Steps To Reproduce :
tar -xvf framaBug.tar.gz
make wp
## Attachments
- [framaBug.tar.gz](/uploads/f07e549fb7296718c7ae0d86fb99b96e/framaBug.tar.gz)
- [frmaBug.tar.gz](/uploads/a43835306fcfcff1aef5bd28e09e0b4d/frmaBug.tar.gz)https://git.frama-c.com/pub/frama-c/-/issues/115dubious discharge of postcondition2021-02-22T14:00:51ZJens Gerlachdubious discharge of postconditionID0002390:
**This issue was created automatically from Mantis Issue 2390. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002390:
**This issue was created automatically from Mantis Issue 2390. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002390 | Frama-C | Plug-in > wp | public | 2018-07-24 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
Consider the following function
/*@
assigns \nothing;
ensures a == 0;
*/
void foo(int a)
{
a = 0;
}
The postcondition can of course not be verified because the assignment happens to a copy "a" and furthermore nothing is known about the value of "a" in the pre-state.
If I add, however, the admittedly weird looking precondition "requires \valid(&a);" as shown here
/*@
requires \valid(&a);
assigns \nothing;
ensures a == 0;
*/
void bar(int a)
{
a = 0;
}
then Qed discharges the postcondition.
I am not sure this a bug or rather caused by taking the address of a formal argument in the precondition
but in any case it would be nice if someone could have a look at it.
### Steps To Reproduce :
Call
frama-c -wp -wp-rte foo.c
on the attached file.
## Attachments
- [foo.c](/uploads/59eb64f1e1b8ca2563cbfa0bcbb63a83/foo.c)https://git.frama-c.com/pub/frama-c/-/issues/116crash2021-02-22T12:54:02Zmantis-gitlab-migrationcrashID0002409:
**This issue was created automatically from Mantis Issue 2409. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002409:
**This issue was created automatically from Mantis Issue 2409. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002409 | Frama-C | Plug-in > wp | public | 2018-11-13 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | hugo.gimbert | **Assigned To** | correnson | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | macosx | **OS** | mojave | **OS Version** | 10.14.1 |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
frama-c -wp somme.c
with somme.c containing
/*@
logic integer f(integer k) = k;
lemma sumint:
\forall int n;
n >= 0 ==> \sum(0,n,f) == n * (n+1) / 2;
*/
leads to crash
Trace below
### Additional Information :
[kernel] Parsing somme.c (with preprocessing)
[wp] Failure: Unbound logic variable 'f'
[kernel] Current source was: somme.c:4
The full backtrace is:
Raised at file "src/kernel_services/plugin_entry_points/log.ml" (inlined), line 531, characters 24-31
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 998, characters 12-50
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 524, characters 9-23
Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 527, characters 9-16
Called from file "src/plugins/wp/LogicSemantics.ml", line 205, characters 18-38
Called from file "src/plugins/wp/LogicSemantics.ml", line 238, characters 16-32
Called from file "src/plugins/wp/Warning.ml", line 146, characters 6-10
Called from file "src/plugins/wp/LogicSemantics.ml", line 920, characters 12-32
Called from file "src/plugins/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/plugins/wp/Context.ml", line 34, characters 35-46
Called from file "src/plugins/wp/LogicCompiler.ml" (inlined), line 435, characters 20-35
Called from file "src/plugins/wp/LogicSemantics.ml", line 124, characters 10-23
Called from file "list.ml", line 88, characters 20-23
Called from file "list.ml", line 88, characters 32-39
Called from file "list.ml", line 88, characters 32-39
Called from file "src/plugins/wp/LogicSemantics.ml", line 594, characters 23-52
Called from file "src/plugins/wp/Warning.ml", line 146, characters 6-10
Called from file "src/plugins/wp/LogicSemantics.ml", line 920, characters 12-32
Called from file "src/plugins/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/plugins/wp/Context.ml", line 34, characters 35-46
Called from file "src/plugins/wp/LogicCompiler.ml" (inlined), line 435, characters 20-35
Called from file "src/plugins/wp/LogicSemantics.ml", line 124, characters 10-23
Called from file "src/plugins/wp/LogicSemantics.ml", line 361, characters 16-35
Called from file "src/plugins/wp/Warning.ml", line 146, characters 6-10
Called from file "src/plugins/wp/LogicSemantics.ml", line 931, characters 12-42
Called from file "src/plugins/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/plugins/wp/Context.ml", line 34, characters 35-46
Called from file "src/plugins/wp/LogicCompiler.ml" (inlined), line 434, characters 28-51
Called from file "src/plugins/wp/LogicSemantics.ml", line 735, characters 39-62
Called from file "src/plugins/wp/Warning.ml", line 146, characters 6-10
Called from file "src/plugins/wp/LogicSemantics.ml", line 931, characters 12-42
Called from file "src/plugins/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/plugins/wp/Context.ml", line 34, characters 35-46
Called from file "src/plugins/wp/LogicCompiler.ml", line 399, characters 21-32
Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48
Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48
Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48
Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48
Called from file "src/plugins/wp/LogicCompiler.ml", line 485, characters 6-60
Called from file "src/plugins/wp/LogicCompiler.ml", line 741, characters 6-104
Called from file "src/plugins/wp/LogicCompiler.ml", line 758, characters 24-46
Called from file "src/plugins/wp/cfgWP.ml", line 1351, characters 31-42
Called from file "map.ml", line 295, characters 20-25
Called from file "src/plugins/wp/cfgWP.ml", line 1435, characters 19-59
Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48
Called from file "src/plugins/wp/Context.ml" (inlined), line 73, characters 21-47
Called from file "src/plugins/wp/Model.ml" (inlined), line 127, characters 21-45
Called from file "src/plugins/wp/Model.ml" (inlined), line 129, characters 18-36
Called from file "src/plugins/wp/cfgWP.ml", line 1433, characters 14-202
Called from file "src/plugins/wp/Model.ml", line 120, characters 17-20
Re-raised at file "src/plugins/wp/Model.ml", line 125, characters 19-28
Called from file "src/plugins/wp/Model.ml" (inlined), line 126, characters 19-36
Called from file "src/plugins/wp/cfgWP.ml", line 1431, characters 10-1023
Called from file "src/plugins/wp/register.ml", line 689, characters 15-40
Called from file "src/libraries/stdlib/extlib.ml", line 301, characters 14-17
Re-raised at file "src/libraries/stdlib/extlib.ml", line 301, characters 41-48
Called from file "src/libraries/stdlib/extlib.ml", line 302, characters 2-12
Called from file "src/libraries/stdlib/extlib.ml", line 302, characters 2-12
Called from file "queue.ml", line 105, 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 791, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 821, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 230, characters 4-8
Plug-in wp aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Chlorine-20180502.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
hugo-9:TP3 gimbert$ cat somme.c
/*@
logic integer f(integer k) = k;
lemma sumint:
\forall int n;
n >= 0 ==> \sum(0,n,f) == n * (n+1) / 2;
*/
## Attachments
- [somme.c](/uploads/5ef73e24f859da4da063d6d4e135ea99/somme.c)https://git.frama-c.com/pub/frama-c/-/issues/117contracts about memory mapped I/O through volatile memory locations2021-02-22T12:54:04Zmantis-gitlab-migrationcontracts about memory mapped I/O through volatile memory locationsID0002407:
**This issue was created automatically from Mantis Issue 2407. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002407:
**This issue was created automatically from Mantis Issue 2407. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002407 | Frama-C | Plug-in > wp | public | 2018-10-31 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jmaytac | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
We've attached a small example in which a state machine communicates a peripheral through a volatile variable , on line 6 of constants.h:
volatile uint32_t rxBuffer;
The state of the machine is held by a struct mac, declared on line 21 of mac.h:
struct mac {
mac_packet_t mac_packet;
MessageType latestMessage;
mac_bridge_t MAC_BRIDGE_A;
}
the mac_bridge_t represents the machine's memory mapped I/O interface, as declared on line 15 of mac_bridge.h:
struct mac_bridge
{
volatile uint32_t *cmd_rx_buffer;
}
on line 13 of main.c,
mac_t mac = the_mac();
mac becomes a pointer to singleton_mac instance of struct mac declared on line 8 of mac.c and returned by the function the_mac() defined on line 17 of mac.c. On line 14 of main.c,
mac->MAC_BRIDGE_A = theMacBridge();
mac's IO interface MAC_BRIDGE_A becomes the singletonMacBridgeA instance of struct mac_bridge returned by the function theMacBridge() defined on line 11 of mac.c
mac_bridge_t theMacBridge() {
singletonMacBridgeA.cmd_rx_buffer = &rxBuffer;
return &singletonMacBridgeA;
}
thus, mac has as MAC_BRIDGE_A singletonMacBridgeA whose cmd_rx_buffer is a reference to the volatile rxBuffer. The volatile rxBuffer reads and writes from ghost state as given on line 7 of constants.h:
//@ ghost uint32_t injectorAPBBuffer[4294967296];
//@ ghost uint32_t injectorAPBBufferCount=0;
/*@ ghost //@ requires buffer == &(rxBuffer);
@ uint32_t readsBuffer(volatile uint32_t *buffer) {
@ static uint32_t injectorAPBBufferCount = 0;
@ for (int i=0; i<4294967296; i++) {
@ injectorAPBBuffer[i%4294967296]=i%42949967296;
@ }
@ if (buffer == &(rxBuffer)) {
@ return injectorAPBBuffer[injectorAPBBufferCount++];
@ }
@ else
@ return 0;
@ }
@ */
//@ ghost uint32_t bufferAPBCollector[4294967296];
//@ ghost uint32_t bufferAPBCollectorCount = 0;
/*@ ghost //@ requires buffer == &(rxBuffer);
@ uint32_t writesBuffer(volatile uint32_t *buffer, uint32_t v) {
@ if (buffer == &(rxBuffer)){
@ return bufferAPBCollector[(bufferAPBCollectorCount++)%64] = v;
@ }
@ else {
@ return 0;
@ }
@ }
@*/
//@ volatile (rxBuffer) reads readsBuffer writes writesBuffer;
mac implements a transition system driven by an alphabet of labels obtained through calls to macbridge_get_packet, defined on line 3 of mac_bridge.c
mac_packet_t macbridge_get_packet(mac_bridge_t mac_bridge)
{
mac_packet_t received_packet={0};
received_packet.object_high=(uint8_t)(*(mac_bridge->cmd_rx_buffer));
return(received_packet);
}
when the given macbridge_t is the reference to the singletonMacBridgeA, we want this function to have as postcondition that the packet this function returns has the value found in the appropriate ghost state
/*@
behavior A:
assumes mac_bridge == &singletonMacBridgeA;
ensures \result.object_high == (uint8_t)injectorAPBBuffer[(injectorAPBBufferCount-1)%4294967296];
*/
mac_packet_t macbridge_get_packet(mac_bridge_t mac_bridge);
The resulting Alt-ergo doesn't seem to capture the post-condition.
(* ---------------------------------------------------------- *)
(* --- Post-condition (file mac_bridge.h, line 24) in 'macbridge_get_packet' --- *)
(* ---------------------------------------------------------- *)
goal macbridge_get_packet_post:
forall t : int farray.
forall t_1 : (addr,int) farray.
forall t_2 : (addr,addr) farray.
forall a : addr.
let a_1 = shiftfield_F7_mac_bridge_cmd_rx_buffer(a) : addr in
let a_2 = t_2[a_1] : addr in
let x = t_1[a_2] : int in
(region(a.base) <= 0) ->
framed(t_2) ->
linked(t) ->
valid_rd(t, a_1, 1) ->
is_uint32(x) ->
valid_rd(t, a_2, 1) ->
(x = to_uint8(x))
## Attachments
- [framaExample.tar.gz](/uploads/ab7c400254275ad87e4710a1a81cafe6/framaExample.tar.gz)https://git.frama-c.com/pub/frama-c/-/issues/118Mk_addr not defined in Memory.v (coqwp via why3ide)2021-02-22T12:54:05Zmantis-gitlab-migrationMk_addr not defined in Memory.v (coqwp via why3ide)ID0002414:
**This issue was created automatically from Mantis Issue 2414. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002414:
**This issue was created automatically from Mantis Issue 2414. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002414 | Frama-C | Plug-in > wp | public | 2018-12-07 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | visq | **Assigned To** | correnson | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Memory.Mk_addr is needed for Coq proofs but not in Memory.v (it *is* present in Memory.why).
As a consequence, Coq fails to compile the generated proof scripts for a null pointer check:
> Error: The reference Memory.Mk_addr was not found in the current environment.
### Additional Information :
Frama-c Argon 18.0
Coq 8.6
why3 0.88.3
### Steps To Reproduce :
cat <<EOF >id.c
/*@ requires \valid(p);
ensures *p == \old(*p);
*/
void id(int* p)
{
int tmp;
if (p == (int*)0) return;
tmp = *p;
*p = ~~tmp;
}
EOF
frama-c -wp -wp-rte -wp-split -wp-prover why3ide id.c
# Select Postcondition Line 2
# Coq
# Edit
# Replay
# => Error: The reference Memory.Mk_addr was not found in the current environment.https://git.frama-c.com/pub/frama-c/-/issues/121floating-point support is somwhat incomplete2021-02-22T12:56:27Zmantis-gitlab-migrationfloating-point support is somwhat incompleteID0002459:
**This issue was created automatically from Mantis Issue 2459. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002459:
**This issue was created automatically from Mantis Issue 2459. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002459 | Frama-C | Plug-in > wp | public | 2019-07-02 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | florian | **Assigned To** | correnson | **Resolution** | suspended |
| **Priority** | normal | **Severity** | block | **Reproducibility** | always |
| **Platform** | any | **OS** | any | **OS Version** | any |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi!
Maybe I am doing something fundamentally wrong, but I've tried some simple programs and I don't get anywhere. For example:
/*@ requires x >= 0.0f && x <= 100.0f;
*/
void float_fun(float x)
{
float y = x + 1.0f;
//@ assert y >= 1.0f;
}
I've had a look in share/frama-c/wp/why3/Cfloat.why and I'm not surprised nothing works, the axiomatisation is very incomplete, compared to the current stuff in why3. Could you please port to https://gitlab.inria.fr/why3/why3/blob/master/stdlib/ieee_float.mlw and then use a SMT solver by default that supports it natively (i.e. CVC4 or Z3)?
I know this is a bit of a drastic change, but as it stands WP is not overly useful for anyone trying to do anything with floats (e.g. control systems)...https://git.frama-c.com/pub/frama-c/-/issues/122malloc breaks reasoning about assigns2021-02-22T13:34:49Zmantis-gitlab-migrationmalloc breaks reasoning about assignsID0002455:
**This issue was created automatically from Mantis Issue 2455. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002455:
**This issue was created automatically from Mantis Issue 2455. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002455 | Frama-C | Plug-in > wp | public | 2019-06-17 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jwaksbaum | **Assigned To** | correnson | **Resolution** | suspended |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | i386 | **OS** | Darwin | **OS Version** | 18.6.0 |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
If a function contains a call to malloc, WP fails to verify its assigns clause.
This could be because malloc does assign to variables in order to track allocation state, but if so there should be a way of specifying that the function assigns to only the listed variables, as well as whatever malloc assigns to. Even duplicating the annotation on malloc will not verify, which includes assigns clauses for the malloc state variables.
### Steps To Reproduce :
# Verify a function with a call to malloc and assigns \nothing
frama-c -lib-entry -c11 -wp -wp-rte -wp-prover [...] example.c -wp-fct f
# Verify a function with the same contract as malloc, which only calls malloc
frama-c -lib-entry -c11 -wp -wp-rte -wp-prover [...] example.c wp-fct malloc_wrapper
## Attachments
- [example.c](/uploads/419009a078988ed9875d2ded26c9f430/example.c)https://git.frama-c.com/pub/frama-c/-/issues/123explain wp's syntactic restrictions on "inductive" definitions2021-02-22T12:56:27ZJochen Burghardtexplain wp's syntactic restrictions on "inductive" definitionsID0002337:
**This issue was created automatically from Mantis Issue 2337. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002337:
**This issue was created automatically from Mantis Issue 2337. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002337 | Frama-C | Documentation | public | 2017-12-14 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | text | **Reproducibility** | N/A |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
In Sect.2.6.3 "Inductive predicates" (p.50) of the manual "acsl-implementation-Sulfur-20171101.pdf", it is announced that "tools might enforce syntactic conditions on the form of inductive definitions". However, in the Wp manual (file "wp-manual-Sulfur-20171101.pdf") the string "inductive" doesn't occur at all. It should be explained there what restrictions Wp enforces on "inductive" definitions; in case it doesn't restrict them at all, this should be mentioned, too. I didn't check other plugin manuals for the occurrence of the string "inductive".
As a side remark: From a user's point of view, the freedom of each plugin to give its own semantics to (details of) ACSL constructs is confusing, and sometimes even annoying. From a software engineer's point of view, admitting too much freedom to plugins gives away the advantages of a integerated framework/plugin architecture. Having different semantics for ACSL details may compromise the interoperability of plugins.https://git.frama-c.com/pub/frama-c/-/issues/124incomplete loading of saved state when using WP?2021-02-22T14:00:16ZJens Gerlachincomplete loading of saved state when using WP?ID0002290:
**This issue was created automatically from Mantis Issue 2290. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002290:
**This issue was created automatically from Mantis Issue 2290. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002290 | Frama-C | Plug-in > wp | public | 2017-03-09 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Linux/macOS | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
When I run the line
frama-c -save swap.sav -wp -wp-rte swap.c
on the attached line and then load the saved sate with
frama-c-gui -load swap.sav
I observe the following:
1.) a message in the Frama-C-GUI:"1 state in saved file ingnored. It is invalid in this Frama-C configuration."
2.) the GUI shows which proof obligations have been verified but the tab "WP Goals" does not show any information about which prover was successful
### Additional Information :
I am not sure whether this a problem of the kernel or of the WP plug-in.
## Attachments
- [swap.c](/uploads/68eb8d47535f4c84d136f65f15dec59a/swap.c)https://git.frama-c.com/pub/frama-c/-/issues/125Shape of VC depends on selection of properties2021-09-21T13:53:03ZJens GerlachShape of VC depends on selection of propertiesID0002404:
**This issue was created automatically from Mantis Issue 2404. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002404:
**This issue was created automatically from Mantis Issue 2404. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002404 | Frama-C | Plug-in > wp | public | 2018-10-08 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | sometimes |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
WP allows to select properties by using the option -wp-prop. I have noticed the following:
When selecting a property 'foo' by -wp-prop=foo, sometimes all VCs that belong to that property are verified.
However, when I wish to verify all properties, some VC's of the property 'foo' are not verified.
This might be caused by the fact that the the actual "shape" of a VC appears to depend on -wp-prop.
(I attach an example of the slight differences between a VC that belongs to a certain property "foo" depending on whether -wp-prop=foo is used or not.)
This of course defeats somehow the purpose of using -wp-prop and it would be a welcome feature
if the generation of a VC of a property 'foo' is not affected by "-wp-prop=foo".
### Additional Information :
Is this maybe a problem of Qed?
Also, if there are several ways to generate/simplify a VC, it would be nice if one chooses one that has a higher likelihood to be verified.
## Attachments
- [diff.txt](/uploads/14ff154d537bcec5e27f7f5946ba2bfd/diff.txt)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/126Prove of \false2021-04-15T06:50:23ZJens GerlachProve of \falseID0002427:
**This issue was created automatically from Mantis Issue 2427. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002427:
**This issue was created automatically from Mantis Issue 2427. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002427 | Frama-C | Plug-in > wp | public | 2019-02-16 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
When the attached program foo.c is analysed with the command line
frama-c -pp-annot -no-unicode -wp -wp-prover alt-ergo -wp-prover eprover foo.c
then the assertion "\false" is verified with "eprover" (2.2).
To me the axiomatics and the lemma look fine which would mean that it is a problem of "eprover".
However, I would like that an WP expert has a look at it before I contact the developer of "eprover".
Thanks in advance.
### Steps To Reproduce :
I am using Frama-C 18.0, Why3 0.88.3, alt-ergo 2.2.0, eprover 2.2.
## Attachments
- [foo.c](/uploads/96dbe2588b177df6328014404f4b189f/foo.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/128Syntax error in reorder_defs.ml after running make2022-09-28T11:13:02Zmantis-gitlab-migrationSyntax error in reorder_defs.ml after running makeID0002480:
**This issue was created automatically from Mantis Issue 2480. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002480:
**This issue was created automatically from Mantis Issue 2480. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002480 | Frama-C | Plug-in > clang | public | 2019-10-03 | 2019-10-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | gpajela | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | block | **Reproducibility** | have not tried |
| **Platform** | Linux x86_64 | **OS** | Ubuntu | **OS Version** | 18.04.3 LTS |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | - |
### Description :
I am trying to follow the instructions at https://frama-c.com/frama-clang.html to install Frama-Clang. However, I get a "Syntax error" after I run make:
$ make
Generating .Makefile.plugin.generated
Ocamlc intermediate_format.cmi
Ocamlc intermediate_format_parser.cmi
Ocamlc intermediate_format_parser.cmo
Ocamlc frama_Clang_option.cmi
Ocamlc frama_Clang_option.cmo
Ocamlc fclang_datatype.cmi
Ocamlc fclang_datatype.cmo
Ocamlc reorder_defs.cmi
Ocamlc reorder_defs.cmo
File "reorder_defs.ml", line 310, characters 6-10:
Error: Syntax error
/data/loewenheim/a/gpajela/.opam/default/share/frama-c/Makefile.generic:77: recipe for target 'reorder_defs.cmo' failed
make: *** [reorder_defs.cmo] Error 2
### Additional Information :
I am using Frama-C 19.0 Potassium, which I installed using opam pin. I am using version 2.0.4 of opam. I am using the default versions of OCaml and Clang for this version of Ubuntu: OCaml 4.05.0 and clang version 6.0.0.Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/129Freelance2021-02-22T12:54:22Zmantis-gitlab-migrationFreelanceID0002477:
**This issue was created automatically from Mantis Issue 2477. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002477:
**This issue was created automatically from Mantis Issue 2477. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002477 | Frama-C | Kernel > ACSL implementation | public | 2019-09-23 | 2019-09-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | michal | **Assigned To** | virgile | **Resolution** | no change required |
| **Priority** | immediate | **Severity** | text | **Reproducibility** | sometimes |
| **Platform** | windows7 | **OS** | windows7 | **OS Version** | windows7 |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | - |
### Description :
I'm staff at fieldengineer.com,we have a technical support of telecom engineers.We created the FE Platform to streamline engagement between field engineers and businesses looking for them.https://git.frama-c.com/pub/frama-c/-/issues/130FieldEngineer2021-02-22T12:54:23Zmantis-gitlab-migrationFieldEngineerID0002476:
**This issue was created automatically from Mantis Issue 2476. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002476:
**This issue was created automatically from Mantis Issue 2476. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002476 | Frama-C | Kernel > ACSL implementation | public | 2019-09-23 | 2019-09-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | michal | **Assigned To** | virgile | **Resolution** | no change required |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | random |
| **Platform** | windows7 | **OS** | windows7 | **OS Version** | windows7 |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | - |
### Description :
I'm staff at fieldengineer.com,we have a technical support of telecom engineers.We created the FE Platform to streamline engagement between field engineers and businesses looking for them.https://git.frama-c.com/pub/frama-c/-/issues/131Can't view publications on the wiki2022-05-09T13:31:47Zmantis-gitlab-migrationCan't view publications on the wikiID0002474:
**This issue was created automatically from Mantis Issue 2474. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002474:
**This issue was created automatically from Mantis Issue 2474. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002474 | Frama-C | Documentation > website | public | 2019-09-10 | 2019-09-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | abutterfield | **Assigned To** | bobot | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Clicking the link low down on https://frama-c.com/support.html to acess the wiki to
see list of publications results in a "404 not found" error.
That link is: https://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:publications
The shorter link https://bts.frama-c.com/dokuwiki/ also fails with a 404
### Steps To Reproduce :
Try to visit https://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:publications
or https://bts.frama-c.com/dokuwiki/François BobotFrançois Bobothttps://git.frama-c.com/pub/frama-c/-/issues/134Bytecode only build fail with error 1272021-02-22T13:33:25Zmantis-gitlab-migrationBytecode only build fail with error 127ID0002473:
**This issue was created automatically from Mantis Issue 2473. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002473:
**This issue was created automatically from Mantis Issue 2473. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002473 | Frama-C | Kernel > Makefile | public | 2019-08-23 | 2019-08-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | madroach | **Assigned To** | bobot | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | amd64 bytecode only | **OS** | OpenBSD | **OS Version** | -current |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Frama-C build fine with native code compilers available, but fails to build
bytecode-only with the following error. I suspect the relevant clue is the _DEP_REDO suffix ?
Generating src/plugins/callgraph/.Makefile.plugin.generated
Generating src/plugins/metrics/.Makefile.plugin.generated
gmake[1]: Entering directory '/usr/obj/pobj/frama-c-19.0/Frama-C-snapshot-19.0'
Ocamldep src/plugins/metrics/.depend
gmake[1]: *** [src/plugins/metrics/.Makefile.plugin.generated:901: src/plugins/metrics/Metrics_DEP_REDO] Error 127
gmake[1]: Leaving directory '/usr/obj/pobj/frama-c-19.0/Frama-C-snapshot-19.0'
Ocamlc src/plugins/aorai/bool3.cmo
gmake: *** [share/Makefile.generic:78: src/plugins/aorai/bool3.cmo] Error 127
### Steps To Reproduce :
Install OCaml without native-code compilers, install dependencies, try to build Frama-C.https://git.frama-c.com/pub/frama-c/-/issues/135E-ACSL: segmentation fault on a simple strlen function2021-02-22T13:33:18Zmantis-gitlab-migrationE-ACSL: segmentation fault on a simple strlen functionID0002472:
**This issue was created automatically from Mantis Issue 2472. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002472:
**This issue was created automatically from Mantis Issue 2472. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002472 | Frama-C | Plug-in > E-ACSL | public | 2019-08-19 | 2019-08-22 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | - |
### Description :
E-ACSL successfully generates executable for this example and fails at runtime with segmentation fault error in shadow_alloca function at initialization stage.
<pre>
#include <stddef.h>
#include <stdint.h>
#include <stdio.h>
/*@ requires \exists size_t i; s[i] == '\0' && \valid_read(s+(0..i));
assigns \nothing;
ensures s[\result] == '\0';
ensures \forall size_t j; 0 <= j < \result ==> s[j] != '\0';
*/
size_t strlen(char *s)
{
size_t len;
/*@ loop invariant \forall size_t i; i < len ==> s[i] != '\0';
loop assigns len;
loop variant SIZE_MAX - len;
*/
for(len = 0; s[len] != '\0'; ++len);
return len;
}
int main(int argc, char *argv[])
{
for(int i = 0; i < argc; ++i) {
printf("%s: %d\n", argv[i], strlen(argv[i]));
}
return 0;
}
</pre>
### Additional Information :
$ gdb ./a.out.e-acsl
Temporary breakpoint 1, main (argc=1, argv=0x7fffffffd3e8) at a.out.frama.c:278
278 __e_acsl_memory_init(& argc,& argv,8UL);
Program received signal SIGSEGV, Segmentation fault.
shadow_alloca (ptr=ptr@entry=0x7fffffffd298, size=size@entry=8) at /home/work/.opam/framac/bin/../share/frama-c/e-acsl//segment_model/e_acsl_segment_tracking.h:562
562 prim_shadow[i] = (code << 2);
main function could be simple. For example, fails also in this case:
int main(void)
{
char *str = "0123456789";
printf("%s: %d\n", str, strlen(str));
return 0;
}
### Steps To Reproduce :
$ e-acsl-gcc.sh -c ./strlen.c
$ ./a.out.e-acsl
[1] 26340 segmentation fault (core dumped) ./a.out.e-acsl
## Attachments
- [strlen.c](/uploads/8cc47a4d07786ef1a83cc2d83a9ef725/strlen.c)https://git.frama-c.com/pub/frama-c/-/issues/136Crash at "hashtbl.ml", line 4622021-02-22T13:35:08Zmantis-gitlab-migrationCrash at "hashtbl.ml", line 462ID0002467:
**This issue was created automatically from Mantis Issue 2467. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002467:
**This issue was created automatically from Mantis Issue 2467. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002467 | Frama-C | Kernel | public | 2019-07-26 | 2019-08-22 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Victor Sverdlin | **Assigned To** | signoles | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | opensuse-tumbleweed | **OS Version** | 20190723 |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Raised at file "hashtbl.ml", line 462, characters 17-32
Called from file "src/libraries/project/state_topological.ml", line 62, characters 23-38
### Additional Information :
(* Frama-C journal generated at 16:46 the 26/07/2019 *)
exception Unreachable
exception Exception of string
[@@@ warning "-26"]
(* Run the user commands *)
let run () =
Project.set_keep_current false;
File.init_from_cmdline ();
Dynamic.Parameter.String.set ""
"/media/sf_home/temp/gps_try/sent_LDRA/src/main.c";
begin try
(* exception Log.AbortError("kernel") raised on: *)
File.init_from_cmdline ();
raise Unreachable
with
| Unreachable as exn -> raise exn
| exn (* Log.AbortError("kernel") *) ->
(* continuing: *)
begin try
(* exception Log.AbortError("kernel") raised on: *)
File.prepare_from_c_files ();
raise Unreachable
with
| Unreachable as exn -> raise exn
| exn (* Log.AbortError("kernel") *) ->
(* continuing: *) raise (Exception (Printexc.to_string exn))
end
end
(* Main *)
let main () =
Journal.keep_file "./.frama-c/frama_c_journal.ml";
try run ()
with
| Unreachable -> Kernel.fatal "Journal reaches an assumed dead code"
| Exception s -> Kernel.log "Journal re-raised the exception %S" s
| exn ->
Kernel.fatal
"Journal raised an unexpected exception: %s"
(Printexc.to_string exn)
(* Registering *)
let main : unit -> unit =
Dynamic.register
~plugin:"Frama_c_journal.ml"
"main"
(Datatype.func Datatype.unit Datatype.unit)
~journalize:false
main
(* Hooking *)
let () = Cmdline.run_after_loading_stage main; Cmdline.is_going_to_load ()
### Steps To Reproduce :
Just open new project and add at least one .c (or .h) file
## Attachments
- [main.c](/uploads/337a510fa380eff8f13edf74a7a7db10/main.c)https://git.frama-c.com/pub/frama-c/-/issues/137Can we calculate or extract metrics from program dependency graph generated b...2021-02-22T12:54:35Zmantis-gitlab-migrationCan we calculate or extract metrics from program dependency graph generated by frama-cID0002465:
**This issue was created automatically from Mantis Issue 2465. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002465:
**This issue was created automatically from Mantis Issue 2465. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002465 | Frama-C | Plug-in > metrics | public | 2019-07-17 | 2019-07-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ainne26 | **Assigned To** | maroneze | **Resolution** | no change required |
| **Priority** | high | **Severity** | major | **Reproducibility** | sometimes |
| **Platform** | - | **OS** | Windows , Ubuntu | **OS Version** | Windows 10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
I generate program dependency graphs of c code by using frama-c. Now I have to extract or calculate metrics from these program dependency graphs for further processing. Can frama-c calculate metrics from program dependency graphs?https://git.frama-c.com/pub/frama-c/-/issues/138tset issues in manual "acsl-implementation-Aluminium-20160501.pdf"2021-02-22T12:54:36ZJochen Burghardttset issues in manual "acsl-implementation-Aluminium-20160501.pdf"ID0002236:
**This issue was created automatically from Mantis Issue 2236. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002236:
**This issue was created automatically from Mantis Issue 2236. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002236 | Frama-C | Documentation > manuals | public | 2016-06-27 | 2019-07-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | text | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
in fig.2.7 on p.35, the alternative for set comprehension should be
"{ term | binders ..." rather than " tset | binders ... ". The next line's alternative should also use "term" rather than "tset". In the corresponding explanation for set comprehension, probably not "the union of the sets denoted by s" is meant but rather "the set of all terms denoted by s".
When the rule "location-address ::= tset" is shown on p.58 and 79, and "location ::= tset" on p.29 (BTW: I wonder whether both rules should be joined into a single one?), some remark could be given on the semantics of (a singleton containing just) a proper-expression term. For example, "assigns n*n" seems perfectly valid, when "n" is an integer variable - are such clauses forbidden, or do they have a reasonable meaning?
On p.93, in the subsection "Typing rules for sets", rule 4 and 5 appear to deviate from the syntactical form explained at subsection start. There is no \vdash in the antecedent of rule 4, and no comma right of a \vdash in any of the involved 4 lines. In rule 5's antecedent, "b \cup \Lambda" should probably read "b:bool \cup \Lambda". I also didn't understand what "tset \tau" should mean.
In Fig.2.25 on p.72, no initialisation of a model variable is admitted by the grammar (since the rule "parameter ::= type-expr id", appearing on p.49 in Fig.2.12, dosn't allow an initialization), while in example 2.61 on p.73, the model variable "forbidden" is initialized, and apparently by a tset, viz. "\empty".https://git.frama-c.com/pub/frama-c/-/issues/139grammar and implementation disagree on predicate/logic declarations2021-02-22T13:34:55ZDavid Cokgrammar and implementation disagree on predicate/logic declarationsID0002438:
**This issue was created automatically from Mantis Issue 2438. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002438:
**This issue was created automatically from Mantis Issue 2438. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002438 | Frama-C | Documentation > ACSL | public | 2019-05-22 | 2019-07-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | davidrcok | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The ACSL grammar has declarations:
//@ predicate a;
and definitions
//@ predicate a = \true;
The current grammar requires declarations to be in an axiomatic.
However the current implementation in Frama-C allows both definitions and declarations both at global scope and within axiomatics.
I propose changing the ACSL documentation/grammar to match current behavior.
Similarly axioms should be allowed both inside and outside axiomatics.