frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T14:00:16Zhttps://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/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/3[wp] shall use per-behaviour assigns at call sites2021-08-05T08:49:16ZNikolai Kosmatov[wp] shall use per-behaviour assigns at call sites# Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *20.0 (Calcium)* (as reported by `frama-c -version`)
- Plug-in used: *WP*
- OS name: *Ubuntu*
- OS version: *19.10*
*Please add specific information deemed...# Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *20.0 (Calcium)* (as reported by `frama-c -version`)
- Plug-in used: *WP*
- OS name: *Ubuntu*
- OS version: *19.10*
*Please add specific information deemed relevant with regard to this issue.*
# Steps to reproduce the issue
frama-c-gui -wp behavior_assigns.c
*Please indicate here steps to follow which reproduce the issue.*
See the attached file for a minimal example. [behavior_assigns.c](/uploads/b4eaee1cce8750d4749d64794e79883c/behavior_assigns.c)
# Expected behaviour
The assigns clause of caller can be proved.
# Actual behaviour
The assigns clause of caller is not proved.
The assigns clauses specific for particular behaviors in a callee cannot be used in the caller
under specific conditions falling into such behavior(s) to prove a more restrictive assigns clause
in the caller, rather than the most general assigns taking into account all behaviors of the callee.
# Fix ideas
Obvious workarounds include additional postconditions, that make the specifications more complex and
make the proof with WP less powerful. Matching the callee's behaviors to prove stronger assigns clauses
in the caller could be helpful.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2[wp] non-provable local typing constraints in lemmas2021-05-28T09:30:55ZJens Gerlach[wp] non-provable local typing constraints in lemmas# Steps to reproduce the issue
The attached archive contains the ACSL function `Count` together with several lemma.
Also contained are
- a Makefile
- a coq proof in file `wp0.script.20` for lemma `CountBounds` that works for Frama-C 20...# Steps to reproduce the issue
The attached archive contains the ACSL function `Count` together with several lemma.
Also contained are
- a Makefile
- a coq proof in file `wp0.script.20` for lemma `CountBounds` that works for Frama-C 20
- an attempt of a coq proof in file `wp0.script.21` for lemma `CountBounds` that fails for Frama-C 21
- The files `CountBounds.v.20` and `CountBounds.v.21` contain the coq code as extracted from CoqIde
# Expected behaviour
My problem is that I am unable to adapt the coq proof that worked fro Frama-C 20 to the newer version of Frama-C.
# Actual behaviour
I suspect that this is related to changes in the generated Coq code of the VC of lemma `CountBounds`
This can be best seen when calling `diff CountBounds.v.20 CountBounds.v.21`.
```
$ diff CountBounds.v.20 CountBounds.v.21
39,40c39,40
< (((t.[ (shift_sint32 a x) ]) <> i_2)%Z) -> ((i < i_1)%Z) ->
< ((is_sint32 i_2%Z)) ->
---
> let x_1 := (t.[ (shift_sint32 a x) ])%Z in ((x_1 <> i_2)%Z) ->
> ((i < i_1)%Z) -> ((is_sint32 i_2%Z)) -> ((is_sint32 x_1)) ->
```
# Fix ideas
I think the issue is caused by the condition `((is_sint32 x_1))` for the newly introduced term `x_1 := (t.[ (shift_sint32 a x) ])%Z`. I haven't found a way to satisfy the condition `((is_sint32 x_1))` and I suspect that it is not possible.
If it is possible, then I apologise and ask for a hint.
Regards
Jens Gerlach
[CoqFramac21.tar](/uploads/e95b883ad30f134748c5a7289fa6902d/CoqFramac21.tar)Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/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/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/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/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/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/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/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/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/159Ambiguous path error using why32021-02-22T12:55:18Zmantis-gitlab-migrationAmbiguous path error using why3ID0002454:
**This issue was created automatically from Mantis Issue 2454. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002454:
**This issue was created automatically from Mantis Issue 2454. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002454 | Frama-C | Plug-in > wp | public | 2019-06-17 | 2019-06-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jwaksbaum | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | i386 | **OS** | Darwin | **OS Version** | 18.6.0 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Why3 errors on the generated goals produce by w3 on certain inputs with the following message:
Ambiguous path:
both /nix/store/nf4sbv0j6dc0grks7iplf9byv989mjg5-why3-0.88.3/share/why3/modules/Matrix.mlw
and /var/folders/2j/dbl_p0mj3rgd879z8nt7r4600000gp/T/wpdeac45.dir/typed/Matrix.why
### Steps To Reproduce :
Why3 errors on the generated goals produce by w3 on certain inputs with the following message:
Ambiguous path:
both /nix/store/nf4sbv0j6dc0grks7iplf9byv989mjg5-why3-0.88.3/share/why3/modules/Matrix.mlw
and /var/folders/2j/dbl_p0mj3rgd879z8nt7r4600000gp/T/wpdeac45.dir/typed/Matrix.why
## Attachments
- [example.c](/uploads/ba254a88318716a5e0665ff9fe46d1f4/example.c)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/151number of generated files in Frama-C 18 vs 19. beta(2)2021-02-22T12:54:59ZJens Gerlachnumber of generated files in Frama-C 18 vs 19. beta(2)ID0002453:
**This issue was created automatically from Mantis Issue 2453. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002453:
**This issue was created automatically from Mantis Issue 2453. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002453 | Frama-C | Plug-in > wp | public | 2019-06-14 | 2019-07-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | bobot | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C 19-Potassium |
### Description :
This entry references issue
https://github.com/Frama-C/Frama-C-snapshot/issues/21
in order to be able to easily add files.
### Steps To Reproduce :
Run the command
frama-c -pp-annot -no-unicode -wp -wp-rte -warn-unsigned-overflow -warn-unsigned-downcast -wp-model Typed+ref -wp-out rc.wp rc.c
on the attached files.
As mentioned in the github issue, both 18.0 and 19.beta(2) report 17 VC of which 5 are discharged by Qed and the remaining 12 are verified by Alt-Ergo.
However, Frama-C 18.0 generates 12 .mlw and .out files, respectively.
Frama-C 19 beta2, on the other hand, only generates 9 .mlw and .out files, respectively.
The latter behaviour confuses our internal evaluation scripts which report that only 9 of the remaining 12 proof obligations have been discharged by Alt-Ergo.
## Attachments
- [rc.c](/uploads/12c6518483a56dad661d3ee7feabf59b/rc.c)https://git.frama-c.com/pub/frama-c/-/issues/168Division by zero doesn't increase the number of VC in console output2021-02-22T12:55:28Zmantis-gitlab-migrationDivision by zero doesn't increase the number of VC in console outputID0002428:
**This issue was created automatically from Mantis Issue 2428. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002428:
**This issue was created automatically from Mantis Issue 2428. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002428 | Frama-C | Plug-in > wp | public | 2019-02-17 | 2019-02-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Obvious division by zero doesn't increase the total number of proof obligations:
Test2:
<pre>
/*@ assigns \nothing;
*/
int test2(int a)
{
return a / 0;
}
</pre>
Frama-C:
<pre>
[kernel] Parsing test2.c (with preprocessing)
[rte] annotating function test2
[rte] test2.c:5:8: Warning: guaranteed RTE: assert division_by_zero: 0 ≢ 0;
[wp] 1 goal scheduled
[wp] Proved goals: 1 / 1
Qed: 1
</pre>
Proved goals line is the same as in the case without division:
Test1:
<pre>
/*@ assigns \nothing;
*/
int test1(int a)
{
return a;
}
</pre>
Frama-C output:
<pre>
[kernel] Parsing test1.c (with preprocessing)
[rte] annotating function test1
[wp] 1 goal scheduled
[wp] Proved goals: 1 / 1
Qed: 1
</pre>
From my point of view this is an incorrect behavior and the proved goals like should be 'Proved goals: 1 / 2' as in this case:
Test3:
<pre>
/*@ assigns \nothing;
*/
int test3(int a)
{
//@ assert 0 != 0;
return a / 0;
}
</pre>
Frama-C:
<pre>
[kernel] Parsing test3.c (with preprocessing)
[rte] annotating function test3
[rte] test3.c:6:8: Warning: guaranteed RTE: assert division_by_zero: 0 ≢ 0;
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_test3_assert : Unknown (109ms)
[wp] Proved goals: 1 / 2
Qed: 1
Alt-Ergo: 0 (unknown: 1)
</pre>
## Attachments
- [test2.c](/uploads/6a8a966174608d26a4e3aaca44d430f1/test2.c)https://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/169One \valid seems sufficient to write in a whole array.2021-02-22T12:55:31Zmantis-gitlab-migrationOne \valid seems sufficient to write in a whole array.ID0002426:
**This issue was created automatically from Mantis Issue 2426. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002426:
**This issue was created automatically from Mantis Issue 2426. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002426 | Frama-C | Plug-in > wp | public | 2019-02-12 | 2019-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | VincentPenelle | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Linux | **OS** | Linux Manjaro | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
I am on Chlorine version.
When I try to verify the following function with RTE guard enabled, WP succeeds. However, I think it should not, as only the first cell is specified to be valid, the rest is just specified to have valid read.
/*@ requires \valid(a);
@ requires \valid_read(a + (0 .. n-1));
@ requires 0 <= n <= INT_MAX;
*/
void foo(int *a, int n){
/*@ loop invariant 0 <= i <= n;
@ loop invariant \valid(a + (0 .. n-1));
*/
for (int i = 0; i<n;i++) a[i] = i;
}
Note: that works as well without any loop.
It doesn't work if you declare to pointers with different names, and declare one to be \valid and the other to be \valid_read (like in swap function for example).
It looks like the loop invariant \valid is simplified to true by Qed.
If that's normal, please explain me why.
Thanks,
--
Vincent Penelle.
### Steps To Reproduce :
Specify an array as being \valid_read, and one of its cells to be \valid.
Then, try to write in any cell.
Generate the RTE guards. WP should succeed to prove that the cells you're writing in are \valid.https://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)