frama-c issues
https://git.frama-c.com/pub/frama-c/-/issues
2021-02-22T13:30:33Z
https://git.frama-c.com/pub/frama-c/-/issues/1205
Property reported as inconditionnally valid when its dependency graph shows s...
2021-02-22T13:30:33Z
Virgile Prevosto
Property reported as inconditionnally valid when its dependency graph shows some orange box
ID0001443:
**This issue was created automatically from Mantis Issue 1443. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001443:
**This issue was created automatically from Mantis Issue 1443. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001443 | Frama-C | Plug-in > wp | public | 2013-06-11 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130501 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
Using wp on the attached files, the rte-generated asserts (and some loop invariants) are reported as valid (green bullet), while they are dependent of some unproved loop invariant.
I flag it as WP bug, as it occurs only when specifying two provers with -wp-proof, so that I suspect some issue in reporting dependencies in this setting.
### Steps To Reproduce :
command line used:
frama-c-gui -wp -wp-model Typed+ref -wp-split binary_search_proved.c -wp-rte -wp-proof alt-ergo,why3:Z3
## Attachments
- [binary_search_proved.c](/uploads/4339976a1729dbee33172d7fad3defb5/binary_search_proved.c)
https://git.frama-c.com/pub/frama-c/-/issues/1199
Confusing bullets for unproven obligations under OSX
2021-02-22T13:30:17Z
Jens Gerlach
Confusing bullets for unproven obligations under OSX
ID0001631:
**This issue was created automatically from Mantis Issue 1631. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001631:
**This issue was created automatically from Mantis Issue 1631. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001631 | Frama-C | Plug-in > wp | public | 2014-01-24 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | OSX | **OS** | - | **OS Version** | 10.9.1 |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
Under OSX an unproven obligation is depicted by a red bullet.
It appears as if that po is actually wrong.
Under Linux a cross (x) is shown instead, which I find better.
I think I would prefer a question mark for a proof obligation that could neither be verified nor refuted.
I attach two screen shots: one from osx and one from linux that show the differences.
### Additional Information :
might be related to issue 0001485
## Attachments
- [gui-osx-and-xubuntu.pdf](/uploads/df960fcf66544389a56320c9d25012b9/gui-osx-and-xubuntu.pdf)
https://git.frama-c.com/pub/frama-c/-/issues/1197
Allow starting coq from Frama-C GUI also for proven obligations
2021-02-22T13:30:12Z
Jens Gerlach
Allow starting coq from Frama-C GUI also for proven obligations
ID0001623:
**This issue was created automatically from Mantis Issue 1623. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001623:
**This issue was created automatically from Mantis Issue 1623. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001623 | Frama-C | Plug-in > wp | public | 2014-01-21 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | Linux, OSX | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
Currently it is not possible to start the codide from the Frama-C GUI
for a proof obligation that has already been proven by Coq.
However, it would be desirable to do so in order to improve/refactor an already existing proof.
https://git.frama-c.com/pub/frama-c/-/issues/1195
Qedlib.v definition of tactic "replace by" clashes with standard tactic "repl...
2023-01-04T11:04:20Z
Jens Gerlach
Qedlib.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 obligation
https://git.frama-c.com/pub/frama-c/-/issues/1192
Bug in let-elimination (due to <==> and assert false).
2023-02-03T12:18:59Z
Loïc Correnson
Bug 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/1191
WP ignores some goal
2021-02-22T14:02:45Z
mantis-gitlab-migration
WP ignores some goal
ID0001588:
**This issue was created automatically from Mantis Issue 1588. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001588:
**This issue was created automatically from Mantis Issue 1588. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001588 | Frama-C | Plug-in > wp | public | 2013-12-20 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
On this example, WP ignore some of the goals. There should be 3 goals, but :
[wp] 1 goal scheduled
[wp] [Qed] Goal typed_f_loop_inv_l1_2_established : Valid
Loop invariant preservation and assertion are ignore.
### Additional Information :
I simplified the example as much as possible, but it seems that the number of statements is important to reproduce the problem 8-/
### Steps To Reproduce :
frama-c wp.c -wp
## Attachments
- [wp.c](/uploads/f296e3e3d81e278bf5e25179c5d16e29/wp.c)
https://git.frama-c.com/pub/frama-c/-/issues/1181
invalid loop invariant marked as valid (without pending hypothesis)
2021-02-22T13:30:09Z
Virgile Prevosto
invalid loop invariant marked as valid (without pending hypothesis)
ID0001462:
**This issue was created automatically from Mantis Issue 1462. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001462:
**This issue was created automatically from Mantis Issue 1462. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001462 | Frama-C | Plug-in > wp | public | 2013-07-29 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | correnson | **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 Neon-20140301 |
### Description :
Given the program below, wp discharges all proof obligations, including the first loop invariant whose preservation is false. This allows then to prove the invalid assertion after the loop. It seems that all three loop invariants (with their \at() term) are necessary to reproduce the issue.
### Additional Information :
-- file.c
void f(int c) {
int x = 0;
int y = 0;
/*@ assert for_value: c<= 0 || c == 1 || c>=2; */
if (c==2) { x=1; y=1; }
L:
/*@
loop invariant \at(x==0,L) ==> i!=0 ==> y == 0;
loop invariant \at(x==1,L) ==> i!=0 ==> x == 1;
loop invariant \at(c==0,Pre) ==> i==0 ==> x == 0;
loop assigns i,x,y;
*/
for (int i = 0; i<10; i++) {
if (c == 0) { x = 0; }
if (c == 1) { y = 1; }
if (c == 2) { x = 1; }
}
if (c==1) { /*@ assert consequence_of_false_invariant: y==0; */ }
}
### Steps To Reproduce :
frama-c -wp file.c
One can see the inconsistent status (green/black bullet) of the assert with
frama-c-gui -wp file.c -then -val -main f -slevel 100
https://git.frama-c.com/pub/frama-c/-/issues/1173
ACSL label LoopEntry not handled by WP
2022-10-06T14:57:24Z
mantis-gitlab-migration
ACSL label LoopEntry not handled by WP
ID0001353:
**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/1147
Generate proof obligation for drivers when driver instantiate a logic acsl de...
2023-07-21T13:21:41Z
Jens Gerlach
Generate proof obligation for drivers when driver instantiate a logic acsl declaration
ID0001694:
**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 Correnson
Loïc Correnson
https://git.frama-c.com/pub/frama-c/-/issues/1146
Generate footprint from reads clauses of logic declarations
2021-08-05T09:15:35Z
Jens Gerlach
Generate footprint from reads clauses of logic declarations
ID0001693:
**This issue was created automatically from Mantis Issue 1693. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001693:
**This issue was created automatically from Mantis Issue 1693. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001693 | Frama-C | Plug-in > wp | public | 2014-03-13 | 2014-03-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | high | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
It would be helpful if the reads clause of an axiomatic definition would be
used to generate additional hypothesis for coq proofs.
Loïc Correnson
Loïc Correnson
https://git.frama-c.com/pub/frama-c/-/issues/1145
Develop strategies to efficiently run WP with different ATP and Coq
2021-09-21T13:22:14Z
Jens Gerlach
Develop strategies to efficiently run WP with different ATP and Coq
ID0001699:
**This issue was created automatically from Mantis Issue 1699. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001699:
**This issue was created automatically from Mantis Issue 1699. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001699 | Frama-C | Plug-in > wp | public | 2014-03-14 | 2014-03-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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 strategy should be controlled by a view options that also take into account how many processes are available.
Loïc Correnson
Loïc Correnson
https://git.frama-c.com/pub/frama-c/-/issues/1032
WP - strcpy not proved
2021-02-22T13:17:51Z
mantis-gitlab-migration
WP - strcpy not proved
ID0001652:
**This issue was created automatically from Mantis Issue 1652. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001652:
**This issue was created automatically from Mantis Issue 1652. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001652 | Frama-C | Plug-in > wp | public | 2014-02-24 | 2014-06-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dharma | **Assigned To** | - | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Ubuntu | **OS** | Linux | **OS Version** | 64 bit |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
I took the attached program from one of the WP tutorials but added the main function which calls strcpy. I wonder why the requires are not valid. I do not know what is wrong with my two strings in main.
### Steps To Reproduce :
[formal_verification]$ frama-c -pp-annot -wp -wp-rte -wp-proof why3:Z3,alt-ergo -wp-split -wp-model Typed+ref string_lib.c [kernel] preprocessing with "gcc -C -E -I. -dD string_lib.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function main
[wp] Collecting variable usage
[wp] 4 goals scheduled
[wp] [Qed] Goal typed_ref_main_call_strcpy_pre_2_part1 : Valid [wp] [Qed] Goal typed_ref_main_call_strcpy_pre_2_part1 : Valid [wp] [Alt-Ergo] Goal typed_ref_main_call_strcpy_pre : Unknown [wp] [Alt-Ergo] Goal typed_ref_main_call_strcpy_pre_2_part2 : Unknown (Qed:4ms) [wp] [Z3] Goal typed_ref_main_call_strcpy_pre_2_part2 : Unknown (Qed:4ms) [wp] [Z3] Goal typed_ref_main_call_strcpy_pre : Unknown [wp] [Alt-Ergo] Goal typed_ref_main_call_strcpy_pre_3 : Valid (24ms) (22) [wp] [Z3] Goal typed_ref_main_call_strcpy_pre_3 : Valid (10ms)
## Attachments
- [string_lib.c](/uploads/83ca58d14714f50a83c5dbefcf99dec0/string_lib.c)
https://git.frama-c.com/pub/frama-c/-/issues/1031
WP: Assertion not proved -> conversion from float to int issue?
2021-02-22T14:02:32Z
mantis-gitlab-migration
WP: Assertion not proved -> conversion from float to int issue?
ID0001655:
**This issue was created automatically from Mantis Issue 1655. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001655:
**This issue was created automatically from Mantis Issue 1655. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001655 | Frama-C | Plug-in > wp | public | 2014-02-27 | 2014-06-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dharma | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Ubuntu | **OS** | Linux | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
I'm using Frama-C for my course at UMD. Found it pretty helpful.
I tried this puzzle, but cannot get WP to prove the assertion, which is true.
I ran through the GDB and found that the value of i is INT_MIN, satisfying the assert.
#include <limits.h>
/*@ requires x != 0;
assigns \nothing;
*/
void assert(int x);
int main()
{
float f = INT_MAX;
int i = f;
assert(i == INT_MIN);
return 0;
}
### Steps To Reproduce :
[formal_verification]$ frama-c -wp -wp-rte float_to_int_assert.c
[kernel] preprocessing with "gcc -C -E -I. float_to_int_assert.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function main
[wp] 3 goals scheduled
[wp] [Alt-Ergo] Goal typed_main_assert_rte_float_to_int_2 : Valid (8ms)
[wp] [Alt-Ergo] Goal typed_main_assert_rte_float_to_int : Valid (12ms)
[wp] [Alt-Ergo] Goal typed_main_call_assert_pre : Unknown
## Attachments
- [int_of_real_why3.diff](/uploads/3aadceb64f4a89ae445498f3e92952de/int_of_real_why3.diff)
- [floats_and_ints.diff](/uploads/b4984e6711b9343f82562f3dd284f08a/floats_and_ints.diff)
https://git.frama-c.com/pub/frama-c/-/issues/1030
int to double - assert not verified
2021-02-22T14:02:32Z
mantis-gitlab-migration
int to double - assert not verified
ID0001651:
**This issue was created automatically from Mantis Issue 1651. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001651:
**This issue was created automatically from Mantis Issue 1651. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001651 | Frama-C | Plug-in > wp | public | 2014-02-24 | 2014-06-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dharma | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Ubuntu | **OS** | Linux | **OS Version** | 64 bit |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
For this below program, the assert should be valid I think but the WP is not proving it.
#include <limits.h>
/*@ requires x != 0;
assigns \nothing;
*/
void assert(int x);
int main()
{
double f = INT_MAX;
int i = f;
assert(i == INT_MAX);
return 0;
}
### Additional Information :
The regular C assert was able to prove when I run the a.out after compiling the wrong (commenting the ACSL's assert).
### Steps To Reproduce :
[formal_verification]$ frama-c -wp -wp-rte double_to_int_max_2.c -pp-annot [kernel] preprocessing with "gcc -C -E -I. -dD double_to_int_max_2.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function main
[wp] 3 goals scheduled
[wp] [Alt-Ergo] Goal typed_main_assert_rte_float_to_int_2 : Valid (4ms) [wp] [Alt-Ergo] Goal typed_main_assert_rte_float_to_int : Valid (12ms) [wp] [Alt-Ergo] Goal typed_main_call_assert_pre : Unknown (1s)
https://git.frama-c.com/pub/frama-c/-/issues/1029
short int to float assertion not proved
2021-02-22T14:02:32Z
mantis-gitlab-migration
short int to float assertion not proved
ID0001653:
**This issue was created automatically from Mantis Issue 1653. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001653:
**This issue was created automatically from Mantis Issue 1653. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001653 | Frama-C | Plug-in > wp | public | 2014-02-24 | 2014-06-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dharma | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Ubuntu | **OS** | Linux | **OS Version** | 64 bit |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Wonder why this assertion is not provable even though it is a valid one.
#include <limits.h>
/*@ requires x != 0;
assigns \nothing;
*/
void assert(int x);
int main()
{
float f = SHRT_MAX;
short int i = f;
assert(i == SHRT_MAX);
}
### Steps To Reproduce :
[formal_verification]$ frama-c -wp -wp-rte float_to_short_int_max_2.c -pp-annot [kernel] preprocessing with "gcc -C -E -I. -dD float_to_short_int_max_2.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function main
[wp] 3 goals scheduled
[wp] [Alt-Ergo] Goal typed_main_assert_rte_float_to_int_2 : Valid (4ms) [wp] [Alt-Ergo] Goal typed_main_assert_rte_float_to_int : Valid (8ms) [wp] [Alt-Ergo] Goal typed_main_call_assert_pre : Unknown
https://git.frama-c.com/pub/frama-c/-/issues/1027
Frama-C/WP does not warn about unsatisfied precondition
2023-07-21T13:45:04Z
Jens Gerlach
Frama-C/WP does not warn about unsatisfied precondition
ID0001678:
**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/1026
Signal -7 and then crashed.
2021-02-22T13:47:19Z
mantis-gitlab-migration
Signal -7 and then crashed.
ID0001602:
**This issue was created automatically from Mantis Issue 1602. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001602:
**This issue was created automatically from Mantis Issue 1602. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001602 | Frama-C | Plug-in > wp | public | 2014-01-15 | 2014-06-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dharma | **Assigned To** | correnson | **Resolution** | unable to reproduce |
| **Priority** | high | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
$ frama-c -wp -wp-rte test_frama.c -wp-fct=myFunc -wp-bhv=basic -main myFunc -lib-entry -wp-timeout=500
[kernel] preprocessing with "gcc -C -E -I. test_frama.c"
[wp] Running WP plugin...
[rte] annotating function myFunc
[wp] Collecting axiomatic usage
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_myFunc_basic_post : Failed
Error: Unix.SIGNAL -7
Any comments?
### Steps To Reproduce :
I used Alt-Ergo 0.95.2. Unfortunately, this code is somewhat complex and cannot disclose here although I would like to share.
## Attachments
- [ApLowAlm.mlw](/uploads/39c448b8eed5e0db531692fb99845956/ApLowAlm.mlw)
https://git.frama-c.com/pub/frama-c/-/issues/1024
WP doesn't warn about volatile variables
2021-04-15T07:10:32Z
mantis-gitlab-migration
WP doesn't warn about volatile variables
ID0001801:
**This issue was created automatically from Mantis Issue 1801. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001801:
**This issue was created automatically from Mantis Issue 1801. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001801 | Frama-C | Plug-in > wp | public | 2014-06-06 | 2014-06-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
I noticed that WP doesn't handle volatile variables, which is not a problem, but the problem is that it proves properties about them without any warning at all, which a quiet embarrassing I suppose.
### Steps To Reproduce :
$ frama-c -wp-fct main test_volatile.c
volatile int v = 10;
//@ ensures \result == 10;
int main (void) {
int x = v;
//@ assert v == 10;
v = 3;
//@ assert v == 3;
return x;
}
Loïc Correnson
Loïc Correnson
https://git.frama-c.com/pub/frama-c/-/issues/1020
syntax error for alt-ergo with memset spec
2021-02-22T13:17:31Z
mantis-gitlab-migration
syntax error for alt-ergo with memset spec
ID0001587:
**This issue was created automatically from Mantis Issue 1587. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001587:
**This issue was created automatically from Mantis Issue 1587. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001587 | Frama-C | Plug-in > wp | public | 2013-12-16 | 2014-06-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
When trying to prove the first loop invariant of this example, there is a message:
/tmp/wpd57f12.dir/typed/A_MemSet.ergo:10:[wp] user error:
Prover Alt-Ergo returns Failed
characters 6-106:typing error: syntax error
and neither the establishment nor the preservation can be proved.
### Additional Information :
Command line is :
frama-c -cpp-extra-args=-I`frama-c -print-share-path`/libc pb_wp.c -wp
## Attachments
- [pb_wp.c](/uploads/97bd3bebc043ed6808b7047aec5dd9d0/pb_wp.c)
https://git.frama-c.com/pub/frama-c/-/issues/1019
Assigns not respected in behaviors when using pointers to pointers
2021-08-05T08:49:22Z
mantis-gitlab-migration
Assigns not respected in behaviors when using pointers to pointers
ID0001812:
**This issue was created automatically from Mantis Issue 1812. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001812:
**This issue was created automatically from Mantis Issue 1812. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001812 | Frama-C | Plug-in > wp | public | 2014-06-16 | 2014-06-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Ian | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Ubuntu | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Assigns defined in behaviors are not always respected. The example provided shows an assigns defined in complete behaviors that causes a different results than if defined outside the behaviors. The results are expected to be the same since the behaviors are complete.
### Steps To Reproduce :
Create file (attached: invalid.c):
```
/*@
@ requires \valid(a) && \valid(*a) && \separated(a, *a);
@ behavior all:
@ assumes \true;
@ assigns **a;
@ complete behaviors all;
@*/
void set_next_next(int **a){
**a = 0;
}
void main(){
int **a, *b, c;
b = &c;
a = &b;
pre_fct:
set_next_next(a);
//@ assert b == \at(b, pre_fct);
}
```
Run:
```
frama-c -cpp-command 'gcc -C -E' -wp invalid.c
```
Result:
Assertion in main does not validate.
By moving the assigns statement outside the behavior, the assertion is validated:
```
/*@
@ requires \valid(a) && \valid(*a) && \separated(a, *a);
@ assigns **a;
@ behavior all:
@ assumes \true;
@ complete behaviors all;
@*/
```
## Attachments
- [invalid.c](/uploads/3d4a401d6a5d55ab1cb43bcbb73e53c8/invalid.c)
- [valid.c](/uploads/a336506d1703a71e66da940fbdef2a11/valid.c)
Loïc Correnson
Loïc Correnson