frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2022-09-22T08:58:47Zhttps://git.frama-c.com/pub/frama-c/-/issues/2629Anomalous behavior of anonymous 'behavior'2022-09-22T08:58:47ZDavid CokAnomalous behavior of anonymous 'behavior'
### Steps to reproduce the issue
See this code:
```
int P;
int Q;
/*@
requires P != 0;
behavior always:
assigns Q;
ensures Q == 1;
complete behaviors always;
*/
void b() {
Q = 1;
}
//@ assigns Q;
void a() {
b();
}
...
### Steps to reproduce the issue
See this code:
```
int P;
int Q;
/*@
requires P != 0;
behavior always:
assigns Q;
ensures Q == 1;
complete behaviors always;
*/
void b() {
Q = 1;
}
//@ assigns Q;
void a() {
b();
}
/*@
requires P != 0;
assigns Q;
ensures Q == 1;
*/
void d() {
Q = 1;
}
//@ assigns Q;
void c() {
d();
}
```
which is an minimal as I could make it.
Note that a calls b, where b has a always-true behavior. c calls d the same way, but without a behavior.
The example is extracted from a larger specification with lots of behaviors.
### Actual behaviour
In my environment, the above, run with `frama-c -wp` produces
```
fc $ frama-c -wp behavior.c
[kernel] Parsing behavior.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 11 goals scheduled
[wp] [Alt-Ergo 2.4.1] Goal typed_a_assigns_exit : Timeout (Qed:0.81ms) (10s)
[wp] [Alt-Ergo 2.4.1] Goal typed_a_call_b_requires : Timeout (Qed:0.78ms) (10s)
[wp] [Alt-Ergo 2.4.1] Goal typed_a_assigns_normal : Timeout (Qed:0.77ms) (10s)
[wp] [Alt-Ergo 2.4.1] Goal typed_c_call_d_requires : Timeout (10s)
[wp] Proved goals: 7 / 11
Qed: 7
Alt-Ergo 2.4.1: 0 (interrupted: 4)
```
That is c calling d is fine. a calling b is not.
### Expected behaviour
I expect a calling be to behave precisely like c calling d.
It appears that even with a prefix consisting of just requires clauses, WP produces an
anonymous behavior that contains something like `assigns \everything`. That then causes
the very mysterious assigns errors that you see above.
Fortunately, now that I know the problem there is an easy workaround -- but prior to that it wasted many days of time.
### Contextual information
Frama-C 25.0, built from source, with WP
MacOS 12.5Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1173ACSL label LoopEntry not handled by WP2022-10-06T14:57:24Zmantis-gitlab-migrationACSL label LoopEntry not handled by WPID0001353:
**This issue was created automatically from Mantis Issue 1353. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001353:
**This issue was created automatically from Mantis Issue 1353. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001353 | Frama-C | Plug-in > wp | public | 2013-01-30 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
As said in the title, the ACSL label LoopEntry seems to be not handled by WP but it is accepted by the kernel.
Using the -wp-warnings option I got warnings like :
- Warning: Generalization of un-labeled values
Reason: Some labels may escape the control flow
but it took me some time to understand the problem.
In the example below, changing LoopEntry by L in the loop invariant makes it work.
BTW, in the example below, it doesn't work either when removing the first (c++;) statement !
### Additional Information :
int G;
//@ requires G == 0; ensures G == 0;
void f (int c) {
c++;
L: //@ loop invariant G == \at (G, LoopEntry);
while (c) c++;
}https://git.frama-c.com/pub/frama-c/-/issues/2636[WP] Builtin \sign(float64) is not defined2022-12-14T12:36:37ZNiksonber[WP] Builtin \sign(float64) is not defined<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Description
Built-in \\sign is not defined in WP.
`Builtin \sign(float64) not defined`
`[wp] Failure: Logic type 'sign' undefined`
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
### Steps To Reproduce
Run: `frama-c -wp -wp-out . -wp-prover coq -wp-model +float -wp-interactive update just_sign.c`
Where `just_sign.c` is:
```
#include <math.h>
/*@
predicate is_same_sign(double X, double Y) = \sign(X) == \sign(Y);
*/
/*@
ensures (is_same_sign(a_double, \result)) ;
assigns \nothing;
*/
double dummy (double a_double) {
return a_double;
}
```
I got the following output:
```
[wp] Warning: Missing RTE guards
[wp] just_sign.c:4: Warning: Builtin \sign(float64) not defined
[wp] just_sign.c:4: Warning: Builtin \sign(float64) not defined
[wp] 2 goals scheduled
[wp] Failure: Logic type 'sign' undefined
```
### Expected behaviour
Expected a definition for \sign.
<!--
Please explain here what is the expected behaviour.
-->
### Actual behaviour
WP reports:
```
[wp] Failure: Logic type 'sign' undefined
[wp] just_sign.c:4: Warning: Builtin \sign(float64) not defined
```
<!--
Please explain here what is the actual (faulty) behaviour.
-->
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 24.0, 25.0 (Manganese), 26.0+dev (Iron) (I tried Several versions)
- Plug-in used: WP
- OS name: Ubuntu
- OS version: 22.04 LTS
<!--
### Additional information (optional)
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/1195Qedlib.v definition of tactic "replace by" clashes with standard tactic "repl...2023-01-04T11:04:20ZJens GerlachQedlib.v definition of tactic "replace by" clashes with standard tactic "replace with"ID0001626:
**This issue was created automatically from Mantis Issue 1626. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001626:
**This issue was created automatically from Mantis Issue 1626. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001626 | Frama-C | Plug-in > wp | public | 2014-01-22 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
I cannot use the standard coq tactic "replace with" because it clashes (apparently with
"replace by" defined in Qedlib.v)
### Steps To Reproduce :
Just try to use "replace A by B" in a coq proof of a wp proof obligationhttps://git.frama-c.com/pub/frama-c/-/issues/2644[WP] Fails to verify left shift by 2 on range2023-01-24T11:13:25ZCostava[WP] Fails to verify left shift by 2 on range<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
```c
/*@
requires a == 1;
assigns \nothing;
ensures \result == (a << 2);
*/
unsigned int do_one(const unsigned int a) {
return (a << 2);
}
/*@
requires a == 2;
assigns \nothing;
ensures \result == (a << 2);
*/
unsigned int do_two(const unsigned int a) {
return (a << 2);
}
/*@
requires 1 <= a <= 2;
assigns \nothing;
ensures \result == (a << 2);
*/
unsigned int do_some_shift2(const unsigned int a) {
return (a << 2);
}
/*@
requires 1 <= a <= 2;
assigns \nothing;
ensures \result == (a << 1);
*/
unsigned int do_some_shift1(const unsigned int a) {
return (a << 1);
}
```
```sh
$ frama-c -wp -wp-rte fcshift.c
```
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
All goals verified successfully.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
```sh
$ frama-c -wp -wp-rte fcshift.c
[kernel] Parsing fcshift.c (with preprocessing)
[rte:annot] annotating function do_one
[rte:annot] annotating function do_some_shift1
[rte:annot] annotating function do_some_shift2
[rte:annot] annotating function do_two
[wp] 8 goals scheduled
[wp] [Alt-Ergo 2.4.1] Goal typed_do_some_shift2_ensures : Timeout (Qed:2ms) (10s)
[wp] Proved goals: 7 / 8
Qed: 6 (0.33ms-0.64ms-2ms)
Alt-Ergo 2.4.1: 1 (10ms) (92) (interrupted: 1)
```
The ensures goal can be verified when `a` has a single value of either `1` or `2` respectively for the `do_one` and `do_two` functions.
But if `a` is `1` or `2` (for function `do_some_shift2`), then the ensures goal fails to verify.
Oddly, the goal succeeds if the left shift is by `1` instead of `2` (function `do_some_shift1`).
[cppreference.com](https://en.cppreference.com/w/c/language/arithmetic_types) is stating that `unsigned int` should always have at least 16 bits, so it is weird to me that changing the amount of the shift is making a difference.
Doubling the timeout to 20 does not make the goal succeed automatically.
Using `frama-c-gui`, I know that I can apply tactic `Logical Shift` on `lsl(a, 2)` in order to make the goal succeed, but a goal that is this specific and simple failing to verify seems like a bug.
### Contextual information
- Frama-C installation mode: opam
- Frama-C version: 25.0 (Manganese)
- Plug-in used: WP, RTE, Alt-Ergo 2.4.1
- OS name: Manjaro Linux
- OS version: Sikaris 22.0.0
### Additional information (optional)
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->
N/ALoïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1192Bug in let-elimination (due to <==> and assert false).2023-02-03T12:18:59ZLoïc CorrensonBug in let-elimination (due to <==> and assert false).ID0001586:
**This issue was created automatically from Mantis Issue 1586. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001586:
**This issue was created automatically from Mantis Issue 1586. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001586 | Frama-C | Plug-in > wp | public | 2013-12-16 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | correnson | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
Bug in let-elimination (due to <==> and assert false).
Using -wp-no-let makes the assert false not-proved as expected.
### Additional Information :
In the attached program, we have no assumption and everything is proved
with WP (Frama-C Fluorine June), including the assert 1==2 in case N!
frama-c-gui -pp-annot -wp -wp-rte q19_switch_fun_call.c
It appears that the issue is coming from the equivalences used in the
behaviours of compute_trans(). If we replace "<==>" by "==>", then the
1==2 assert is not proved (substitute call to compute_trans() by
compute_trans2() in main()).
In both cases (compute_trans() and compute_trans2()), the contract is
always proved.
## Attachments
- [q19_switch_fun_call.c](/uploads/fa377321dbdcb32a2de9f013fc50164f/q19_switch_fun_call.c)
- [q20_switch_fun_call.c](/uploads/3a712d89800fa2c38926aac03f141f57/q20_switch_fun_call.c)https://git.frama-c.com/pub/frama-c/-/issues/1226WP Plugin with Alt-Ergo - unable to prove?2023-03-06T17:48:30Zmantis-gitlab-migrationWP Plugin with Alt-Ergo - unable to prove?ID0001601:
**This issue was created automatically from Mantis Issue 1601. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001601:
**This issue was created automatically from Mantis Issue 1601. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001601 | Frama-C | Plug-in > wp | public | 2014-01-13 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dharma | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | urgent | **Severity** | block | **Reproducibility** | always |
| **Platform** | Ubuntu | **OS** | Linux | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
I'm trying to test WP plugin with Alt-Ergo on a fairly complex function. Unfortunately, I am not able to figure out what's wrong with the "basic" behavior given below.
This behavior should be true because there is no other place tenumRMode is updated except the first conditional statement's else section.
The weird thing is that if I comment some lines arbitrarily (after the first if-else block) I always get "valid" from Alt-ergo.
Any comments? The below code might be lengthy, but the behavior is easy to verify manually because the variables mentioned in the behavior are never updated after the first if-else block.
I also discussed with a alt-ergo developer, see http://stackoverflow.com/questions/21036098/wp-plugin-with-alt-ergo-unable-to-prove
### Steps To Reproduce :
/*@ behavior basic:
@ assumes fRrValue == 0;
@ ensures tenumRMode == SS_A_MODE;
@
*/
$ frama-c -wp -wp-rte -wp-bhv=basic foo.c -wp-out t -lib-entry -main foo -wp-model ref -wp-timeout=50 -wp-fct=foo -wp-out t
[kernel] preprocessing with "gcc -C -E -I. foo.c"
[wp] Running WP plugin...
[rte] annotating function foo
[wp] Collecting axiomatic usage
[wp] Collecting variable usage
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_ref_foo_basic_post : Unknown (Qed:20ms)
typedef unsigned char BOOL;
#define TRUE 1
#define FALSE 0
typedef unsigned char uint8;
typedef unsigned short int uint16;
typedef unsigned long uint32;
uint16 F_MIN_R = 15;
const uint8 RESP_STATE = 30;
typedef enum
{
RESP_MODE,
SS_A_MODE
}tenumMode;
tenumMode tenumRMode;
BOOL gbCaMStatus;
BOOL gbCaaStatus;
uint8 mnPb;
BOOL mbApLYRange;
BOOL mbApLRange;
float gfApYLineSlope;
float gfApYLineConst;
float gfApRLineSlope;
float gfApRLineConst;
float mfAp;
uint16 almC;
uint16 nApLYL = 0;
uint16 nApLRL = 0;
uint16 Ap_Y_L_Ui = 0;
uint16 Ap_R_L_Ui = 0;
float fCaValue=0.0;
float fRrValue = 0.0;
uint16 nCaLYL=0;
uint16 nCaLRL=0;
/*@ behavior basic:
@ assumes fRrValue == 0;
@ ensures tenumRMode == SS_A_MODE;
@
*/
void foo()
{
float mfNewAp = 0;
BOOL bYAp = FALSE;
BOOL bRAp = FALSE;
BOOL bApAlmC = FALSE;
if (fRrValue != 0)
{
/* Some code here */
}
else
{
if (mnPb == 1)
{
mfAp = RESP_STATE;
mnPb = 2;
}
tenumRMode = SS_A_MODE;
}
if ( (mfAp >= F_MIN_R) &&
((gbCaMStatus == TRUE) && (gbCaaStatus == FALSE)) )
{
bApAlmC = TRUE;
almC = 1;
}
else
{
almC = 0;
}
if ( (bApAlmC == TRUE)
&& (mfAp < nApLYL)
&& (fCaValue >= nCaLYL) )
{
float fmultval = 0;
fmultval = gfApYLineSlope*fCaValue;
mfNewAp = fmultval + gfApYLineConst;
if (mfAp >= mfNewAp)
bYAp = TRUE;
else
bYAp = FALSE;
Ap_Y_L_Ui = (uint16)mfNewAp;
}
if ((bApAlmC == TRUE) && (fCaValue > (float)nCaLYL))
{
mfNewAp = ((gfApYLineSlope*fCaValue) + gfApYLineConst);
if (mfNewAp < (float)nApLYL);
Ap_Y_L_Ui = (uint16)mfNewAp;
}
else if ((bApAlmC == TRUE) && (fCaValue <= (float)nCaLYL))
Ap_Y_L_Ui = F_MIN_R;
if ( (bApAlmC == TRUE) && (fCaValue >= nCaLRL) )
{
float fmultval = 0;
fmultval = gfApRLineSlope*fCaValue;
mfNewAp = fmultval + gfApRLineConst;
if (mfAp >= mfNewAp)
bRAp = TRUE;
else
bRAp = FALSE;
Ap_R_L_Ui = (uint16)mfNewAp;
}
else if ( (bApAlmC == TRUE) && (fCaValue < nCaLRL) )
Ap_R_L_Ui = F_MIN_R;
if ( (mfAp >= nApLYL)
|| ((bApAlmC == TRUE) && (fCaValue < nCaLYL))
|| ((bYAp == TRUE)
&& (gbCaMStatus == TRUE) && (gbCaaStatus == FALSE) ) )
{
mbApLYRange = TRUE;
}
else
mbApLYRange = FALSE;
if ( (mfAp >= nApLRL)
|| ((bApAlmC == TRUE) && (fCaValue < nCaLRL))
|| ((bRAp == TRUE)
&& (gbCaMStatus == TRUE) && (gbCaaStatus == FALSE) ) )
{
/* Some code here */
}
}https://git.frama-c.com/pub/frama-c/-/issues/1230WP: This term has type real but is expected to have type int2023-03-09T16:58:29Zmantis-gitlab-migrationWP: This term has type real but is expected to have type intID0001622:
**This issue was created automatically from Mantis Issue 1622. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001622:
**This issue was created automatically from Mantis Issue 1622. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001622 | Frama-C | Plug-in > wp | public | 2014-01-20 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dharma | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | high | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
Hi,
I'm not sure "This term has type real but is expected to have type int" when using WP with Z3 (Z3 version 4.3.1).
Please note that I do not have this error when I used alt-ergo (0.95.2).
$ frama-c -wp-proof=z3 -wp -wp-rte foo.c -wp-fct=foo -wp-bhv=basic -wp-out=t -pp-annot
[kernel] preprocessing with "gcc -C -E -I. -dD foo.c"
[wp] Running WP plugin...
[rte] annotating function foo
[wp] Collecting axiomatic usage
[wp] 1 goal scheduled
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
File "t/typed/foo_Why3_ide.why", line 60, characters 14-17:
This term has type real but is expected to have type int
------------------------------------------------------------
[wp] [Z3] Goal typed_foo_basic_post : Failed
Error: Why3 exits with status [1]
### Steps To Reproduce :
The generated why file is attached for your reference. foo.c is given below.
typedef unsigned char BOOL;
#define TRUE 1
#define FALSE 0
typedef unsigned char uint8;
typedef unsigned short int uint16;
typedef unsigned long uint32;
uint16 F_MIN_R = 15;
const uint8 RESP_STATE = 30;
typedef enum
{
RESP_MODE,
SS_A_MODE
}tenumMode;
tenumMode tenumRMode;
BOOL gbCaMStatus;
BOOL gbCaaStatus;
uint8 mnPb;
BOOL mbApLYRange;
float gfApYLineSlope;
float gfApYLineConst;
float gfApRLineSlope;
float gfApRLineConst;
float mfAp;
uint16 almC;
uint16 nApLYL = 0;
uint16 nApLRL = 0;
uint16 Ap_Y_L_Ui = 0;
uint16 Ap_R_L_Ui = 0;
float fCaValue=0.0;
float fRrValue = 0.0;
uint16 nCaLYL=0;
uint16 nCaLRL=0;
/*@
@ behavior basic:
@ assumes fRrValue == 0;
@ ensures tenumRMode == SS_A_MODE;
@
*/
void foo()
{
float mfNewAp = 0;
BOOL bYAp = FALSE;
BOOL bRAp = FALSE;
BOOL bApAlmC = FALSE;
if (fRrValue != 0)
{
/* Some code here */
}
else
{
if (mnPb == 1)
{
mfAp = RESP_STATE;
mnPb = 2;
}
tenumRMode = SS_A_MODE;
}
//@ assert fRrValue == 0.0 ==> tenumRMode == SS_A_MODE;
if ( (mfAp >= F_MIN_R) &&
((gbCaMStatus == TRUE) && (gbCaaStatus == FALSE)) )
{
bApAlmC = TRUE;
almC = 1;
}
else
{
almC = 0;
}
//@ assert fRrValue == 0.0 ==> tenumRMode == SS_A_MODE;
if ( (bApAlmC == TRUE)
&& (mfAp < nApLYL)
&& (fCaValue >= nCaLYL) )
{
float fmultval = 0;
fmultval = gfApYLineSlope*fCaValue;
mfNewAp = fmultval + gfApYLineConst;
if (mfAp >= mfNewAp)
bYAp = TRUE;
else
bYAp = FALSE;
Ap_Y_L_Ui = (uint16)mfNewAp;
}
//@ assert fRrValue == 0.0 ==> tenumRMode == SS_A_MODE;
if ((bApAlmC == TRUE) && (fCaValue > (float)nCaLYL))
{
mfNewAp = ((gfApYLineSlope*fCaValue) + gfApYLineConst);
if (mfNewAp < (float)nApLYL);
Ap_Y_L_Ui = (uint16)mfNewAp;
}
else if ((bApAlmC == TRUE) && (fCaValue <= (float)nCaLYL))
Ap_Y_L_Ui = F_MIN_R;
if ( (bApAlmC == TRUE) && (fCaValue >= nCaLRL) )
{
float fmultval = 0;
fmultval = gfApRLineSlope*fCaValue;
mfNewAp = fmultval + gfApRLineConst;
if (mfAp >= mfNewAp)
bRAp = TRUE;
else
bRAp = FALSE;
Ap_R_L_Ui = (uint16)mfNewAp;
}
else if ( (bApAlmC == TRUE) && (fCaValue < nCaLRL) )
Ap_R_L_Ui = F_MIN_R;
//@ assert fRrValue == 0.0 ==> tenumRMode == SS_A_MODE;
if ( (mfAp >= nApLYL)
|| ((bApAlmC == TRUE) && (fCaValue < nCaLYL))
|| ((bYAp == TRUE)
&& (gbCaMStatus == TRUE) && (gbCaaStatus == FALSE) ) )
{
mbApLYRange = TRUE;
}
else
mbApLYRange = FALSE;
//@ assert fRrValue == 0.0 ==> tenumRMode == SS_A_MODE;
if ( (mfAp >= nApLRL)
|| ((bApAlmC == TRUE) && (fCaValue < nCaLRL))
|| ((bRAp == TRUE)
&& (gbCaMStatus == TRUE) && (gbCaaStatus == FALSE) ) )
{
}
//@ assert fRrValue == 0.0 ==> tenumRMode == SS_A_MODE;
}
## Attachments
- [foo_Why3_ide.why](/uploads/1e4aa501f0fc2649d40235d8589c9976/foo_Why3_ide.why)https://git.frama-c.com/pub/frama-c/-/issues/2650Stack overflow using WP in Wp__Register.step_finally2023-03-29T20:08:35ZChristophe GarionStack overflow using WP in Wp__Register.step_finallyFrama-C 26.1 and its WP plugin crash with a stack overflow when trying to prove a function:
```
The full backtrace is:
Raised at Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 834, characters 41-48
Called fro...Frama-C 26.1 and its WP plugin crash with a stack overflow when trying to prove a function:
```
The full backtrace is:
Raised at Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 834, characters 41-48
Called from Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 835, characters 2-12
Called from Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 835, characters 2-12
Called from Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 835, characters 2-12
Called from Stdlib__Queue.iter.iter in file "queue.ml", line 121, characters 6-15
Called from Frama_c_boot__Boot.play_analysis in file "src/init/boot/boot.ml", line 36, characters 4-20
Called from Frama_c_kernel__Cmdline.play_in_toplevel_one_shot in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 850, characters 2-9
Called from Frama_c_kernel__Cmdline.play_in_toplevel in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 880, characters 18-64
Called from Frama_c_kernel__Cmdline.catch_toplevel_run in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 233, characters 4-8
Unexpected error (Stack overflow).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 26.1 (Iron).
```
The function to be proved is part of a rather big C file included in the attached archive. Sorry for the complexity (and maybe the bad quality) of the C code, it is in fact produced by a Lustre compiler we are working on. I will try to produce a real MWE...
Running Frama-C and WP on the whole file causes a stack overflow on `List.map` but I reduce the error when proving the `Arrays1_Arrays1_node_step` function. I use the `ref` and the `real` memory model.
When launching Frama-C on the function, no goal is produced (at least there is no printing of it), only Frama-C is running (there is no process involving Alt-Ergo or Z3 for instance). the crash happens after 13 minutes (!) on my computer (a recent laptop with i9 cores).
### Steps to reproduce the issue
* open the attached archive
* issue the following command:
```
frama-c -wp -wp-model ref,real -wp-fct Arrays1_Arrays1_node_step Arrays1.c
```
### Contextual information
- Frama-C installation mode: opam with an OCaml 4.14.0 switch
- Frama-C version: 26.1 (Iron)
- Plug-in used: WP
- OS name: Linux
- OS version: 22.04
Thanks,
Christophe
[arrays_stack_overflow_wo_optimization.tgz](/uploads/e88a0fcabd4de811d59024517c679f5d/arrays_stack_overflow_wo_optimization.tgz)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2657frama-c-gui frozen and why3 not found2023-04-13T14:44:13ZRongframa-c-gui frozen and why3 not found### Problem Description ###
When running `opam install alt-ergo`, my terminal shows:
```
Package alt-ergo is already installed (current version is 2.4.2).
```
However, when running `frama-c-gui -wp -rte -main.c`, the terminal shows:
...### Problem Description ###
When running `opam install alt-ergo`, my terminal shows:
```
Package alt-ergo is already installed (current version is 2.4.2).
```
However, when running `frama-c-gui -wp -rte -main.c`, the terminal shows:
```
(frama-c-gui:4023): GLib-CRITICAL **: 09:36:25.664: Source ID 8 was not found when attempting to remove it.
```
The GUI is opened but frozen. No clicking is responded and the console shows `User Error: Prover 'alt-ergo' not found in why3.conf.`
### Steps to reproduce the issue
frama-c-gui -wp -rte -main.c
### Expected behaviour
open the window of frama-c-gui and run normally
### Actual behaviour
The GUI is opened but frozen. No clicking is responded and the console shows `User Error: Prover 'alt-ergo' not found in why3.conf.`
### Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *frama-c.26.1*
- Plug-in used: *Plug-in used*
- OS name: *Ubuntu*
- OS version: *22.04.2 LTS*
### Additional information (optional)
After running "opam upgrade", the following information appears:
```
Everything as up-to-date as possible (run with --verbose to show unavailable upgrades).
The following packages are not being upgraded because the new versions conflict with other installed packages:
- ocaml-config.3
- ocplib-simplex.0.5
∗ alt-ergo-lib.2.4.2 is installed and requires ocplib-simplex (>= 0.4 & < 0.5)
- why3.1.6.0
∗ frama-c.26.1 is installed and requires why3 (>= 1.5.1 & < 1.6~)
However, you may "opam upgrade" these packages explicitly, which will ask permission to downgrade or uninstall the conflicting packages.
Nothing to do.
# Run eval $(opam env) to update the current shell environment
```https://git.frama-c.com/pub/frama-c/-/issues/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/2631Naming the anonymous behavior for -wp-bhv2023-06-21T08:58:19ZDavid CokNaming the anonymous behavior for -wp-bhvFeature request (or perhaps just information):
in using WP, the -wp-bhv option works fine for named behaviors. But how does one indicate to check just the anonymous behavior?
If there is no way currently, then please add some syntax tha...Feature request (or perhaps just information):
in using WP, the -wp-bhv option works fine for named behaviors. But how does one indicate to check just the anonymous behavior?
If there is no way currently, then please add some syntax that does not interfere with most shells. For example -wp-bhv ~Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2663Parse-print-reparse error with WP strategies2023-07-21T09:11:17ZNikolai KosmatovParse-print-reparse error with WP strategies## Contextual information: currently used versions
- Frama-C installation mode: *Opam*
- Frama-C version 27.0dev (tested commit: 3396bd)
- Alt-Ergo 2.4.3
- OS name: *Ubuntu*
- OS version: *20.04*
## The issue
On the attached file, aft...## Contextual information: currently used versions
- Frama-C installation mode: *Opam*
- Frama-C version 27.0dev (tested commit: 3396bd)
- Alt-Ergo 2.4.3
- OS name: *Ubuntu*
- OS version: *20.04*
## The issue
On the attached file, after parsing and printing the code, running frama-c again to parse the code produces an error (due to missing parentheses around a list of arguments (..)).
[strategy.c](/uploads/d089f42a7b3f32480a9d03227f201f0a/strategy.c)
Commands used:
`frama-c strategy.c -print -no-unicode -ocode pp_strategy.c`
`frama-c pp_strategy.c`Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/365Why3ide cannot be opened in this version2023-07-21T13:01:20ZPierre Yves PiriouWhy3ide cannot be opened in this versionID0002289:
**This issue was created automatically from Mantis Issue 2289. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002289:
**This issue was created automatically from Mantis Issue 2289. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002289 | Frama-C | Plug-in > wp | public | 2017-03-01 | 2017-03-01 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Pierre-Yves Piriou | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | linux 3.2.0-4-amd64 | **OS** | Debian | **OS Version** | 7.11 |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
When I try to open the Why3 IDE from the GUI to edit a proof (right-click on Why3 column, then 'open why3ide'), the "running icon" is displayed but the IDE does not open.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2632-wp-print for only failed goals2023-07-21T13:01:36ZDavid Cok-wp-print for only failed goalsI suggest a variation on -wp-print that only lists the details for failed goals, perhaps -wp-print-failuresI suggest a variation on -wp-print that only lists the details for failed goals, perhaps -wp-print-failuresLoïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1147Generate proof obligation for drivers when driver instantiate a logic acsl de...2023-07-21T13:21:41ZJens GerlachGenerate proof obligation for drivers when driver instantiate a logic acsl declarationID0001694:
**This issue was created automatically from Mantis Issue 1694. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001694:
**This issue was created automatically from Mantis Issue 1694. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001694 | Frama-C | Plug-in > wp | public | 2014-03-13 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
This would be helpful for proving (in coq) that a model of an ACSL logic function actually exists.Loïc CorrensonLoïc Corrensonhttps://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/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/1027Frama-C/WP does not warn about unsatisfied precondition2023-07-21T13:45:04ZJens GerlachFrama-C/WP does not warn about unsatisfied preconditionID0001678:
**This issue was created automatically from Mantis Issue 1678. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001678:
**This issue was created automatically from Mantis Issue 1678. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001678 | Frama-C | Plug-in > wp | public | 2014-03-07 | 2014-06-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | duplicate |
| **Priority** | high | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | Linux, OSX | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Here is the setup:
```c
/*@
requires 0 < a ;
assigns \nothing;
ensures 0 < \result < 10;
*/
int foo(int a);
/*@
assigns \nothing;
ensures 0 < \result < 30;
*/
int bar(int x)
{
int a = foo(1); // precondition satisfied
int b = foo(0); // precondition violated and recognized
int c = foo(x); // precondition not satisfied and not recognized
return a + b + c;
}
```
When I process this example with
frama-c-gui -wp -cpp-command 'gcc -C -E -I.' -pp-annot -wp-rte -no-unicode -wp-out ./out.wp
-wp-proof alt-ergo -wp-proof coq foo.c
then a green bullet appears next to the line
int c = foo(x); // precondition not satisfied and not recognized
However, it is unknown whether x satisfies the precondition "0 < x" of foo.
If, however, the lines are reverse like this
int c = foo(x);
int b = foo(0);
then both calls are correctly flagged as orange (yellow?)
### Additional Information :
The problem also appears in the release candidate for Neon.https://git.frama-c.com/pub/frama-c/-/issues/2680[WP] Using Z3 when predicate with access to struct defined leads to inconsist...2023-11-27T15:03:11ZReMarxist[WP] Using Z3 when predicate with access to struct defined leads to inconsistency### Steps to reproduce the issue
Launch the following example with this command (note big timeout):
```bash
frama-c -wp -rte -wp-prover="z3" -wp-timeout 100 acsl.c
```
Example:
```c
struct S
{
int n;
};
/*@ axiomatic Block {
pr...### Steps to reproduce the issue
Launch the following example with this command (note big timeout):
```bash
frama-c -wp -rte -wp-prover="z3" -wp-timeout 100 acsl.c
```
Example:
```c
struct S
{
int n;
};
/*@ axiomatic Block {
predicate isZero(int left) =
left == 0;
// Unused, but necessary for verification
logic int getN(struct S *s) = s->n;
}*/
/*@ requires \valid(s);
requires isZero(s->n);
assigns \nothing;
ensures \false; // Verified by Z3
*/
void g(struct S *s)
{
}
/*@ assigns \nothing;
ensures \false; // Verified by Z3
*/
void f()
{
struct S s;
s.n = 0;
g(&s);
}
```
As you can see, specifications establish that f() and g() ensure obviously false statement. The problem is in verification of g(), I've defined f() to show that preconditions of g() can be satisfied.
### Expected behaviour
Attempt to prove `\false` in postcondition of `g()` should fail.
### Actual behaviour
Z3 proves `\false` in postcondition of `g()`:
```
[kernel] Parsing tmp/acsl/acsl.c (with preprocessing)
[rte:annot] annotating function f
[rte:annot] annotating function g
[wp] Running WP plugin...
[wp] 9 goals scheduled
[wp] Proved goals: 9 / 9
Qed: 7
Z3 4.12.2: 2
```
### Contextual information
- Frama-C installation mode: opam
- Frama-C version: 27.1 (Cobalt)
- Z3 version 4.12.2 - 64 bit
- Why3 platform version: 1.6.0
- Plug-in used: WP
- OS name: Ubuntu
- OS version: 20.04
### Additional information
The problem may be in Z3 itself, because Alt-Ergo and CVC4 cannot prove these goals. I've also reproduced the problem using docker image from Docker Hub.
I've posted this report as a question on StackOverflow previously (https://stackoverflow.com/questions/77460683/why-wp-with-z3-proves-false-when-access-to-struct-field-is-defined) as I wasn't able to post an issue here.Allan BlanchardAllan Blanchard