frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T13:32:50Zhttps://git.frama-c.com/pub/frama-c/-/issues/1483WP computation is looping during variable analysis2021-02-22T13:32:50Zmantis-gitlab-migrationWP computation is looping during variable analysisID0001355:
**This issue was created automatically from Mantis Issue 1355. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001355:
**This issue was created automatically from Mantis Issue 1355. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001355 | Frama-C | Plug-in > wp | public | 2013-01-31 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | Frama-C Fluorine-20130401 |
### Description :
Sorry: I didn't manage to build a small example to reproduce the problem that happen on a large application.
The infinite loop occurs before starting the WP computation itself,
but after the [wp:cil2cfg] processing.
It seems to be during the analysis which stat with:
[wp:var_analysis] [LP+AT] logic parameters and address taken computation
The debug messages while looping are :
[wp:var_kind] TheGlobalVariable is a memvar
[wp:context] POPK 0: "init_value"
[wp:context] PUSH 0: "init_value"
[wp:var_kind] TheGlobalVariable is a memvar
[wp:context] POPK 0: "init_value"
[wp:context] PUSH 0: "init_value"
... etc... (always with the same variable name).
Maybe it is important to say that :
- there are recursive calls in the application;
- the variable is static to one file;
- the type of the variable is a structure.
I don't know what else I can say to help, but please ask for more details if you have an idea.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)https://git.frama-c.com/pub/frama-c/-/issues/959WP crashes on \floor builtin2021-04-15T08:15:30Zmantis-gitlab-migrationWP crashes on \floor builtinID0001936:
**This issue was created automatically from Mantis Issue 1936. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001936:
**This issue was created automatically from Mantis Issue 1936. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001936 | Frama-C | Plug-in > wp | public | 2014-10-12 | 2014-10-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | WolframKahl | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | GNU/Linux | **OS Version** | 3.14.14-gentoo |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running
frama-c-gui -wp floor.c
produces the following in the pre-GUI-console:
[kernel] preprocessing with "gcc -C -E -I. floor.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] user error: Builtin \floor(real) not defined
[wp] failure: Logic '\floor' undefined
and then crashes with a pop-up containing:
Current source was: :0
The full backtrace is:
Raised at file "hashtbl.ml", line 254, characters 18-27
Called from file "hashtbl.ml", line 262, characters 22-38
Plug-in wp aborted: internal error.
Reverting to previous state.
Look at the console for additional information (if any).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301.
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
(I get this also with Fluorine.)
### Additional Information :
Backtrace from the command-line:
$ frama-c -wp floor.c
[kernel] preprocessing with "gcc -C -E -I. floor.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] user error: Builtin \floor(real) not defined
[wp] failure: Logic '\floor' undefined
[kernel] Current source was: floor.c:7
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "src/wp/LogicCompiler.ml", line 698, characters 20-51
Called from file "src/wp/LogicCompiler.ml", line 748, characters 10-23
Called from file "src/wp/LogicSemantics.ml", line 518, characters 8-34
Called from file "src/wp/LogicSemantics.ml", line 768, characters 12-27
Called from file "src/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/wp/Context.ml", line 34, characters 41-46
Called from file "src/wp/LogicCompiler.ml", line 358, characters 20-35
Called from file "src/wp/LogicSemantics.ml", line 336, characters 31-50
Called from file "src/wp/LogicSemantics.ml", line 779, characters 12-37
Called from file "src/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/wp/Context.ml", line 34, characters 41-46
Called from file "src/wp/Warning.ml", line 155, characters 14-18
Called from file "src/wp/cfgWP.ml", line 456, characters 23-140
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "list.ml", line 74, characters 24-34
Called from file "src/wp/calculus.ml", line 331, characters 22-64
Called from file "src/wp/calculus.ml", line 341, characters 23-45
Called from file "src/wp/calculus.ml", line 613, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 586, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 589, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 589, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 579, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 574, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 699, characters 40-59
Called from file "set.ml", line 288, characters 38-41
Called from file "map.ml", line 169, characters 20-25
Called from file "map.ml", line 169, characters 10-18
Called from file "map.ml", line 169, characters 10-18
Called from file "src/wp/calculus.ml", line 699, characters 4-64
Called from file "src/wp/calculus.ml", line 745, characters 19-51
Called from file "src/wp/cfgWP.ml", line 1382, characters 39-62
Called from file "src/wp/cfgWP.ml", line 1371, characters 14-837
Called from file "src/wp/Model.ml", line 111, characters 17-20
Re-raised at file "src/wp/Model.ml", line 116, characters 25-28
Called from file "src/wp/Model.ml", line 117, characters 19-36
Called from file "src/wp/register.ml", line 435, characters 17-42
Called from file "src/wp/register.ml", line 574, characters 17-24
Re-raised at file "src/wp/register.ml", line 578, characters 29-31
Called from file "src/wp/register.ml", line 575, characters 17-24
Re-raised at file "src/wp/register.ml", line 579, characters 32-34
Called from file "src/wp/register.ml", line 575, characters 17-24
Re-raised at file "src/wp/register.ml", line 579, characters 32-34
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 37, characters 4-20
Called from file "src/kernel/cmdline.ml", line 735, characters 2-9
Called from file "src/kernel/cmdline.ml", line 214, characters 4-8
Plug-in wp aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301.
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
### Steps To Reproduce :
frama-c -wp floor.c
frama-c-gui -wp floor.c
## Attachments
- [floor.c](/uploads/a68db963d3a04b7082b71cb6bdd8566a/floor.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/635WP crashes on generation of PO for assigns clause (assertion failure in MemVa...2021-02-22T14:01:52ZVirgile PrevostoWP crashes on generation of PO for assigns clause (assertion failure in MemVar.ml)ID0002124:
**This issue was created automatically from Mantis Issue 2124. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002124:
**This issue was created automatically from Mantis Issue 2124. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002124 | Frama-Clang | Plug-in > wp | public | 2015-06-01 | 2015-06-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | correnson | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
On the example source below, frama-c -wp reduced.i crashes with the following error:
File "src/wp/MemVar.ml", line 491, characters 54-60: Assertion failed
Apparently (by inferring why the offending function in MemVar got called), the p1+0 in the assigns for fn1 leads WP to think that p1 should be instantiated with an array (in particular, if you remove the +0, everything is fine).
-- reduced.i
/*@ assigns *(p1); */
int fn1(char *p1);
/*@
assigns \nothing;
*/
void fn2(void) {
char pcr_index;
fn1(&pcr_index);
}https://git.frama-c.com/pub/frama-c/-/issues/571WP crashes on generation of PO for assigns clause (assertion failure in MemVa...2021-02-22T14:01:52ZVirgile PrevostoWP crashes on generation of PO for assigns clause (assertion failure in MemVar.ml)ID0002126:
**This issue was created automatically from Mantis Issue 2126. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002126:
**This issue was created automatically from Mantis Issue 2126. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002126 | Frama-C | Plug-in > wp | public | 2015-06-02 | 2016-01-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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 Magnesium |
### Description :
On the example source below, frama-c -wp reduced.i crashes with the following error:
File "src/wp/MemVar.ml", line 491, characters 54-60: Assertion failed
Apparently (by inferring why the offending function in MemVar got called), the p1+0 in the assigns for fn1 leads WP to think that p1 should be instantiated with an array (in particular, if you remove the +0, everything is fine).
-- reduced.i
/*@ assigns *(p1); */
int fn1(char *p1);
/*@
assigns \nothing;
*/
void fn2(void) {
char pcr_index;
fn1(&pcr_index);
}https://git.frama-c.com/pub/frama-c/-/issues/527WP crashes with \pointer_comparable2021-04-14T15:33:46Zmantis-gitlab-migrationWP crashes with \pointer_comparableID0002207:
**This issue was created automatically from Mantis Issue 2207. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002207:
**This issue was created automatically from Mantis Issue 2207. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002207 | Frama-C | Plug-in > wp | public | 2016-02-03 | 2016-02-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jochenam | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Linux Mint | **OS Version** | 17.3 |
| **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | - |
### Description :
See also issue 0002206:
When instead of only -val Frama-C is called with -val -wp, the WP plug-in crashes, seemingly because of the pointer_comparable generated by Value.
### Steps To Reproduce :
Run Frama-C on attached file:
frama-c -val -wp main.c
## Attachments
- [main.c](/uploads/f7bb9f114ed5bbc36cf916a66ea75994/main.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/518WP detect a non-natural loop on a do-while(0) loop2021-04-15T08:47:58Zmantis-gitlab-migrationWP detect a non-natural loop on a do-while(0) loopID0001911:
**This issue was created automatically from Mantis Issue 1911. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001911:
**This issue was created automatically from Mantis Issue 1911. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001911 | Frama-C | Plug-in > wp | public | 2014-08-19 | 2016-03-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
In the attached example, the do-while(0) "false" loop makes the WP fail with the message:
wp2.c:8:[wp] warning: calculus failed on strategy
for 'main', behavior 'default!', all properties, both assigns or not because
unsupported non-natural loop without invariant property. (abort)
Maybe it can be detected that this is not a loop in fact ?
### Additional Information :
It is ok with -wp-invariants option.
### Steps To Reproduce :
$ frama-c -wp-fct main wp2.c
## Attachments
- [wp2.c](/uploads/b42a155d1a7118131a8c4260a6a121b4/wp2.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1024WP doesn't warn about volatile variables2021-04-15T07:10:32Zmantis-gitlab-migrationWP doesn't warn about volatile variablesID0001801:
**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 CorrensonLoïc Corrensonhttps://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/1925[wp] failure: not an integer (Blob)2021-04-14T15:42:16Zmantis-gitlab-migration[wp] failure: not an integer (Blob)ID0001332:
**This issue was created automatically from Mantis Issue 1332. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001332:
**This issue was created automatically from Mantis Issue 1332. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001332 | Frama-C | Plug-in > wp | public | 2012-12-15 | 2012-12-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Philippe | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | - |
### Description :
> cat bar.c
typedef struct S { signed char x[16]; } S;
/*@ axiomatic Y { logic integer Z (S t, integer i, integer j) reads t.x[i..j]; } */
/*@ ensures \result == Z(s, 0, 15); */
int foo(S s) { return 0; }
> frama-c -wp -wp-rte -wp-fct foo bar.c
[kernel] preprocessing with "gcc -C -E -I. bar.c"
[wp] Running WP plugin...
[rte] annotating function foo
[wp] warning: Interpreting reads-definition as expressions rather than tsets
bar.c:6:[wp] failure: not an integer (Blob)
[kernel] The full backtrace is:
Raised at file "src/kernel/log.ml", line 523, characters 30-31
Called from file "src/kernel/log.ml", line 517, characters 9-16
Re-raised at file "src/kernel/log.ml", line 520, characters 15-16
Called from file "src/wp/translate_prop.ml", line 911, characters 16-71
Called from file "src/wp/translate_prop.ml", line 1323, characters 12-33
Called from file "src/wp/translate_prop.ml", line 1579, characters 32-52
Called from file "list.ml", line 69, characters 12-15
Called from file "src/wp/translate_prop.ml", line 1974, characters 14-68
Re-raised at file "src/wp/translate_prop.ml", line 2029, characters 12-15
Called from file "src/wp/translate_prop.ml", line 1827, characters 27-34
Re-raised at file "src/wp/translate_prop.ml", line 1831, characters 43-48
Called from file "src/wp/translate_prop.ml", line 2188, characters 21-56
Called from file "src/wp/translate_prop.ml", line 1570, characters 17-59
Called from file "src/wp/translate_prop.ml", line 1323, characters 12-33
Called from file "src/wp/translate_prop.ml", line 1745, characters 19-38
Called from file "src/wp/translate_prop.ml", line 1707, characters 13-30
Called from file "src/wp/wp_error.ml", line 102, characters 13-20
Re-raised at file "src/wp/wp_error.ml", line 95, characters 20-23
Called from file "src/wp/cfgWeakestPrecondition.ml", line 224, characters 17-33
Called from file "src/wp/cfgWeakestPrecondition.ml", line 154, characters 18-44
Re-raised at file "src/wp/wp_error.ml", line 90, characters 20-23
Called from file "src/wp/cfgWeakestPrecondition.ml", line 165, characters 34-54
Re-raised at file "src/wp/cfgWeakestPrecondition.ml", line 184, characters 14-17
Called from file "src/wp/cfgpropid.ml", line 96, characters 10-20
Re-raised at file "src/wp/cfgpropid.ml", line 100, characters 14-15
Called from file "src/wp/cfgpropid.ml", line 140, characters 12-59
Called from file "list.ml", line 74, characters 24-34
Called from file "src/wp/calculus.ml", line 326, characters 22-64
Called from file "src/wp/calculus.ml", line 336, characters 23-45
Called from file "src/wp/calculus.ml", line 575, characters 20-43
Called from file "src/wp/calculus.ml", line 498, characters 21-42
Called from file "src/wp/calculus.ml", line 548, characters 20-43
Called from file "src/wp/calculus.ml", line 498, characters 21-42
Called from file "src/wp/calculus.ml", line 551, characters 20-43
Called from file "src/wp/calculus.ml", line 498, characters 21-42
Called from file "src/wp/calculus.ml", line 551, characters 20-43
Called from file "src/wp/calculus.ml", line 498, characters 21-42
Called from file "src/wp/calculus.ml", line 541, characters 20-43
Called from file "src/wp/calculus.ml", line 498, characters 21-42
Called from file "src/wp/calculus.ml", line 536, characters 20-43
Called from file "src/wp/calculus.ml", line 498, characters 21-42
Called from file "src/wp/calculus.ml", line 661, characters 40-59
Called from file "set.ml", line 288, characters 38-41
Called from file "set.ml", line 293, characters 37-58
Called from file "set.ml", line 293, characters 42-57
Called from file "set.ml", line 293, characters 42-57
Called from file "src/wp/calculus.ml", line 661, characters 4-64
Called from file "src/wp/calculus.ml", line 708, characters 19-51
Called from file "src/wp/cfgProof.ml", line 238, characters 30-53
Called from file "list.ml", line 69, characters 12-15
Called from file "src/wp/cfgProof.ml", line 228, characters 8-666
Called from file "src/wp/register.ml", line 586, characters 22-41
Called from file "src/wp/register.ml", line 679, characters 17-24
Re-raised at file "src/wp/register.ml", line 683, characters 32-34
Called from file "src/wp/register.ml", line 678, characters 17-24
Re-raised at file "src/wp/register.ml", line 682, characters 29-31
Called from file "src/wp/register.ml", line 678, characters 17-24
Re-raised at file "src/wp/register.ml", line 682, characters 29-31
Called from file "src/wp/register.ml", line 678, characters 17-24
Re-raised at file "src/wp/register.ml", line 682, characters 29-31
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 38, characters 4-20
Called from file "src/kernel/cmdline.ml", line 720, characters 2-9
Called from file "src/kernel/cmdline.ml", line 197, characters 4-8
Plug-in wp aborted: internal error.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2589[WP] Failure to verify range information after bitwise and on signed integers2022-01-11T07:16:49ZGuerricChupin[WP] Failure to verify range information after bitwise and on signed integersIn the function below, WP fails to verify the assertion (which I believe is true after exhaustively testing it):
```c
/*@ assigns \nothing;
@*/
int8_t foo(int8_t n) {
int8_t m = n & 0xF;
/*@ assert 0 <= m < 16; */
return ...In the function below, WP fails to verify the assertion (which I believe is true after exhaustively testing it):
```c
/*@ assigns \nothing;
@*/
int8_t foo(int8_t n) {
int8_t m = n & 0xF;
/*@ assert 0 <= m < 16; */
return m;
}
```
It does so with all signed integer types, but doesn't with unsigned integer types. Performing the `&` on an unsigned integer type and casting the result to a signed integer doesn't work either. For instance, in the function below, the first assertion is verified but not the second:
```c
int8_t bar(int8_t n) {
uint8_t m = n & 0xF;
/*@ assert 0 <= m < 16; */
int8_t p = m;
/*@ assert 0 <= p < 16; */
return p;
}
```
Test file: [test.c](/uploads/2751b8e74f9f0f37840a32cbff4965ce/test.c)
I used this command to run Frama-C:
```bash
frama-c -wp -wp-rte test.c -wp-prover why3:alt-ergo -wp-prover why3:cvc4 -wp-prover why3:Z3
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 24.0
- Plug-in used: WP, RTE
- OS name: Fedora
- OS version: 35
- Solvers: Alt-Ergo 2.4.1, CVC4 1.8, Z3 4.8.11
### 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.
-->https://git.frama-c.com/pub/frama-c/-/issues/2690[WP] Frama-C/WP 28.0 does not work with Isabelle/HOL2024-03-06T11:53:41Zkwaxer[WP] Frama-C/WP 28.0 does not work with Isabelle/HOL### Steps to reproduce the issue
1. Make sure Isabelle/HOL is installed and `why3` is configured to use it.
2. Create file `test.h` with the following code:
```
/*@
logic \list<integer> enumeration (integer n) = n == 0 ? \Nil : enu...### Steps to reproduce the issue
1. Make sure Isabelle/HOL is installed and `why3` is configured to use it.
2. Create file `test.h` with the following code:
```
/*@
logic \list<integer> enumeration (integer n) = n == 0 ? \Nil : enumeration (n - 1) ^ [|n - 1|];
lemma enumeration_length: \forall integer n; 0 <= n ==> \length (enumeration (n)) == n;
*/
```
3. Run WP plugin selecting Isabelle/HOL as a backend: `frama-c -wp -wp-prover=why3:isabelle -wp-interactive=fix -wp-cache=none test.h`
### Expected behaviour
Earlier versions of Frama-C (e.g. 27.1) produce the following output:
```
[kernel] Parsing test.h (with preprocessing)
[wp] 1 goal scheduled
[wp] Proved goals: 1 / 1
Qed: 0
Isabelle 2022: 1 (8.1s)
```
with the theory
```isabelle
theory lemma_enumeration_length imports Why3.Why3 begin
why3_open "lemma_enumeration_length.xml"
why3_vc wp_goal
using assms L_enumeration_def
by (induction i) (simp_all add: facts.length_concat length_cons length_nil)
why3_end
end
```
### Actual behaviour
Frama-C 28.0 produces the following:
```
[kernel] Parsing test.h (with preprocessing)
[wp] 1 goal scheduled
[wp] [Failure] typed_lemma_enumeration_length (Isabelle)
[wp] Proved goals: 0 / 1
Qed: 0
Failed: 1
```
### Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *28.0 (Nickel)*
- Plug-in used: *WP*
- OS name: *Ubuntu*
- OS version: *22.04.4 LTS*
### Additional information (optional)
`-wp-msg-key why3_api` gives the following error trace:
```
[wp] Failure: [Why3 Error] anomaly: Sys_error(".../.frama-c/wp/interactive/lemma_enumeration_length/.xml: No such file or directory")
Raised by primitive operation at Stdlib.open_out_gen in file "stdlib.ml", line 331, characters 29-55
Called from Stdlib.open_out in file "stdlib.ml" (inlined), line 336, characters 2-74
Called from Frama_c_kernel__Command.pp_to_file in file "src/libraries/utils/command.ml", line 31, characters 13-35
Called from Wp__ProverWhy3.prepare in file "src/plugins/wp/ProverWhy3.ml", line 1339, characters 6-130
Called from Wp__ProverWhy3.interactive in file "src/plugins/wp/ProverWhy3.ml", line 1352, characters 8-37
Called from Wp__ProverWhy3.build_proof_task in file "src/plugins/wp/ProverWhy3.ml", line 1413, characters 8-59
```
There is an unexpected slash right the before `.xml` file extension.https://git.frama-c.com/pub/frama-c/-/issues/1191WP ignores some goal2021-02-22T14:02:45Zmantis-gitlab-migrationWP ignores some goalID0001588:
**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/776WP ignores some goals when 'initialized' is used in hypotheses2021-02-22T13:11:28Zmantis-gitlab-migrationWP ignores some goals when 'initialized' is used in hypothesesID0001670:
**This issue was created automatically from Mantis Issue 1670. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001670:
**This issue was created automatically from Mantis Issue 1670. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001670 | Frama-C | Plug-in > wp | public | 2014-03-04 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
The message:
[wp] warning: Allocable, Freeable, Valid_read, Fresh and Initialized not yet implemented
is perfectly clear, but I would have expected that annotations using these predicates would have been ignored. Instead of that, proof obligations of other annotations simply disappear.
### Steps To Reproduce :
Example:
/*@ requires r1: \initialized(Y+(0 .. 99));
assigns X[0..99];
ensures X[0] == Y[0];
*/
void cp( int *X, int *Y );
void f (int *A, int *B) {
cp(B, A);
/*@ assert a1: A[0] == B[0]; */
}
Without the 'requires' property, the assertion is proved:
$ frama-c -wp test.c -wp-prop a1
...
[wp] 1 goal scheduled
[wp] [Qed] Goal typed_f_assert_a1 : Valid
[wp] Proved goals: 1 / 1
Qed: 1
With the 'requires' property, the assertion is not even scheduled as a goal:
$ frama-c -wp test.c -wp-prop a1
...
[wp] 0 goal scheduled
[wp] Proved goals: 0 / 0https://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/385WP inserts unwanted new lines into Coq proofs2021-04-15T09:00:28ZJens GerlachWP inserts unwanted new lines into Coq proofsID0002266:
**This issue was created automatically from Mantis Issue 2266. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002266:
**This issue was created automatically from Mantis Issue 2266. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002266 | Frama-C | Plug-in > wp | public | 2017-01-02 | 2017-01-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
I have noticed (since Aluminium) that whenever I work on a Coq proof, then WP adds a newline to all the other Coq proofs in wp0.script (right before "Qed.").
In the long run, it is a bit annoying to have all these empty lines in the coq proofs...Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/261WP: internal error: only the kernel should set the status of property assumes2021-02-22T12:57:46Zmantis-gitlab-migrationWP: internal error: only the kernel should set the status of property assumesID0002383:
**This issue was created automatically from Mantis Issue 2383. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002383:
**This issue was created automatically from Mantis Issue 2383. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002383 | Frama-C | Plug-in > wp | public | 2018-07-04 | 2018-07-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | correnson | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
Example:
<pre>
int test(void)
{
int a = 1;
/*@ behavior ok:
assumes a > 0;
ensures \true;
*/
return 3;
}
</pre>
Command:
<pre>
frama-c -wp test.c
</pre>
Log:
<pre>
[wp] [CFG] Goal test_stmt_ok_post : Valid (Unreachable)
[wp] [CFG] Goal test_stmt_ok_assume : Valid (Unreachable)
[kernel] failure: only the kernel should set the status of property assumes
a > 0
[kernel] Current source was: test.c:1
The full backtrace is:
Raised at file "src/kernel_services/plugin_entry_points/log.ml" (inlined), line 568, characters 24-31
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 939, characters 6-44
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 562, characters 9-16
Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 565, characters 9-16
Called from file "src/kernel_services/ast_data/property_status.ml", line 538, characters 4-109
Called from file "src/kernel_services/ast_data/property_status.ml" (inlined), line 551, characters 42-80
Called from file "src/plugins/wp/wpAnnot.ml", line 81, characters 4-71
Called from file "list.ml", line 85, characters 12-15
Called from file "list.ml", line 85, characters 12-15
Called from file "src/plugins/wp/wpAnnot.ml", line 1243, characters 10-38
Called from file "src/plugins/wp/wpAnnot.ml", line 1258, characters 12-28
Called from file "src/plugins/wp/wpAnnot.ml", line 1271, characters 16-68
Called from file "src/plugins/wp/Generator.ml", line 108, characters 4-67
Called from file "map.ml", line 270, characters 20-25
Called from file "src/plugins/wp/Generator.ml", line 136, characters 4-39
Called from file "src/plugins/wp/register.ml", line 654, characters 15-40
Called from file "src/libraries/stdlib/extlib.ml", line 299, characters 14-17
Re-raised at file "src/libraries/stdlib/extlib.ml", line 299, characters 41-48
Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12
Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12
Called from file "queue.ml", line 105, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 37, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 789, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 819, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8
Frama-C aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
</pre>
## Attachments
- [test.c](/uploads/2597c1f73c5b7b83511f003173086460/test.c)https://git.frama-c.com/pub/frama-c/-/issues/246WP is not able to validate a statically declared structure followed by a memset2021-02-22T12:57:18ZPatricia MouyWP is not able to validate a statically declared structure followed by a memsetID0002387:
**This issue was created automatically from Mantis Issue 2387. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002387:
**This issue was created automatically from Mantis Issue 2387. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002387 | Frama-C | Plug-in > wp | public | 2018-07-11 | 2018-09-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pmo | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
By using a clean way to declare the structure, WP fails to validate the structure but by using a "dirty" way, it works !
#include <string.h>
typedef struct {
int i;
float f;
} stest;
void notclean_but_valid() {
char b[sizeof(stest)];
stest *s = b;
memset(s, 0, sizeof(stest));
}
void clean_but_invalid() {
stest s;
memset(&s, 0, sizeof(stest));
}
### Steps To Reproduce :
frama-c -wp-model typed_cast_ref -wp struc.chttps://git.frama-c.com/pub/frama-c/-/issues/2673[WP] non-matching of strategies with logical operators2024-03-04T10:14:59ZNikolai Kosmatov[WP] non-matching of strategies with logical operators### Steps to reproduce the issue
On the attached example
[logical_pattern.c](/uploads/0bb48f222b06fb2a470e76d756be35f0/logical_pattern.c)
running the following command
`frama-c-gui logical_pattern.c -wp -wp-rte -wp-prover=alt-ergo,...### Steps to reproduce the issue
On the attached example
[logical_pattern.c](/uploads/0bb48f222b06fb2a470e76d756be35f0/logical_pattern.c)
running the following command
`frama-c-gui logical_pattern.c -wp -wp-rte -wp-prover=alt-ergo,tip -wp-timeout 1 -wp-prop post`
to apply a strategy with Split does not seem to accept the pattern and to match the precondition with logical operations `&&` and `||`
```
strategy FastAltErgo: \prover("alt-ergo", 1); // run Alt-Ergo for 1 sec.
strategy EagerAltErgo: \prover("alt-ergo",10); // run Alt-Ergo for 10 sec.
strategy SplitProver:
FastAltErgo,
\tactic("Wp.split"
,\pattern( ((A && B) || (C && D)) )
,\children(EagerAltErgo)
),
EagerAltErgo;
proof SplitProver: post;
```
### Expected behaviour
According to documentation, ACSL logical operations are recognized and after a successful matching, a script is created with two subgoals (to be completed).
### Actual behaviour
Syntax error is reported (Invalid pattern. Ignoring global annotation).
### Contextual information
- Frama-C installation mode: opam from GIT pub
- Frama-C version: first version of the strategy mechanism (https://git.frama-c.com/pub/frama-c.git#3396bd), also the recent update on master on pub (by the branch fix/wp/strategies)
- Plug-in used: WP with Why3 1.6.0 and Alt-Ergo 2.4.3
- OS name: Ubuntu
- OS version: 22.04Loï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 Blanchard