frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-05-28T09:30:55Zhttps://git.frama-c.com/pub/frama-c/-/issues/2[wp] non-provable local typing constraints in lemmas2021-05-28T09:30:55ZJens Gerlach[wp] non-provable local typing constraints in lemmas# Steps to reproduce the issue
The attached archive contains the ACSL function `Count` together with several lemma.
Also contained are
- a Makefile
- a coq proof in file `wp0.script.20` for lemma `CountBounds` that works for Frama-C 20...# Steps to reproduce the issue
The attached archive contains the ACSL function `Count` together with several lemma.
Also contained are
- a Makefile
- a coq proof in file `wp0.script.20` for lemma `CountBounds` that works for Frama-C 20
- an attempt of a coq proof in file `wp0.script.21` for lemma `CountBounds` that fails for Frama-C 21
- The files `CountBounds.v.20` and `CountBounds.v.21` contain the coq code as extracted from CoqIde
# Expected behaviour
My problem is that I am unable to adapt the coq proof that worked fro Frama-C 20 to the newer version of Frama-C.
# Actual behaviour
I suspect that this is related to changes in the generated Coq code of the VC of lemma `CountBounds`
This can be best seen when calling `diff CountBounds.v.20 CountBounds.v.21`.
```
$ diff CountBounds.v.20 CountBounds.v.21
39,40c39,40
< (((t.[ (shift_sint32 a x) ]) <> i_2)%Z) -> ((i < i_1)%Z) ->
< ((is_sint32 i_2%Z)) ->
---
> let x_1 := (t.[ (shift_sint32 a x) ])%Z in ((x_1 <> i_2)%Z) ->
> ((i < i_1)%Z) -> ((is_sint32 i_2%Z)) -> ((is_sint32 x_1)) ->
```
# Fix ideas
I think the issue is caused by the condition `((is_sint32 x_1))` for the newly introduced term `x_1 := (t.[ (shift_sint32 a x) ])%Z`. I haven't found a way to satisfy the condition `((is_sint32 x_1))` and I suspect that it is not possible.
If it is possible, then I apologise and ask for a hint.
Regards
Jens Gerlach
[CoqFramac21.tar](/uploads/e95b883ad30f134748c5a7289fa6902d/CoqFramac21.tar)Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/3[wp] shall use per-behaviour assigns at call sites2021-08-05T08:49:16ZNikolai Kosmatov[wp] shall use per-behaviour assigns at call sites# Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *20.0 (Calcium)* (as reported by `frama-c -version`)
- Plug-in used: *WP*
- OS name: *Ubuntu*
- OS version: *19.10*
*Please add specific information deemed...# Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *20.0 (Calcium)* (as reported by `frama-c -version`)
- Plug-in used: *WP*
- OS name: *Ubuntu*
- OS version: *19.10*
*Please add specific information deemed relevant with regard to this issue.*
# Steps to reproduce the issue
frama-c-gui -wp behavior_assigns.c
*Please indicate here steps to follow which reproduce the issue.*
See the attached file for a minimal example. [behavior_assigns.c](/uploads/b4eaee1cce8750d4749d64794e79883c/behavior_assigns.c)
# Expected behaviour
The assigns clause of caller can be proved.
# Actual behaviour
The assigns clause of caller is not proved.
The assigns clauses specific for particular behaviors in a callee cannot be used in the caller
under specific conditions falling into such behavior(s) to prove a more restrictive assigns clause
in the caller, rather than the most general assigns taking into account all behaviors of the callee.
# Fix ideas
Obvious workarounds include additional postconditions, that make the specifications more complex and
make the proof with WP less powerful. Matching the callee's behaviors to prove stronger assigns clauses
in the caller could be helpful.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/16[wp] unsoundness for base-offset2021-02-22T14:00:48ZLoïc Correnson[wp] unsoundness for base-offsetComputation of WP for `\offset()` in MemTyped is actually using a function `base_offset(idx)` that max index of cells in memory to their actual offset in bytes. Example:
```
struct S {
int f; // index 0, offset 0
long g; // in...Computation of WP for `\offset()` in MemTyped is actually using a function `base_offset(idx)` that max index of cells in memory to their actual offset in bytes. Example:
```
struct S {
int f; // index 0, offset 0
long g; // index 1, offset 4
int h; // index 2, offset 12
}; // size,=3, sizeof=16
```
This function is left mostly unspecified, and is required to be monotonic.
This prevent WP from computing exact offsets, but is _not_ a problem, this is just an under-specification.
Moreover, the index-offset correspondance _could_ be formally specified for each known base-address from its type (if it does not changed, as it is assumed in MemTyped).
However, this function is currently the _same_ for all base address, which is certainly incorrect and might cause unsoundness when asking WP for computing `\offset()` within variables of different types.
It **shall** be modelled as `base_offset(base, index)`.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/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/41Z3 and CVC4 working for Frama-C 22 (Titanium) beta after some initial problems2021-04-13T17:49:41ZJens GerlachZ3 and CVC4 working for Frama-C 22 (Titanium) beta after some initial problems**I updated the title after figuring out a solution**
- [x] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [x] the issue has not yet been reported on our [BTS](https://bts.frama-c.com);
- ...**I updated the title after figuring out a solution**
- [x] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [x] the issue has not yet been reported on our [BTS](https://bts.frama-c.com);
- [x] you installed Frama-C as prescribed in the [instructions](INSTALL.md).
# Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *22.0-beta (Titanium)*
- Plug-in used: *WP*
- OS name: *Xubuntu*
- OS version: *Ubuntu 20.04.1 LTS*
*Please add specific information deemed relevant with regard to this issue.*
I am able to use the options `-wp-prover Alt-Ergo -wp-prover native:coq ` with *ACSL by Example*.
However when using either `-wp-prover Z3` or `-wp-prover z3` I receive the following error message.
(Note that `z3` (4.8.6) has been installed and that it has been successfully registered with `why3 config --full-config`)
```
[kernel] Parsing find.c (with preprocessing)
[rte] annotating function find
[wp] User Error: Prover 'z3' not found in why3.conf
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 25 goals scheduled
[wp] Proved goals: 25 / 25
Qed: 16 (2ms-6ms-20ms)
Alt-Ergo 2.3.3: 9 (5ms-12ms) (87)
[wp] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Plug-in wp aborted: invalid user input.
```
Similar with `CVC4` and `cvc4`.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/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/55z3 ERROR: unknown parameter 'model_compress'2021-02-22T12:52:03Zrwmjonesz3 ERROR: unknown parameter 'model_compress'ID0002509:
**This issue was created automatically from Mantis Issue 2509. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002509:
**This issue was created automatically from Mantis Issue 2509. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002509 | Frama-C | Plug-in > wp | public | 2020-10-15 | 2020-10-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | rwmjones | **Assigned To** | correnson | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Apparently z3 dropped this parameter and replaced it with "model.compact" without bothering with backward compatibility: https://github.com/Z3Prover/z3/issues/2704#issuecomment-554489258
### Steps To Reproduce :
Use z3 4.8.9, turn on debugging.
<6.827036,call_prover>Call_provers: actual command is:
z3 -smt2 -t:10000 sat.random_seed=42
model_compress=false nlsat.randomize=false
smt.random_seed=42 -st
/tmp/why_b9efc2_zilch-T-wp_goal.smt2
ERROR: unknown parameter 'model_compress'https://git.frama-c.com/pub/frama-c/-/issues/58Wp crashes on a recursive function2021-02-22T13:34:36ZFrédéric LoulergueWp crashes on a recursive functionID0002420:
**This issue was created automatically from Mantis Issue 2420. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002420:
**This issue was created automatically from Mantis Issue 2420. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002420 | Frama-C | Plug-in > wp | public | 2018-12-28 | 2020-09-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | frederic.loulergue@nau.edu | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Mac | **OS** | macOS | **OS Version** | Mojave 10.14.1 |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
frama-c -wp tmp.c give the following trace. If the recursive call in e_get is removed, no crash.
[kernel] Parsing tmp.c (with preprocessing)
[wp] Running WP plugin...
[kernel] Current source was: tmp.c:14
The full backtrace is:
Raised by primitive operation at file "src/kernel_services/ast_data/statuses_by_call.ml", line 198, characters 11-65
Called from file "list.ml", line 82, characters 20-23
Called from file "src/kernel_services/ast_data/statuses_by_call.ml", line 231, characters 6-150
Called from file "src/plugins/wp/cil2cfg.ml", line 859, characters 6-35
Called from file "src/plugins/wp/cil2cfg.ml", line 821, characters 21-51
Called from file "src/plugins/wp/cil2cfg.ml", line 890, characters 20-52
Called from file "src/plugins/wp/cil2cfg.ml", line 821, characters 21-51
Called from file "src/plugins/wp/cil2cfg.ml", line 821, characters 21-51
Called from file "src/plugins/wp/cil2cfg.ml", line 821, characters 21-51
Called from file "src/plugins/wp/cil2cfg.ml", line 890, characters 20-52
Called from file "src/plugins/wp/cil2cfg.ml", line 821, characters 21-51
Called from file "src/plugins/wp/cil2cfg.ml", line 890, characters 20-52
Called from file "src/plugins/wp/cil2cfg.ml", line 821, characters 21-51
Called from file "src/plugins/wp/cil2cfg.ml", line 1216, characters 13-47
Called from file "src/plugins/wp/cil2cfg.ml", line 1248, characters 6-30
Called from file "src/libraries/project/state_builder.ml", line 565, characters 17-22
Called from file "src/plugins/wp/cil2cfg.ml" (inlined), line 1288, characters 13-33
Called from file "src/plugins/wp/wpAnnot.ml", line 1291, characters 12-26
Called from file "src/plugins/wp/wpAnnot.ml", line 1307, characters 12-28
Called from file "src/plugins/wp/wpAnnot.ml", line 1320, characters 16-68
Called from file "src/plugins/wp/Generator.ml", line 109, characters 4-67
Called from file "map.ml", line 291, characters 20-25
Called from file "src/plugins/wp/Generator.ml", line 137, characters 4-39
Called from file "src/plugins/wp/register.ml", line 686, characters 15-40
Called from file "src/libraries/stdlib/extlib.ml", line 332, characters 14-17
Re-raised at file "src/libraries/stdlib/extlib.ml", line 332, characters 41-48
Called from file "src/libraries/stdlib/extlib.ml", line 333, characters 2-12
Called from file "src/libraries/stdlib/extlib.ml", line 333, characters 2-12
Called from file "queue.ml", line 105, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 792, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 822, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 229, characters 4-8
Unexpected error (Stack overflow).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is 18.0 (Argon).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
## Attachments
- [tmp.c](/uploads/db0023943b4d5bc953e110a335fcc7c7/tmp.c)https://git.frama-c.com/pub/frama-c/-/issues/59error in generated proof obligation2021-02-22T12:52:08ZJens Gerlacherror in generated proof obligationID0002501:
**This issue was created automatically from Mantis Issue 2501. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002501:
**This issue was created automatically from Mantis Issue 2501. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002501 | Frama-C | Plug-in > wp | public | 2020-03-10 | 2020-06-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | AllanBlanchard | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | Linux, macOS | **OS Version** | - |
| **Product Version** | Frama-C 20-Calcium | **Target Version** | - | **Fixed in Version** | Frama-C 21-Scandium |
### Description :
The attached file 'issue.c' contains a simplified (but still not very small) example of an issue I have within ACSL by Example.
There is lemma R_2 for the logic function R.
The definition of R uses the logic function F contained in the axiomatic block A.
When trying to verify R_2 with the command line below I obtain the message
[Why3 Error] anomaly: Failure("Can't find 'L_F' in why3 namespace")
frama-c -wp -wp-prover alt-ergo -wp-prover native:coq issue.c
[kernel] Parsing issue.c (with preprocessing)
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 2 goals scheduled
[wp] [Failed] Goal typed_lemma_R_2
Alt-Ergo 2.3.1: Failed
[Why3 Error] anomaly: Failure("Can't find 'L_F' in why3 namespace")
Coq: Unknown
[wp] [Cache] found:1
[wp] Proved goals: 1 / 2
Qed: 0
Coq: 0 (unknown: 1)
Alt-Ergo 2.3.1: 1 (10ms) (23) (cached: 1) (failed: 1)
When looking at the generated verification condition with Coq I found the following:
The generated hypothesis 'FixL_R' uses of course the function 'L_F'.
However, the necessary import clause 'Require Import A_A.' comes only AFTER the definition of 'FixL_R'.
### Additional Information :
There is a work-around by calling the helper function 'Fix' in the definition of R (see the comment in the code).
The problem also "disappears' if lemma 'R_1' is removed (but I don't have this option).
While looking at this problem, I noticed that in general coq definitions and import clauses are interspersed in the verification conditions...
## Attachments
- [issue.c](/uploads/e4b3b207592281459b4d9e552d904f4a/issue.c)https://git.frama-c.com/pub/frama-c/-/issues/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/75Failure to detect qed libraries when running wp2021-02-22T12:52:46Zmantis-gitlab-migrationFailure to detect qed libraries when running wpID0002389:
**This issue was created automatically from Mantis Issue 2389. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002389:
**This issue was created automatically from Mantis Issue 2389. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002389 | Frama-C | Plug-in > wp | public | 2018-07-17 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | timourf | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Linux | **OS Version** | - |
| **Product Version** | - | **Target Version** | Frama-C 17-Chlorine | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
This is not a problem with this particular code, but I will include it anyways for the sake of completeness and reproducibility.
With the following C code "average.c"
=============================================
/*@ ensures \result == \abs(x); */
double abs(double x) {
if (x >= 0) return x;
else return (-x);
}
/*@ requires 0x1p-967 <= C <= 0x1p970;
@ ensures \result == \round_double(\NearestEven, (x+y)/2);
@ */
double average(double C, double x, double y) {
if (C <= abs(x)) return x/2+y/2;
else return (x+y)/2;
}
=============================================
running the command
>frama-c -wp -wp-model +float -wp-prover "why3:coq" -wp-print average.c
produces the following output
=============================================
[kernel] Parsing average.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] average.c:9: Warning:
Builtin \NearestEven not defined
[wp] 2 goals scheduled
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /home/timourf/.opam/default/share/frama-c/wp/why3/why3.conf
Fatal error while loading driver file '/home/timourf/.opam/default/share/why3/drivers/coq.drv':
File "/home/timourf/.opam/default/share/frama-c/wp/why3/coq.drv", line 24, characters 7-14:
Library file not found: qed
------------------------------------------------------------
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /home/timourf/.opam/default/share/frama-c/wp/why3/why3.conf
Fatal error while loading driver file '/home/timourf/.opam/default/share/why3/drivers/coq.drv':
File "/home/timourf/.opam/default/share/frama-c/wp/why3/coq.drv", line 24, characters 7-14:
Library file not found: qed
... (less relevant output) ...
=============================================
the line referenced in coq.drv is
"theory qed.Qed meta "realized_theory" "qed.Qed", "Qed" end
### Additional Information :
Product Version: Frama-C-Chlorine-20180501 **not an option in reporting tool**
I reported this here because the error seems to be with the configurations files generated by frama-c in the frama-c/wp directory, but I can't be sure that the problem isn't with why3 itself. I'm still very new to using these tools.
Note: the "Builtin \NearestEven not defined" seems to be a separate bug, referenced here: https://lists.gforge.inria.fr/pipermail/frama-c-discuss/2016-July/005117.html
### Steps To Reproduce :
Installed the following via OPAM
coq 8.8.0 (because 8.8.1+ reports not supported by why3)
why3-coq 1.0.0
frama-c-chlorine-20180501
error persists after uninstalling and re-installing all of the above
## Attachments
- [coq.drv](/uploads/7d46c6d1e6ee9a9a0ee6e60e0dbb72f7/coq.drv)
- [wp.driver](/uploads/9801629381f7c222b5f698622a1d6551/wp.driver)https://git.frama-c.com/pub/frama-c/-/issues/76conditional input annotations result in why3 type errors2021-02-22T12:52:48Zmantis-gitlab-migrationconditional input annotations result in why3 type errorsID0002394:
**This issue was created automatically from Mantis Issue 2394. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002394:
**This issue was created automatically from Mantis Issue 2394. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002394 | Frama-C | Plug-in > wp | public | 2018-08-23 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | timourf | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | GNU/Linux | **OS Version** | Debian 9 |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
I am trying to put conditions on my function specification that specify return values conditioned on special input values. A minimal example is as follows:
/*@ requires 0 <= t <= 1;
@ ensures t == 1.f ==> \result == b;
@ assigns \nothing
*/
float interpolate(float a, float b, float t) { ... }
Why3 (stderr) reports:
===================================================================================
File "/tmp/wp0a3ed9.dir/typed/interpolate_Why3_ide.why", line 20, characters 11-26:
This term has type real -> real, but is expected to have type real
===================================================================================
The "problem line" is "ensures t == 1.f ==> \result == b;"
This seems to be a problem between wp and why3. The error persists with every external prover I use with why3. The list of provers I've tried is [Z3,CVC3,CVC4,Alt-Ergo,Gappa], and the only exception is why3:coq (see issue 0002389).
### Additional Information :
why3 0.88.3
frama-c chlorine 20180502
### Steps To Reproduce :
see attached file "buggy.c"
run:
> frama-c -wp -wp-prover "why3:XXX" buggy.c
where XXX is any prover installed with why3
## Attachments
- [buggy.c](/uploads/323bd028ec39d43d549eae1d88957797/buggy.c)https://git.frama-c.com/pub/frama-c/-/issues/77suggest to provide results of commandl-line "-wp-prop" evaluation in a file i...2021-02-22T12:52:49ZJens Gerlachsuggest to provide results of commandl-line "-wp-prop" evaluation in a file in the wp-out directoryID0002371:
**This issue was created automatically from Mantis Issue 2371. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002371:
**This issue was created automatically from Mantis Issue 2371. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002371 | Frama-C | Plug-in > wp | public | 2018-03-22 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | none | **Severity** | feature | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.10 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
I ran
"frama-c -wp -wp-out without_lemma -wp-gen -wp-prover why3 -wp-prop=-@lemma aaa.c"
and then
"frama-c -wp -wp-out with_lemma -wp-gen -wp-prover why3 aaa.c"
on the attached file.
After that, "diff -r without_lemma with_lemma" reports no difference between both generated directories.
It is clear that Frama-C needs to generate why3 code for the lemma in both cases, since it might be *used* in some proof.
However, as a consequence, there is no information in the generated directories about which lemmas should be proven. It would be nice if in the long run such information could be provided, e.g. in a separate file.
### Additional Information :
Our application scenario is the following:
We run (one of) the above command(s) on a local computer to generate why3 files; then we transfer them to a more powerful remote computer, and run the provers there. On the remote computer, we would like to have the list of lemmas-to-be-proven available.
Note that arbitrarily complex combinations of "-wp-prop" could exclude some lemmas from being proven and include others. Therefore, we don't want to perform the evaluation of command-line args "-wp-prop=..." ourselves again (this is difficult, anyway, cf. #2285).
## Attachments
- [aaa.c](/uploads/ef6c959b3687621110ddcbd77ab2b906/aaa.c)https://git.frama-c.com/pub/frama-c/-/issues/78ill-typed alt-ergo proof obligation2021-02-22T14:01:05ZVirgile Prevostoill-typed alt-ergo proof obligationID0001484:
**This issue was created automatically from Mantis Issue 1484. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001484:
**This issue was created automatically from Mantis Issue 1484. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001484 | Frama-C | Plug-in > wp | public | 2013-09-25 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
Using WP with RTE enabled on the attached file results in proof obligations rejected as ill-typed by Alt-Ergo.
### Additional Information :
Without rte, everything is fine. With RTE, the resulting proof obligation is the following:
forall x_0 : int.
let x_1 = to_sint32(neqb(0, x_0)) : int in
let x_2 = to_uint8(x_0 - (ite((eqb(0, x_0)), 0, 1))) : int in
is_uint8(x_0) ->
(x_1 <= (2147483648 + x_0)) ->
(x_0 <= (2147483647 + x_1)) ->
is_uint8(x_2) ->
(x_2 <= x_0)
the definition of x_1 is lacking an ite(_,0,1) conversion, as shown in the definition of x_2. x_1 does not appear in the PO without RTE, as it is only used in the (x<=2147483648 + x_0) and x_0 <= (2147483647 + x_1) hypotheses reflecting the RTE-generated hypotheses.
Note that writing the RTE-generated hypotheses in the code (and launching WP without -wp-rte) results in warning cast from (boolean) not yet implemented, and degenerated goals.
### Steps To Reproduce :
frama-c -wp -wp-rte t.c
## Attachments
- [t.c](/uploads/085bb97c670f033ea923101dfd6b3a57/t.c)https://git.frama-c.com/pub/frama-c/-/issues/80known, but inferrable, yet not inferred, property not given as precodition to...2021-02-22T12:52:55ZJochen Burghardtknown, but inferrable, yet not inferred, property not given as precodition to proversID0002330:
**This issue was created automatically from Mantis Issue 2330. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002330:
**This issue was created automatically from Mantis Issue 2330. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002330 | Frama-C | Plug-in > wp | public | 2017-10-26 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Phosphorus-20170501 | **OS** | - | **OS Version** | xubuntu 17.04 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
Running "frama-c -wp foo.c -wp-out wp-out -wp-prop=D" on the attached program fails to prove the property D, although it follows immediately from A and C.
A look at the generated file "foo_assert_D_Alt-Ergo.mlw" reveals that the condition "y<=15" from C is not given to Alt-Ergo, while "0<=y" is.
If the former is inserted into the mlw file, Alt-Ergo proves the goal without problems.
Probably, "y<=15" is considered a trivial consequence of "y==(x&0xf)" by Qed; however, it shouldn't, since (e.g.) Alt-Ergo is unable to to infer this: goal C cannot be proven by Alt-Ergo.
### Steps To Reproduce :
Name translation c -> mlw for convenience:
x -> i
y -> x
z -> x_1
## Attachments
- [foo.c](/uploads/2114c61520580b96d2b67fca503e569d/foo.c)https://git.frama-c.com/pub/frama-c/-/issues/81Error in coq code generated by wp2021-02-22T13:34:31Zmantis-gitlab-migrationError in coq code generated by wpID0001806:
**This issue was created automatically from Mantis Issue 1806. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001806:
**This issue was created automatically from Mantis Issue 1806. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001806 | Frama-C | Plug-in > wp | public | 2014-06-12 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | davyg | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
There is a typing error with some code generated by wp.
For example this script :
_Bool g()
{
return 0;
}
//@ensures x == (!!\result == !!x);
_Bool f(_Bool x)
{
return g();
}
When using prover coq from wp generates :
Goal
forall (f_0 x_0 : Z),
((is_uint32 f_0%Z)) ->
((is_uint32 x_0%Z)) ->
((((Zneq_bool 0 x_0))
= ((Zeq_bool ((Zneq_bool 0 f_0)) ((Zneq_bool 0 x_0)))))%Z)%Z.
Proof.
(* auto with zarith. *)
Qed.
which produce this coq error on "Zneq_bool 0 f_0":
Error: In environment
f_0 : int
x_0 : int
The term "Zneq_bool 0 f_0" has type "bool" while it is expected to have type
"int".
### Steps To Reproduce :
Just use the C example with wp/coq as prover (with the gui for example because else wp consider that the script fails and does not print the error)https://git.frama-c.com/pub/frama-c/-/issues/82\false provable from recursive logic definition2021-02-22T14:01:06ZJochen Burghardt\false provable from recursive logic definitionID0002338:
**This issue was created automatically from Mantis Issue 2338. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002338:
**This issue was created automatically from Mantis Issue 2338. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002338 | Frama-C | Plug-in > wp | public | 2017-12-18 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | Ubuntu 17.04 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
Running "frama-c -wp foo.c -wp-prover alt-ergo -wp-prover eprover" on the attached file proves all goals, including a lemma "Check" which just says "\false", from nothing but a recursive definition of a logic int function.
The latter is well-founded since its only recursive call uses a parameter value n==0 which immediately employs the base case.
The problem disappears
(1) when "integer" is used as result type and as 3rd parameter type,
(2) when "a[]" is omitted,
(3) when lemma "Alpha" is renamed to a name lexicographically after "Check", or
(4) when "cvc3" or "cvc4-15" is used instead of "eprover".
The problem remains, however, when "z3" is used.
## Attachments
- [foo.c](/uploads/340c077780845d501a0ff97285b34e30/foo.c)
- [diff.txt](/uploads/2fe9c477a8a70ef0a92fbd1b0e09d964/diff.txt)
- [eprover.input](/uploads/ad8ebe320b201413c34ff6998234e1e0/eprover.input)https://git.frama-c.com/pub/frama-c/-/issues/86WP warning not clear2021-02-22T12:53:10ZJens GerlachWP warning not clearID0002482:
**This issue was created automatically from Mantis Issue 2482. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002482:
**This issue was created automatically from Mantis Issue 2482. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002482 | Frama-C | Plug-in > wp | public | 2019-10-22 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Linux, macOS | **OS Version** | - |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
When I run
frama-c -wp -wp-rte -wp-model Typed f.c
on the attached file, I obtain the warning
[wp] Warning: Memory model hypotheses for function 'f':
/*@ behavior typed: requires \separated(p+(..),a); */
void f(int *a);
However, when I add this requirement by removing the corresponding comment in the contract,
then the warning still occurs.
What can I do to make this warning disappear?
## Attachments
- [f.c](/uploads/bec418c0cc734cf361d31b115a8835b1/f.c)https://git.frama-c.com/pub/frama-c/-/issues/87frama-c/wp generates invalid why32021-02-22T13:35:23Zmantis-gitlab-migrationframa-c/wp generates invalid why3ID0002471:
**This issue was created automatically from Mantis Issue 2471. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002471:
**This issue was created automatically from Mantis Issue 2471. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002471 | Frama-C | Plug-in > wp | public | 2019-08-13 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | abakst | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | macOS | **OS Version** | 10.14 |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
There appears to be an issue with some of the `why3` files that get generated from user axiomatic definitions. I've installed `frama-c` using the `nix-pkgs` on the master branch, and hence have version `19.0`, and `why3` version `1.2.0`.
```c
/*@ axiomatic maps { type model_digit = octet | sextet;
logic integer foo(model_digit i);
}
*/
int foo() {
//@assert \forall int i; i == foo(octet);
return 0;
}
```
Given the (silly) program above in `simple.c`, I get the following behavior
```bash
$ frama-c -wp -wp-prover z3-ce simple.c
[kernel] Parsing simple.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] WPOUT/typed/A_maps.why:13: User Error: why3 syntax error
[wp] [z3-ce] Goal typed_foo_assert : Failed
why3 syntax error
[wp] Proved goals: 0 / 1
Why3 (z3-ce): 0 (failed: 1)
[wp] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Plug-in wp aborted: invalid user input.
```
The A_maps.why file contains:
```
(* ---------------------------------------------------------- *)
(* --- Axiomatic 'maps' --- *)
(* ---------------------------------------------------------- *)
theory A_maps
use bool.Bool
use int.Int
use int.ComputerDivision
use real.RealInfix
use Qed.Qed
use int.Abs as IAbs
use map.Map
type a_model_digit | c_octet | c_sextet
function l_foo a_model_digit : int
end
```
The error seems to be on the line (I'd imagine there should be an '=' but I am not a why3 user)
```
type a_model_digit | c_octet | c_sextet
```
### Steps To Reproduce :
Copy the C source into a new file, simple.c, and attempt to run the command:
frama-c -wp -wp-prover z3-ce simple.c
## Attachments
- [bug.c](/uploads/8df040c765825ec3d66d84e371757e44/bug.c)https://git.frama-c.com/pub/frama-c/-/issues/91quantifiers over logic types do not restrict to valid instances2021-04-15T09:37:11Zmantis-gitlab-migrationquantifiers over logic types do not restrict to valid instancesID0002497:
**This issue was created automatically from Mantis Issue 2497. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002497:
**This issue was created automatically from Mantis Issue 2497. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002497 | Frama-C | Plug-in > wp | public | 2020-01-30 | 2020-02-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | amosr | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 20-Calcium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi,
When I quantify over an unsigned char, the resulting formula uses the is_uint8 predicate to ensure that it only considers valid uint8s. However, if I define a logic type that contains an unsigned char, there is no corresponding is_ predicate for the logic type:
> //@ type logic_type_with_u8 = value(unsigned char);
This type is represented in the generated formula as an unbounded int rather than an unsigned char. This means that quantifying over the logic type includes more values than are allowed - for example, `\forall logic_type_with_u8 l` has to prove that the predicate is true even for values that won't fit in a u8.
As a concrete example, I expect the following to hold, but it does not:
> lemma u8_is_valid: \forall logic_type_with_u8 n; \exists unsigned char u; n == value(u);
Thanks,
Amos
### Additional Information :
PS. I could not test on the latest version from git - how do I get (read-only) access to the git repository?
### Steps To Reproduce :
Download file logic_type_is_valid.c and run with WP:
> frama-c -wp logic_type_is_valid.c
The lemma in this file should hold, but does not.
## Attachments
- [logic_type_is_valid.c](/uploads/ec550b694fa472b8bd9d08dc35a76d72/logic_type_is_valid.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/101-wp-out missing output for Why3 provers in Frama-C 20 beta2023-07-21T13:31:03ZJens Gerlach-wp-out missing output for Why3 provers in Frama-C 20 betaID0002485:
**This issue was created automatically from Mantis Issue 2485. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002485:
**This issue was created automatically from Mantis Issue 2485. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002485 | Frama-C | Plug-in > wp | public | 2019-11-08 | 2019-11-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | Linux | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
When the attached programme is processed with
frama-c -wp -wp-rte -wp-prover native:alt-ergo -wp-out abs.wp abs.c
then the output directory 'abs.wp/typed' contains three files
abs_ensures_3_Alt-Ergo.mlw
abs_ensures_3_Alt-Ergo.out
abs_ensures_3.ergo
When using the command line
frama-c -wp -wp-rte -wp-prover alt-ergo -wp-out abs.wp abs.c
then the output directory 'abs.wp/typed' contains only the generated proof obligation
abs_ensures_3_Why3_Alt_Ergo_2_3_0.why
(similiarly when using another Why3 prover, such as cvc4)
Is there a way to output also the result for Why3 provers?
## Attachments
- [abs.c](/uploads/9fd4b3dcc0cf8490758da51b696be918/abs.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/102alt-ergo support in Frama-C 20 beta2021-04-14T07:30:38ZJens Gerlachalt-ergo support in Frama-C 20 betaID0002484:
**This issue was created automatically from Mantis Issue 2484. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002484:
**This issue was created automatically from Mantis Issue 2484. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002484 | Frama-C | Plug-in > wp | public | 2019-11-08 | 2019-11-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | Linux | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
This is a hint to (better) describe the transition from using alt-ergo in Frama-C 19 and 20.
If it is already described, then I apologize.
In Frama-C 19 and before one uses
-wp-prover alt-ergo for the native interface and
-wp-prover why3:alt-ergo for the Why3 interface
In Frama-C 20 the respective options are
-wp-prover native:alt-ergo for the native interface and
-wp-prover alt-ergo
I propose that it is described with other things in a short transition document.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/103Eprover in Frama-C 20 beta2021-04-15T09:36:20ZJens GerlachEprover in Frama-C 20 betaID0002483:
**This issue was created automatically from Mantis Issue 2483. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002483:
**This issue was created automatically from Mantis Issue 2483. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002483 | Frama-C | Plug-in > wp | public | 2019-11-08 | 2019-11-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Linux | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
I played a bit with various automatic provers in the beta
alt-ergo (2.3.0), native:alt-ergo (2.3.0), cvc4 (1.6), cvc3 (2.4.1), z3 (4.8.6) are recognized.
Eprover (2.4), on the other hand, is not recognized.
To be honest, Eprover is not such a great prover, but it has helped us discovering inconsistencies in our specifications.
Is there a specific reason, Eprover is not supported?
Attached is the error message.
### Steps To Reproduce :
$ frama-c -wp -wp-rte -wp-prover eprover -wp-out abs.wp abs.c
[kernel] Parsing abs.c (with preprocessing)
[rte] annotating function abs_int
[wp] 6 goals scheduled
[wp] [Eprover 2.4] Goal typed_abs_int_ensures_3 : Failed
[Why3 Error] Unknown printer 'tptp-fof'
[wp] [Cache] not used
[wp] Proved goals: 5 / 6
Qed: 5 (0.60ms-3ms-6ms)
Eprover 2.4: 0 (failed: 1)
## Attachments
- [abs.c](/uploads/07380fd95e05b2515b8f7dec3a1bad41/abs.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/104readability of coq(?) names2021-02-22T14:01:08ZJens Gerlachreadability of coq(?) namesID0002100:
**This issue was created automatically from Mantis Issue 2100. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002100:
**This issue was created automatically from Mantis Issue 2100. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002100 | Frama-C | Plug-in > wp | public | 2015-03-31 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Consider the following ACSL lemma:
/*@
lemma X : \forall integer a, b; (a+b)*(a-b) == a*a - b*b;
*/
which is automatically discharged by alt-ergo.
When I open the proof obligation in Coq, the lemma looks like follows:
Goal
forall (i_1 i : Z),
(((i_1 * i_1) = ((i * i) + ((i + i_1) * (i_1 - i))))%Z)%Z.
Under Neon the proof coq representation preserves the original names much better
Goal
forall (a_0 b_0 : Z),
(((a_0 * a_0) = ((b_0 * b_0) + ((a_0 + b_0) * (a_0 - b_0))))%Z)%Z.
The problem gets worse with more parameters.
### Steps To Reproduce :
frama-c-gui -wp lemma.c
## Attachments
- [lemma.c](/uploads/61fcccb55ed44434e03f68ed4e4963af/lemma.c)https://git.frama-c.com/pub/frama-c/-/issues/105suggest boolean expressions for "-wp-prop" arguments2021-02-22T12:53:37ZJochen Burghardtsuggest boolean expressions for "-wp-prop" argumentsID0002285:
**This issue was created automatically from Mantis Issue 2285. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002285:
**This issue was created automatically from Mantis Issue 2285. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002285 | Frama-C | Plug-in > wp | public | 2017-02-27 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | won't fix |
| **Priority** | low | **Severity** | feature | **Reproducibility** | always |
| **Platform** | Silicon-20161101 | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Currently, the semantics of "-wp-prop" arguments is unexplained and difficult to understand, when negation and more than one label is used.
For example, using the attached file, "-wp=prop=A,B,-C" selects l4,l5,l6, whereas "-wp-prop=-C,B,A" selects all but l3, and so does "-wp-prop=A,B,c" (although the set of "C"-labelled lemmas is the complement of that of the "c"-labelled lemmas).
I think, parsing arbitrary boolean expressions (built from "!", "&&", "||") isn't more difficult that the current mechanism, but is easier to describe in the manual and to understand.
Alternatively, "-" could be kept as negation, "," could be used for cunjunction only, and the results of multiple args "-wp-prop=X -wp-prop=Y" could be or-ed together; this would at least allow to express arbitrary sets in disjunctive normal form.
### Additional Information :
Complex set expressions arise when labels are used during proof development to attach prover names (and even options) to properties. Using calls like "frama-c -wp -wp-prop=PROVE_WITH_CVC4 -wp-prover=cvc4 ..." can save a lot of proving time that is normally wasted by unsuccessful attempts by unsuitable provers. Other labels that can save time are "TODO", "NEEDS_LONG_TIMEOUT", etc. This way, boolean expressions arise in a natural way; and the user needs to be sure about their semantics, in order not to overlook proof obligations due to splitting by prover.
## Attachments
- [proptest.c](/uploads/969a6dcaeb4f45e418845f21976d9cb7/proptest.c)
- [bbb.c](/uploads/5672cfb09ff165d83ff4c8efc35aacbd/bbb.c)https://git.frama-c.com/pub/frama-c/-/issues/106suggest unique term normalization for lemmas and goals2021-02-22T12:53:39ZJochen Burghardtsuggest unique term normalization for lemmas and goalsID0002329:
**This issue was created automatically from Mantis Issue 2329. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002329:
**This issue was created automatically from Mantis Issue 2329. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002329 | Frama-C | Plug-in > wp | public | 2017-10-09 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | Phosphorus-20170501 | **OS** | - | **OS Version** | xubuntu 17.04 |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-prop g aaa.c" on the attached file fails to prove the assertion "g", although it obviously follows from "f" by applying lemma "lem". One reason for that is of course the inherent incompleteness of SMT provers like Alt-Ergo and Cvc4. However, another reason is that Frama-C's term normalization(1) swaps some arguments of "+", and
(2) performs swaps in the lemma that differ from those performed in the goal.
As a result, in the attached mlw file,
"(L_Foo(a,b+c)=true) -> (L_Bar(a,c+d)=true)"
appears in the lemma, while "(L_Foo(a,i_1+i_2)=true) -> (L_Bar(a,i+i_1)=true)" appears in the goal. The latter is equivalent to
"(L_Foo(a,c+b)=true) -> (L_Bar(a,d+c)=true)"
when expressed in a notation closer to the source-code. Variable "c" is common to L_Foo and L_Bar; note its different positions in the lemma vs. in the goal.
If the goal is changed to "(L_Foo(a,i_2+i_1)=true) -> (L_Bar(a,i_1+i)=true)", it syntactically matches the lemma, and Alt-Ergo proves it in a few milliseconds.
Unless there are good reasons to swap the arguments of "+", they should be kept in their source-code order; this way, the user has a chance to control what is given to the provers.
However, if there *are* good reasons to include argument swapping in term normalization, it should be performed in the same way both in lemmas and in goals.
A possible explanation for the above behavior of Frama-C is that, for some
reason, source-code variable names are transformed to unrelated internal names
in goals, but not in lemmas, and that term normalization just orders arguments
of commutative functions lexicographically (cf. issue #2100).
## Attachments
- [aaa.c](/uploads/86f4cf4ef5586dff6d49e1d6d35ff66e/aaa.c)
- [main_assert_g_Alt-Ergo.mlw](/uploads/4875bf8644ee1246e06bb880e675a7ad/main_assert_g_Alt-Ergo.mlw)https://git.frama-c.com/pub/frama-c/-/issues/107Information on C type of array is not present (in Coq)2021-02-22T13:48:11ZJens GerlachInformation on C type of array is not present (in Coq)ID0002332:
**This issue was created automatically from Mantis Issue 2332. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002332:
**This issue was created automatically from Mantis Issue 2332. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002332 | Frama-C | Plug-in > wp | public | 2017-11-22 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Linux, macOS | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
In the attached file 'array.c' there are two simple predicates 'AllEqual' and 'Constant' that involve int arrays.
There are also two lemmas that relate both predicate.
While it can automatically verified that "Constant" implies "AllEqual" the proof of the "converse" statement fails. When looking at the Coq presentation of "AllEqual" it becomes apparent that Coq only sees an "integer array"; the specific C type (represented by the predicate 'is_sint32') is NOT present at all.
### Additional Information :
The error also occurs in the beta release of Frama-C 16 (Sulfur).
### Steps To Reproduce :
Run the command:
frama-c-gui -no-unicode -wp -wp-prover alt-ergo -wp-prover coq -wp-script 'wp0.script' array.c
## Attachments
- [array.c](/uploads/9ffd5dc713b956ec02a3457ddc3b71c6/array.c)
- [wp0.script](/uploads/eb44100130d8efee641d5565ee82857b/wp0.script)https://git.frama-c.com/pub/frama-c/-/issues/108suggest to supply previous "ensures" as hypotheses in proof obligation of nex...2021-02-22T12:53:43ZJochen Burghardtsuggest to supply previous "ensures" as hypotheses in proof obligation of next "ensures"ID0002336:
**This issue was created automatically from Mantis Issue 2336. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002336:
**This issue was created automatically from Mantis Issue 2336. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002336 | Frama-C | Plug-in > wp | public | 2017-12-08 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | suspended |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.04 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-rte foo.c -wp-out wp-out" on the attached file fails to prove clauses "E1" (as expected) and "E2". The latter is provable from "E1" by axiom "a2". A look at file "main_post_E2_Alt-Ergo.mlw" reveals that "E1" isn't given as hypothesis, and hence axiom "a2" can't be applied.
I cannot judge whether there is good reason for this behavior of Frama-C/Wp. If there isn't, I suggest that "E1" should be given as hypothesis to the proof obligation for "E2", similar to Frama-C/Wp's behavior on consecutive "assigns" clauses. The same applies to statement contracts.
## Attachments
- [foo.c](/uploads/5ad3994f41ed8b1f3aec521fbbf78ded/foo.c)https://git.frama-c.com/pub/frama-c/-/issues/109Crash on loop with global assigns and per-behavior assigns2021-02-22T13:47:26ZBoris YakobowskiCrash on loop with global assigns and per-behavior assignsID0002180:
**This issue was created automatically from Mantis Issue 2180. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002180:
**This issue was created automatically from Mantis Issue 2180. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002180 | Frama-C | Plug-in > wp | public | 2015-10-19 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | correnson | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
frama-c -wp crashes on the following program
/*@ behavior foo:
*/
void main(void)
{
int i;
int t[10];
i = 0;
/*@ loop assigns t[0 .. i];
for foo: loop assigns t[0 .. i]; */
while (i < 10) {
t[i] = 0;
i ++;
}
return;
}https://git.frama-c.com/pub/frama-c/-/issues/111Coq translation of predicate name changes when additional files are processed...2021-02-22T14:00:22ZJochen BurghardtCoq translation of predicate name changes when additional files are processed by Frama-CID0002340:
**This issue was created automatically from Mantis Issue 2340. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002340:
**This issue was created automatically from Mantis Issue 2340. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002340 | Frama-C | Plug-in > wp | public | 2018-01-04 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | Ubuntu | **OS Version** | Ubuntu 17.04 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-script wp0.script -wp-model Typed+ref -wp-prover coq -wp-prop LowerBoundShift equal_range2_cpp.c" succeeds in proving the lemma in line 16 of "equal_range2_cpp.c", using the Coq proof in file "wp0.script".
However, when "lower_bound_cpp.c" is appended as another command line argument to the same call, the lemma is no longer proven.
Using "wp-out" arguments and running a "diff -r" on the resulting directories reveals that the ACSL predicate name "LowerBound" is translated as "P_LowerBound_1_" for the first (succeeding) run, but as "P_LowerBound_2_" for the second (failing) run.
Note that the definitions of the "LowerBound" predicates literally agree in both C files.
The problem disappears when the overloaded 3-argument version of predicate "LowerBound" is omitted in both C files, or when the contract (i.e. the only use of "LowerBound" in that file) is omitted in file "lower_bound_cpp.c".
## Attachments
- [equal_range2_cpp.c](/uploads/a7f339a24fa1ad2c67458331246b61a8/equal_range2_cpp.c)
- [lower_bound_cpp.c](/uploads/1b5c79b560a67c3ba096b9ce8462c3fc/lower_bound_cpp.c)
- [wp0.script](/uploads/a549eb877d73af8f17c7be0a3cad6d0c/wp0.script)https://git.frama-c.com/pub/frama-c/-/issues/112alt-ergo goals generated directly / via why3 differ in provability2021-02-22T12:53:52ZJochen Burghardtalt-ergo goals generated directly / via why3 differ in provabilityID0002353:
**This issue was created automatically from Mantis Issue 2353. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002353:
**This issue was created automatically from Mantis Issue 2353. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002353 | Frama-C | Plug-in > wp | public | 2018-02-01 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sulfur-20171101 | **OS** | - | **OS Version** | Ubuntu 17.04 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
I generated an Alt-Ergo proof obligation for the ensures clause "xxx" (line 1140) of the attached program "search_n_standalone.c" (which was obtained from "search_n" in "Acsl by example" by "gcc -E -C"). When I did this directly (see attached script "fd"), it was proven without problems. However, when I did this via Why3 (see script "fw"), Alt-Ergo responded "Don't know" after 0.1 seconds.
In order to compare both mlw files given to Alt-Ergo, I moved the goal of the via-Why3 file into the direct file; it became provable there. Removing as many axioms and definitions as possible while keeping the (non-)provability, I obtained the files "xxx_direct.mlw" and "xxx_via_why3.mlw". It seems that the former defines and uses "shift_sint32", while the latter does not (it uses "shift" instead). Probably, this is the reason for the different outcomes of Alt-Ergo.
Although the observed issue may not be bug (both mlw files may be semanically equivalent), it might be desirable to unify the proof obligations given to Alt-Ergo on different pathways.
## Attachments
- [search_n_standalone.c](/uploads/79defa5986c7ebb10060cb2d8013dd27/search_n_standalone.c)
- [fd](/uploads/2325b1feb2a0e2c6bc2768f1552ecbf9/fd)
- [fw](/uploads/ade985efb5f8ea0601fa91f90ec1f340/fw)
- [xxx_direct.mlw](/uploads/49efc095c1124c4e87c110c2b7a10bb7/xxx_direct.mlw)
- [xxx_via_why3.mlw](/uploads/28204d54407af26ed64d8841005b5cef/xxx_via_why3.mlw)https://git.frama-c.com/pub/frama-c/-/issues/113Auto-generated assigns clause for a void* argument crashes wp2021-02-22T13:34:40Zmantis-gitlab-migrationAuto-generated assigns clause for a void* argument crashes wpID0002385:
**This issue was created automatically from Mantis Issue 2385. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002385:
**This issue was created automatically from Mantis Issue 2385. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002385 | Frama-C | Plug-in > wp | public | 2018-07-05 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | schollet | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
When using an unspecified function with an void* argument from an external file, the default generated assigns clause for that argument crashes frama-c and WP miss-attributes the error to the user.
Specifically, for an unspecified function foo(void* p), the auto generated assigns clause states that the function assigns *((char *)p+(0 .. )), which is then picked up by WP as an invalid user input.
Version : Frama-C 17 Chlorine
### Additional Information :
The command run :
frama-c -wp test2.c
Error log :
[kernel] Parsing test2.c (with preprocessing)
[kernel:annot:missing-spec] test2.c:7: Warning:
Neither code nor specification for function foo, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] test2.c:11: User Error: Invalid infinite range i_0+(0..)
[kernel] Plug-in wp aborted: invalid user input.
The auto-generated assigns clause (found with frama-c-gui):
/*@ assigns *((char *)thing + (0 ..));
assigns *((char *)thing + (0 ..)) \from *((char *)thing + (0 ..));
*/
Removing the assigns clause for create stops WP from crashing
### Steps To Reproduce :
run `frama-c -wp test2.c` with those 3 provided files
OR:
Write a function and its specification with at least an assigns clause.
Write in it a call to another function.
Write in another file that 2nd function which takes as an argument an void*.
Write the header and include it in the first file.
For the header and the 2nd file, do not write any specification for the function.
run frama-c -wp on the first file
## Attachments
- [assigns.tar.gz](/uploads/7d8c7280dce8dde42f8cce1f86cbef35/assigns.tar.gz)https://git.frama-c.com/pub/frama-c/-/issues/114Newer releases of FramaC produce apparent WP plug-in bug2021-02-22T14:01:18Zmantis-gitlab-migrationNewer releases of FramaC produce apparent WP plug-in bugID0002401:
**This issue was created automatically from Mantis Issue 2401. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002401:
**This issue was created automatically from Mantis Issue 2401. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002401 | Frama-C | Plug-in > wp | public | 2018-10-01 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jmaytac | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
The code in the attached example models a reactive program which interacts with peripherals via memory mapped I/O through an address defined by a constant. While an older version of frama-C (Phosphorus) successfully produced Altergo axiomatizations of boolean logic functions like the "logic boolean isAMessage(mac_t mac)" defined in mac.h,
"
logic boolean isAMessage(mac_t mac) = ((mac->mac_packet.object_high == 0x0A) && (mac->mac_packet.object_low == 0x0A) && (mac->\
mac_packet.payload_length == 0x00));
"
the newer versions produce as AltErgo axiomatization (see out/typed/Axiomatic11.ergo in the attached)
"
function L_isAMessage
() :
bool =
andb(eqb(#{w_0}, 0), andb(eqb(#{w_1}, 10), eqb(#{w_2}, 10)))
"
Note that the argument to the boolean logic function is absent and the mac_t fields referenced in the ACSL definition of the logic function have. become "#{w_i}" - this malformed AltErgo (# is illegal in AltErgo) seems to originates from WP's QED module's pretty printer, whose find_var_env function returns these malformed names when it fails to find a given name in its environment.
### Steps To Reproduce :
tar -xvf framaBug.tar.gz
make wp
## Attachments
- [framaBug.tar.gz](/uploads/f07e549fb7296718c7ae0d86fb99b96e/framaBug.tar.gz)
- [frmaBug.tar.gz](/uploads/a43835306fcfcff1aef5bd28e09e0b4d/frmaBug.tar.gz)https://git.frama-c.com/pub/frama-c/-/issues/115dubious discharge of postcondition2021-02-22T14:00:51ZJens Gerlachdubious discharge of postconditionID0002390:
**This issue was created automatically from Mantis Issue 2390. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002390:
**This issue was created automatically from Mantis Issue 2390. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002390 | Frama-C | Plug-in > wp | public | 2018-07-24 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
Consider the following function
/*@
assigns \nothing;
ensures a == 0;
*/
void foo(int a)
{
a = 0;
}
The postcondition can of course not be verified because the assignment happens to a copy "a" and furthermore nothing is known about the value of "a" in the pre-state.
If I add, however, the admittedly weird looking precondition "requires \valid(&a);" as shown here
/*@
requires \valid(&a);
assigns \nothing;
ensures a == 0;
*/
void bar(int a)
{
a = 0;
}
then Qed discharges the postcondition.
I am not sure this a bug or rather caused by taking the address of a formal argument in the precondition
but in any case it would be nice if someone could have a look at it.
### Steps To Reproduce :
Call
frama-c -wp -wp-rte foo.c
on the attached file.
## Attachments
- [foo.c](/uploads/59eb64f1e1b8ca2563cbfa0bcbb63a83/foo.c)https://git.frama-c.com/pub/frama-c/-/issues/116crash2021-02-22T12:54:02Zmantis-gitlab-migrationcrashID0002409:
**This issue was created automatically from Mantis Issue 2409. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002409:
**This issue was created automatically from Mantis Issue 2409. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002409 | Frama-C | Plug-in > wp | public | 2018-11-13 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | hugo.gimbert | **Assigned To** | correnson | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | macosx | **OS** | mojave | **OS Version** | 10.14.1 |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
frama-c -wp somme.c
with somme.c containing
/*@
logic integer f(integer k) = k;
lemma sumint:
\forall int n;
n >= 0 ==> \sum(0,n,f) == n * (n+1) / 2;
*/
leads to crash
Trace below
### Additional Information :
[kernel] Parsing somme.c (with preprocessing)
[wp] Failure: Unbound logic variable 'f'
[kernel] Current source was: somme.c:4
The full backtrace is:
Raised at file "src/kernel_services/plugin_entry_points/log.ml" (inlined), line 531, characters 24-31
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 998, characters 12-50
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 524, characters 9-23
Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 527, characters 9-16
Called from file "src/plugins/wp/LogicSemantics.ml", line 205, characters 18-38
Called from file "src/plugins/wp/LogicSemantics.ml", line 238, characters 16-32
Called from file "src/plugins/wp/Warning.ml", line 146, characters 6-10
Called from file "src/plugins/wp/LogicSemantics.ml", line 920, characters 12-32
Called from file "src/plugins/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/plugins/wp/Context.ml", line 34, characters 35-46
Called from file "src/plugins/wp/LogicCompiler.ml" (inlined), line 435, characters 20-35
Called from file "src/plugins/wp/LogicSemantics.ml", line 124, characters 10-23
Called from file "list.ml", line 88, characters 20-23
Called from file "list.ml", line 88, characters 32-39
Called from file "list.ml", line 88, characters 32-39
Called from file "src/plugins/wp/LogicSemantics.ml", line 594, characters 23-52
Called from file "src/plugins/wp/Warning.ml", line 146, characters 6-10
Called from file "src/plugins/wp/LogicSemantics.ml", line 920, characters 12-32
Called from file "src/plugins/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/plugins/wp/Context.ml", line 34, characters 35-46
Called from file "src/plugins/wp/LogicCompiler.ml" (inlined), line 435, characters 20-35
Called from file "src/plugins/wp/LogicSemantics.ml", line 124, characters 10-23
Called from file "src/plugins/wp/LogicSemantics.ml", line 361, characters 16-35
Called from file "src/plugins/wp/Warning.ml", line 146, characters 6-10
Called from file "src/plugins/wp/LogicSemantics.ml", line 931, characters 12-42
Called from file "src/plugins/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/plugins/wp/Context.ml", line 34, characters 35-46
Called from file "src/plugins/wp/LogicCompiler.ml" (inlined), line 434, characters 28-51
Called from file "src/plugins/wp/LogicSemantics.ml", line 735, characters 39-62
Called from file "src/plugins/wp/Warning.ml", line 146, characters 6-10
Called from file "src/plugins/wp/LogicSemantics.ml", line 931, characters 12-42
Called from file "src/plugins/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/plugins/wp/Context.ml", line 34, characters 35-46
Called from file "src/plugins/wp/LogicCompiler.ml", line 399, characters 21-32
Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48
Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48
Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48
Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48
Called from file "src/plugins/wp/LogicCompiler.ml", line 485, characters 6-60
Called from file "src/plugins/wp/LogicCompiler.ml", line 741, characters 6-104
Called from file "src/plugins/wp/LogicCompiler.ml", line 758, characters 24-46
Called from file "src/plugins/wp/cfgWP.ml", line 1351, characters 31-42
Called from file "map.ml", line 295, characters 20-25
Called from file "src/plugins/wp/cfgWP.ml", line 1435, characters 19-59
Called from file "src/plugins/wp/Context.ml", line 70, characters 14-17
Re-raised at file "src/plugins/wp/Context.ml", line 71, characters 37-48
Called from file "src/plugins/wp/Context.ml" (inlined), line 73, characters 21-47
Called from file "src/plugins/wp/Model.ml" (inlined), line 127, characters 21-45
Called from file "src/plugins/wp/Model.ml" (inlined), line 129, characters 18-36
Called from file "src/plugins/wp/cfgWP.ml", line 1433, characters 14-202
Called from file "src/plugins/wp/Model.ml", line 120, characters 17-20
Re-raised at file "src/plugins/wp/Model.ml", line 125, characters 19-28
Called from file "src/plugins/wp/Model.ml" (inlined), line 126, characters 19-36
Called from file "src/plugins/wp/cfgWP.ml", line 1431, characters 10-1023
Called from file "src/plugins/wp/register.ml", line 689, characters 15-40
Called from file "src/libraries/stdlib/extlib.ml", line 301, characters 14-17
Re-raised at file "src/libraries/stdlib/extlib.ml", line 301, characters 41-48
Called from file "src/libraries/stdlib/extlib.ml", line 302, characters 2-12
Called from file "src/libraries/stdlib/extlib.ml", line 302, characters 2-12
Called from file "queue.ml", line 105, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 791, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 821, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 230, characters 4-8
Plug-in wp aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Chlorine-20180502.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
hugo-9:TP3 gimbert$ cat somme.c
/*@
logic integer f(integer k) = k;
lemma sumint:
\forall int n;
n >= 0 ==> \sum(0,n,f) == n * (n+1) / 2;
*/
## Attachments
- [somme.c](/uploads/5ef73e24f859da4da063d6d4e135ea99/somme.c)https://git.frama-c.com/pub/frama-c/-/issues/117contracts about memory mapped I/O through volatile memory locations2021-02-22T12:54:04Zmantis-gitlab-migrationcontracts about memory mapped I/O through volatile memory locationsID0002407:
**This issue was created automatically from Mantis Issue 2407. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002407:
**This issue was created automatically from Mantis Issue 2407. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002407 | Frama-C | Plug-in > wp | public | 2018-10-31 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jmaytac | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
We've attached a small example in which a state machine communicates a peripheral through a volatile variable , on line 6 of constants.h:
volatile uint32_t rxBuffer;
The state of the machine is held by a struct mac, declared on line 21 of mac.h:
struct mac {
mac_packet_t mac_packet;
MessageType latestMessage;
mac_bridge_t MAC_BRIDGE_A;
}
the mac_bridge_t represents the machine's memory mapped I/O interface, as declared on line 15 of mac_bridge.h:
struct mac_bridge
{
volatile uint32_t *cmd_rx_buffer;
}
on line 13 of main.c,
mac_t mac = the_mac();
mac becomes a pointer to singleton_mac instance of struct mac declared on line 8 of mac.c and returned by the function the_mac() defined on line 17 of mac.c. On line 14 of main.c,
mac->MAC_BRIDGE_A = theMacBridge();
mac's IO interface MAC_BRIDGE_A becomes the singletonMacBridgeA instance of struct mac_bridge returned by the function theMacBridge() defined on line 11 of mac.c
mac_bridge_t theMacBridge() {
singletonMacBridgeA.cmd_rx_buffer = &rxBuffer;
return &singletonMacBridgeA;
}
thus, mac has as MAC_BRIDGE_A singletonMacBridgeA whose cmd_rx_buffer is a reference to the volatile rxBuffer. The volatile rxBuffer reads and writes from ghost state as given on line 7 of constants.h:
//@ ghost uint32_t injectorAPBBuffer[4294967296];
//@ ghost uint32_t injectorAPBBufferCount=0;
/*@ ghost //@ requires buffer == &(rxBuffer);
@ uint32_t readsBuffer(volatile uint32_t *buffer) {
@ static uint32_t injectorAPBBufferCount = 0;
@ for (int i=0; i<4294967296; i++) {
@ injectorAPBBuffer[i%4294967296]=i%42949967296;
@ }
@ if (buffer == &(rxBuffer)) {
@ return injectorAPBBuffer[injectorAPBBufferCount++];
@ }
@ else
@ return 0;
@ }
@ */
//@ ghost uint32_t bufferAPBCollector[4294967296];
//@ ghost uint32_t bufferAPBCollectorCount = 0;
/*@ ghost //@ requires buffer == &(rxBuffer);
@ uint32_t writesBuffer(volatile uint32_t *buffer, uint32_t v) {
@ if (buffer == &(rxBuffer)){
@ return bufferAPBCollector[(bufferAPBCollectorCount++)%64] = v;
@ }
@ else {
@ return 0;
@ }
@ }
@*/
//@ volatile (rxBuffer) reads readsBuffer writes writesBuffer;
mac implements a transition system driven by an alphabet of labels obtained through calls to macbridge_get_packet, defined on line 3 of mac_bridge.c
mac_packet_t macbridge_get_packet(mac_bridge_t mac_bridge)
{
mac_packet_t received_packet={0};
received_packet.object_high=(uint8_t)(*(mac_bridge->cmd_rx_buffer));
return(received_packet);
}
when the given macbridge_t is the reference to the singletonMacBridgeA, we want this function to have as postcondition that the packet this function returns has the value found in the appropriate ghost state
/*@
behavior A:
assumes mac_bridge == &singletonMacBridgeA;
ensures \result.object_high == (uint8_t)injectorAPBBuffer[(injectorAPBBufferCount-1)%4294967296];
*/
mac_packet_t macbridge_get_packet(mac_bridge_t mac_bridge);
The resulting Alt-ergo doesn't seem to capture the post-condition.
(* ---------------------------------------------------------- *)
(* --- Post-condition (file mac_bridge.h, line 24) in 'macbridge_get_packet' --- *)
(* ---------------------------------------------------------- *)
goal macbridge_get_packet_post:
forall t : int farray.
forall t_1 : (addr,int) farray.
forall t_2 : (addr,addr) farray.
forall a : addr.
let a_1 = shiftfield_F7_mac_bridge_cmd_rx_buffer(a) : addr in
let a_2 = t_2[a_1] : addr in
let x = t_1[a_2] : int in
(region(a.base) <= 0) ->
framed(t_2) ->
linked(t) ->
valid_rd(t, a_1, 1) ->
is_uint32(x) ->
valid_rd(t, a_2, 1) ->
(x = to_uint8(x))
## Attachments
- [framaExample.tar.gz](/uploads/ab7c400254275ad87e4710a1a81cafe6/framaExample.tar.gz)https://git.frama-c.com/pub/frama-c/-/issues/118Mk_addr not defined in Memory.v (coqwp via why3ide)2021-02-22T12:54:05Zmantis-gitlab-migrationMk_addr not defined in Memory.v (coqwp via why3ide)ID0002414:
**This issue was created automatically from Mantis Issue 2414. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002414:
**This issue was created automatically from Mantis Issue 2414. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002414 | Frama-C | Plug-in > wp | public | 2018-12-07 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | visq | **Assigned To** | correnson | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Memory.Mk_addr is needed for Coq proofs but not in Memory.v (it *is* present in Memory.why).
As a consequence, Coq fails to compile the generated proof scripts for a null pointer check:
> Error: The reference Memory.Mk_addr was not found in the current environment.
### Additional Information :
Frama-c Argon 18.0
Coq 8.6
why3 0.88.3
### Steps To Reproduce :
cat <<EOF >id.c
/*@ requires \valid(p);
ensures *p == \old(*p);
*/
void id(int* p)
{
int tmp;
if (p == (int*)0) return;
tmp = *p;
*p = ~~tmp;
}
EOF
frama-c -wp -wp-rte -wp-split -wp-prover why3ide id.c
# Select Postcondition Line 2
# Coq
# Edit
# Replay
# => Error: The reference Memory.Mk_addr was not found in the current environment.https://git.frama-c.com/pub/frama-c/-/issues/121floating-point support is somwhat incomplete2021-02-22T12:56:27Zmantis-gitlab-migrationfloating-point support is somwhat incompleteID0002459:
**This issue was created automatically from Mantis Issue 2459. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002459:
**This issue was created automatically from Mantis Issue 2459. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002459 | Frama-C | Plug-in > wp | public | 2019-07-02 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | florian | **Assigned To** | correnson | **Resolution** | suspended |
| **Priority** | normal | **Severity** | block | **Reproducibility** | always |
| **Platform** | any | **OS** | any | **OS Version** | any |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi!
Maybe I am doing something fundamentally wrong, but I've tried some simple programs and I don't get anywhere. For example:
/*@ requires x >= 0.0f && x <= 100.0f;
*/
void float_fun(float x)
{
float y = x + 1.0f;
//@ assert y >= 1.0f;
}
I've had a look in share/frama-c/wp/why3/Cfloat.why and I'm not surprised nothing works, the axiomatisation is very incomplete, compared to the current stuff in why3. Could you please port to https://gitlab.inria.fr/why3/why3/blob/master/stdlib/ieee_float.mlw and then use a SMT solver by default that supports it natively (i.e. CVC4 or Z3)?
I know this is a bit of a drastic change, but as it stands WP is not overly useful for anyone trying to do anything with floats (e.g. control systems)...https://git.frama-c.com/pub/frama-c/-/issues/122malloc breaks reasoning about assigns2021-02-22T13:34:49Zmantis-gitlab-migrationmalloc breaks reasoning about assignsID0002455:
**This issue was created automatically from Mantis Issue 2455. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002455:
**This issue was created automatically from Mantis Issue 2455. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002455 | Frama-C | Plug-in > wp | public | 2019-06-17 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jwaksbaum | **Assigned To** | correnson | **Resolution** | suspended |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | i386 | **OS** | Darwin | **OS Version** | 18.6.0 |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
If a function contains a call to malloc, WP fails to verify its assigns clause.
This could be because malloc does assign to variables in order to track allocation state, but if so there should be a way of specifying that the function assigns to only the listed variables, as well as whatever malloc assigns to. Even duplicating the annotation on malloc will not verify, which includes assigns clauses for the malloc state variables.
### Steps To Reproduce :
# Verify a function with a call to malloc and assigns \nothing
frama-c -lib-entry -c11 -wp -wp-rte -wp-prover [...] example.c -wp-fct f
# Verify a function with the same contract as malloc, which only calls malloc
frama-c -lib-entry -c11 -wp -wp-rte -wp-prover [...] example.c wp-fct malloc_wrapper
## Attachments
- [example.c](/uploads/419009a078988ed9875d2ded26c9f430/example.c)https://git.frama-c.com/pub/frama-c/-/issues/124incomplete loading of saved state when using WP?2021-02-22T14:00:16ZJens Gerlachincomplete loading of saved state when using WP?ID0002290:
**This issue was created automatically from Mantis Issue 2290. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002290:
**This issue was created automatically from Mantis Issue 2290. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002290 | Frama-C | Plug-in > wp | public | 2017-03-09 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Linux/macOS | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
When I run the line
frama-c -save swap.sav -wp -wp-rte swap.c
on the attached line and then load the saved sate with
frama-c-gui -load swap.sav
I observe the following:
1.) a message in the Frama-C-GUI:"1 state in saved file ingnored. It is invalid in this Frama-C configuration."
2.) the GUI shows which proof obligations have been verified but the tab "WP Goals" does not show any information about which prover was successful
### Additional Information :
I am not sure whether this a problem of the kernel or of the WP plug-in.
## Attachments
- [swap.c](/uploads/68eb8d47535f4c84d136f65f15dec59a/swap.c)https://git.frama-c.com/pub/frama-c/-/issues/125Shape of VC depends on selection of properties2021-09-21T13:53:03ZJens GerlachShape of VC depends on selection of propertiesID0002404:
**This issue was created automatically from Mantis Issue 2404. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002404:
**This issue was created automatically from Mantis Issue 2404. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002404 | Frama-C | Plug-in > wp | public | 2018-10-08 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | sometimes |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
WP allows to select properties by using the option -wp-prop. I have noticed the following:
When selecting a property 'foo' by -wp-prop=foo, sometimes all VCs that belong to that property are verified.
However, when I wish to verify all properties, some VC's of the property 'foo' are not verified.
This might be caused by the fact that the the actual "shape" of a VC appears to depend on -wp-prop.
(I attach an example of the slight differences between a VC that belongs to a certain property "foo" depending on whether -wp-prop=foo is used or not.)
This of course defeats somehow the purpose of using -wp-prop and it would be a welcome feature
if the generation of a VC of a property 'foo' is not affected by "-wp-prop=foo".
### Additional Information :
Is this maybe a problem of Qed?
Also, if there are several ways to generate/simplify a VC, it would be nice if one chooses one that has a higher likelihood to be verified.
## Attachments
- [diff.txt](/uploads/14ff154d537bcec5e27f7f5946ba2bfd/diff.txt)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/126Prove of \false2021-04-15T06:50:23ZJens GerlachProve of \falseID0002427:
**This issue was created automatically from Mantis Issue 2427. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002427:
**This issue was created automatically from Mantis Issue 2427. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002427 | Frama-C | Plug-in > wp | public | 2019-02-16 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
When the attached program foo.c is analysed with the command line
frama-c -pp-annot -no-unicode -wp -wp-prover alt-ergo -wp-prover eprover foo.c
then the assertion "\false" is verified with "eprover" (2.2).
To me the axiomatics and the lemma look fine which would mean that it is a problem of "eprover".
However, I would like that an WP expert has a look at it before I contact the developer of "eprover".
Thanks in advance.
### Steps To Reproduce :
I am using Frama-C 18.0, Why3 0.88.3, alt-ergo 2.2.0, eprover 2.2.
## Attachments
- [foo.c](/uploads/96dbe2588b177df6328014404f4b189f/foo.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/151number of generated files in Frama-C 18 vs 19. beta(2)2021-02-22T12:54:59ZJens Gerlachnumber of generated files in Frama-C 18 vs 19. beta(2)ID0002453:
**This issue was created automatically from Mantis Issue 2453. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002453:
**This issue was created automatically from Mantis Issue 2453. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002453 | Frama-C | Plug-in > wp | public | 2019-06-14 | 2019-07-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | bobot | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C 19-Potassium |
### Description :
This entry references issue
https://github.com/Frama-C/Frama-C-snapshot/issues/21
in order to be able to easily add files.
### Steps To Reproduce :
Run the command
frama-c -pp-annot -no-unicode -wp -wp-rte -warn-unsigned-overflow -warn-unsigned-downcast -wp-model Typed+ref -wp-out rc.wp rc.c
on the attached files.
As mentioned in the github issue, both 18.0 and 19.beta(2) report 17 VC of which 5 are discharged by Qed and the remaining 12 are verified by Alt-Ergo.
However, Frama-C 18.0 generates 12 .mlw and .out files, respectively.
Frama-C 19 beta2, on the other hand, only generates 9 .mlw and .out files, respectively.
The latter behaviour confuses our internal evaluation scripts which report that only 9 of the remaining 12 proof obligations have been discharged by Alt-Ergo.
## Attachments
- [rc.c](/uploads/12c6518483a56dad661d3ee7feabf59b/rc.c)https://git.frama-c.com/pub/frama-c/-/issues/159Ambiguous path error using why32021-02-22T12:55:18Zmantis-gitlab-migrationAmbiguous path error using why3ID0002454:
**This issue was created automatically from Mantis Issue 2454. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002454:
**This issue was created automatically from Mantis Issue 2454. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002454 | Frama-C | Plug-in > wp | public | 2019-06-17 | 2019-06-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jwaksbaum | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | i386 | **OS** | Darwin | **OS Version** | 18.6.0 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Why3 errors on the generated goals produce by w3 on certain inputs with the following message:
Ambiguous path:
both /nix/store/nf4sbv0j6dc0grks7iplf9byv989mjg5-why3-0.88.3/share/why3/modules/Matrix.mlw
and /var/folders/2j/dbl_p0mj3rgd879z8nt7r4600000gp/T/wpdeac45.dir/typed/Matrix.why
### Steps To Reproduce :
Why3 errors on the generated goals produce by w3 on certain inputs with the following message:
Ambiguous path:
both /nix/store/nf4sbv0j6dc0grks7iplf9byv989mjg5-why3-0.88.3/share/why3/modules/Matrix.mlw
and /var/folders/2j/dbl_p0mj3rgd879z8nt7r4600000gp/T/wpdeac45.dir/typed/Matrix.why
## Attachments
- [example.c](/uploads/ba254a88318716a5e0665ff9fe46d1f4/example.c)https://git.frama-c.com/pub/frama-c/-/issues/168Division by zero doesn't increase the number of VC in console output2021-02-22T12:55:28Zmantis-gitlab-migrationDivision by zero doesn't increase the number of VC in console outputID0002428:
**This issue was created automatically from Mantis Issue 2428. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002428:
**This issue was created automatically from Mantis Issue 2428. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002428 | Frama-C | Plug-in > wp | public | 2019-02-17 | 2019-02-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Obvious division by zero doesn't increase the total number of proof obligations:
Test2:
<pre>
/*@ assigns \nothing;
*/
int test2(int a)
{
return a / 0;
}
</pre>
Frama-C:
<pre>
[kernel] Parsing test2.c (with preprocessing)
[rte] annotating function test2
[rte] test2.c:5:8: Warning: guaranteed RTE: assert division_by_zero: 0 ≢ 0;
[wp] 1 goal scheduled
[wp] Proved goals: 1 / 1
Qed: 1
</pre>
Proved goals line is the same as in the case without division:
Test1:
<pre>
/*@ assigns \nothing;
*/
int test1(int a)
{
return a;
}
</pre>
Frama-C output:
<pre>
[kernel] Parsing test1.c (with preprocessing)
[rte] annotating function test1
[wp] 1 goal scheduled
[wp] Proved goals: 1 / 1
Qed: 1
</pre>
From my point of view this is an incorrect behavior and the proved goals like should be 'Proved goals: 1 / 2' as in this case:
Test3:
<pre>
/*@ assigns \nothing;
*/
int test3(int a)
{
//@ assert 0 != 0;
return a / 0;
}
</pre>
Frama-C:
<pre>
[kernel] Parsing test3.c (with preprocessing)
[rte] annotating function test3
[rte] test3.c:6:8: Warning: guaranteed RTE: assert division_by_zero: 0 ≢ 0;
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_test3_assert : Unknown (109ms)
[wp] Proved goals: 1 / 2
Qed: 1
Alt-Ergo: 0 (unknown: 1)
</pre>
## Attachments
- [test2.c](/uploads/6a8a966174608d26a4e3aaca44d430f1/test2.c)https://git.frama-c.com/pub/frama-c/-/issues/169One \valid seems sufficient to write in a whole array.2021-02-22T12:55:31Zmantis-gitlab-migrationOne \valid seems sufficient to write in a whole array.ID0002426:
**This issue was created automatically from Mantis Issue 2426. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002426:
**This issue was created automatically from Mantis Issue 2426. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002426 | Frama-C | Plug-in > wp | public | 2019-02-12 | 2019-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | VincentPenelle | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Linux | **OS** | Linux Manjaro | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
I am on Chlorine version.
When I try to verify the following function with RTE guard enabled, WP succeeds. However, I think it should not, as only the first cell is specified to be valid, the rest is just specified to have valid read.
/*@ requires \valid(a);
@ requires \valid_read(a + (0 .. n-1));
@ requires 0 <= n <= INT_MAX;
*/
void foo(int *a, int n){
/*@ loop invariant 0 <= i <= n;
@ loop invariant \valid(a + (0 .. n-1));
*/
for (int i = 0; i<n;i++) a[i] = i;
}
Note: that works as well without any loop.
It doesn't work if you declare to pointers with different names, and declare one to be \valid and the other to be \valid_read (like in swap function for example).
It looks like the loop invariant \valid is simplified to true by Qed.
If that's normal, please explain me why.
Thanks,
--
Vincent Penelle.
### Steps To Reproduce :
Specify an array as being \valid_read, and one of its cells to be \valid.
Then, try to write in any cell.
Generate the RTE guards. WP should succeed to prove that the cells you're writing in are \valid.https://git.frama-c.com/pub/frama-c/-/issues/224`strlen` used from code makes it no longer possible to prove `assigns \nothing`.2021-02-22T12:56:40Zmantis-gitlab-migration`strlen` used from code makes it no longer possible to prove `assigns \nothing`.ID0002380:
**This issue was created automatically from Mantis Issue 2380. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002380:
**This issue was created automatically from Mantis Issue 2380. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002380 | Frama-C | Plug-in > wp | public | 2018-06-23 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | namin | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
`strlen` used from code makes it no longer possible to prove `assigns \nothing`. The definition in the Frama-C library has `@ assigns \result \from indirect:s[0..];`, but this should not prevent check?
### Steps To Reproduce :
$ cat bug.c
#include <string.h>
/*@
requires strlen(s)>=0 && \valid(s+(0..strlen(s)));
assigns \nothing;
*/
int len(char *s) {
return strlen(s);
}
$ frama-c -wp -wp-rte -wp-prover CVC4,alt-ergo bug.c
[kernel] Parsing bug.c (with preprocessing)
[rte] annotating function len
[wp] 5 goals scheduled
[wp] [Failed] Goal typed_len_assign_normal_part1
CVC4: Timeout (Qed:2ms) (10s)
Alt-Ergo: Unknown (Qed:2ms) (324ms)
[wp] [Failed] Goal typed_len_assign_exit
CVC4: Timeout (Qed:2ms) (10s)
Alt-Ergo: Unknown (Qed:2ms) (322ms)
[wp] Proved goals: 3 / 5
Qed: 2 (0.35ms-0.85ms-2ms)
Alt-Ergo: 1 (15ms) (20) (unknown: 2)
CVC4: 0 (interrupted: 2)https://git.frama-c.com/pub/frama-c/-/issues/225Some issues related to Frama-C 18.0 (beta) "Argon"2021-02-22T13:33:32ZJens GerlachSome issues related to Frama-C 18.0 (beta) "Argon"ID0002408:
**This issue was created automatically from Mantis Issue 2408. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002408:
**This issue was created automatically from Mantis Issue 2408. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002408 | Frama-C | Plug-in > wp | public | 2018-11-03 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C 18-Argon |
### Description :
This entry serves to link my GitHub issues on Argon (beta) to the BTS. The issues are
https://github.com/Frama-C/Frama-C-snapshot/issues/12
https://github.com/Frama-C/Frama-C-snapshot/issues/13
https://github.com/Frama-C/Frama-C-snapshot/issues/14https://git.frama-c.com/pub/frama-c/-/issues/241Newer releases of FramaC produce apparent WP plug-in bug2021-02-22T14:01:18Zmantis-gitlab-migrationNewer releases of FramaC produce apparent WP plug-in bugID0002403:
**This issue was created automatically from Mantis Issue 2403. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002403:
**This issue was created automatically from Mantis Issue 2403. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002403 | Frama-C | Plug-in > wp | public | 2018-10-01 | 2018-10-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jmaytac | **Assigned To** | correnson | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - |
### Description :
The attached code base is a small example in which a reactive program interacts with peripherals via memory mapped I/O through a constant address. While earlier releases of framaC (Phosphorous) was able to generate full and faithful altergo for our proofs, the new version produces syntactically malformed altergo for the following boolean logic function defined in our example's ACSL:
mac.h line 35:
logic boolean isAMessage(mac_t mac) = ((mac->mac_packet.object_high == 0x0A) && (mac->mac_\
packet.object_low == 0x0A) && (mac->mac_packet.payload_length == 0x00));
Whereas such boolean logic functions were correctly axiomatized in the older (Phosphorous) release, the current version is axiomatizing such a function as :
function L_isAMessage
() :
bool =
andb(eqb(#{w_0}, 0), andb(eqb(#{w_1}, 10), eqb(#{w_2}, 10)))
note that the argument to the logic function is absent, and the fields of hte mac_t referenced in the logic function are rendered as "#{w_i}", about which altergo then complains. These malformed altergo expressions seem to have been generated by the pretty printer's find_var function.
### Steps To Reproduce :
tar -xvf framaBug.tar.gz
make wp
## Attachments
- [framaBug.tar.gz](/uploads/54add4d4c38c4a03cb21e9dd404eef64/framaBug.tar.gz)
- [frmaBug.tar.gz](/uploads/fccae63bbfa3517b0d9bc45326a5f0e6/frmaBug.tar.gz)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/259Invalid sizeof(struct) calculation in Sulfur2021-02-22T12:57:43Zmantis-gitlab-migrationInvalid sizeof(struct) calculation in SulfurID0002344:
**This issue was created automatically from Mantis Issue 2344. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002344:
**This issue was created automatically from Mantis Issue 2344. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002344 | Frama-C | Plug-in > wp | public | 2018-01-19 | 2018-07-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | abustany | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Linux | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
FramaC version: Sulfur-20171101 (cannot select it in BTS because of #0002343)
With the following C code:
-------------------------------
#include <stdint.h>
#include <string.h>
typedef struct {
uint8_t a;
uint8_t b;
uint8_t c;
uint16_t d;
uint16_t e;
uint16_t f;
char g[4086];
uint16_t h;
} message_t;
/*@ requires \valid(msg);
@*/
void reset_message(message_t *msg) {
memset(msg, 0, sizeof(message_t));
}
-------------------------------
Running: frama-c -wp -wp-fct reset_message -wp-rte -wp-print err.c
produces the following unprovable goal:
-------------------------------
Assume {
(* Heap *)
Have: (region(msg_0.base) <= 0) /\ linked(Malloc_0) /\ sconst(Mchar_0).
(* Pre-condition *)
Have: valid_rw(Malloc_0, msg_0, 4093).
}
Prove: valid_rw(Malloc_0, shift_sint8(w, 0), 4098).
-------------------------------
Using the Typed+cast model doesn't help.
I'm not really sure how the size of the struct is computed (with regard to alignment or padding), but somehow two different parts of the code seem to disagree here.https://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/262Strange difference in generated Coq code between Chlorine and Sulfur2021-02-22T13:37:10ZJens GerlachStrange difference in generated Coq code between Chlorine and SulfurID0002374:
**This issue was created automatically from Mantis Issue 2374. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002374:
**This issue was created automatically from Mantis Issue 2374. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002374 | Frama-C | Plug-in > wp | public | 2018-05-09 | 2018-06-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | high | **Severity** | block | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
This report refers to the BETA-release of Chlorine and affects a couple of Coq-proofs in ACSL by Example:
The problem is like this: If the attached file 'foo.c' is processed with the command line
frama-c -wp -wp-prover coq -wp-out foo.wp foo.c
then it produces in foo.wp among other files the Coq file A_Count.v.
The only difference when using with Frama-C-Sulfur or Frama-C-Chlorine is the following:
diff A_Count.sulfur.v A_Count.chlorine.v
28,32c28,32
< Hypothesis Q_CountSectionHit: forall (i_2 i_1 i : Z),
< forall (t : farray addr Z), forall (a : addr), let x := (i_1%Z - 1%Z)%Z in
< (((t.[ (shift_sint32 a x) ]) = i_2)%Z) -> ((i < i_1)%Z) ->
< ((is_sint32 i_2%Z)) ->
< (((1 + ((L_Count t a i%Z x i_2%Z))) = ((L_Count t a i%Z i_1%Z i_2%Z)))%Z).
---
> Hypothesis Q_CountSectionHit: forall (i_1 i : Z), forall (t : farray addr Z),
> forall (a : addr), let x := (i_1%Z - 1%Z)%Z in
> let x_1 := (t.[ (shift_sint32 a x) ])%Z in ((i < i_1)%Z) ->
> ((is_sint32 x_1)) ->
> (((1 + ((L_Count t a i%Z x x_1))) = ((L_Count t a i%Z i_1%Z x_1)))%Z).
It looks like as if the argument 'v' of axiom 'CountSectionHit' has not been translated into Coq.
## Attachments
- [foo.c](/uploads/53423ef104c4f86e7469ef5bb783ec52/foo.c)
- [A_Count.sulfur.v](/uploads/774888275fb8101cef0293aaee7dafa5/A_Count.sulfur.v)
- [A_Count.chlorine.v](/uploads/878201905680422222e1b2e12a40293d/A_Count.chlorine.v)https://git.frama-c.com/pub/frama-c/-/issues/324statement contract apparently confuses parser2021-04-15T09:31:56ZJochen Burghardtstatement contract apparently confuses parserID0002301:
**This issue was created automatically from Mantis Issue 2301. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002301:
**This issue was created automatically from Mantis Issue 2301. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002301 | Frama-C | Plug-in > wp | public | 2017-05-11 | 2017-07-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Phosphorus-20170501-beta1 | **OS** | xubuntu 16.04.1 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp assigns.c" on the attached program produces a warning:
assigns.c:12:[wp] warning: Missing assigns clause (assigns 'everything' instead)
The warning is unjustified since the loop in line 12 does have a "loop assigns" clauses, and loops don't use (plain) "assigns" clauses.
If the trivial assertion in line 9 is activated, the warning disappears, and everything is proven.
If instead the braces in line 5 and 7 are removed, Frama-c reports a crash (text see "Additional Information").
### Additional Information :
Crash message:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing assigns.c (with preprocessing)
[wp] failure: Several assigns ?
[kernel] Current source was: assigns.c:2
The full backtrace is:
Raised at file "src/kernel_services/plugin_entry_points/log.ml", line 568, characters 30-31
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 15-16
Called from file "src/plugins/wp/wpStrategy.ml", line 470, characters 13-63
Called from file "src/plugins/wp/wpStrategy.ml", line 505, characters 8-34
Called from file "list.ml", line 73, characters 12-15
Called from file "src/plugins/wp/wpStrategy.ml", line 541, characters 2-34
Called from file "map.ml", line 168, characters 20-25
Called from file "map.ml", line 168, characters 10-18
Called from file "src/plugins/wp/wpAnnot.ml", line 1023, characters 2-39
Called from file "src/plugins/wp/wpAnnot.ml", line 1094, characters 15-41
Called from file "src/plugins/wp/wpAnnot.ml", line 1273, characters 14-39
Called from file "src/plugins/wp/wpAnnot.ml", line 1274, characters 9-22
Called from file "src/plugins/wp/wpAnnot.ml", line 1363, characters 2-47
Called from file "map.ml", line 168, 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 47-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 134, characters 6-20
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
Plug-in wp aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Phosphorus-20170501-beta1.
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
- [assigns.c](/uploads/f5df9089249e50094cfbca65b1a403f3/assigns.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/333false postcondition shouldn't be verified in default memory-model setting2021-04-15T09:30:17ZJochen Burghardtfalse postcondition shouldn't be verified in default memory-model settingID0002312:
**This issue was created automatically from Mantis Issue 2312. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002312:
**This issue was created automatically from Mantis Issue 2312. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002312 | Frama-C | Plug-in > wp | public | 2017-06-15 | 2017-06-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | Phosphorus-20170501-beta1 | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-rte memmodel_default.c" verifies all 11 proof obligations, while the assert clase in line 21 is obviously violated. The reason for Frama-C's behavior is that it assumes the "Hoare Variables mixed with Pointers" memory model as a default (in accordance with WP manual sect.3.4, p.45) without checking its preconditions, viz. the absence of any address-taking of a variable.
A novice user who doesn't yet know about the subtleties of memory models will assume after the above Frama-c run that the program is ok, as is has been formally verified. This may build up unjustified trust in the program, and discredit Frama-C (or even the whole field of formal methods) once the bug is detected at runtime, possibly causing severe damage.
I suggest to either
1. check the applicability of the "Hoare Variables mixed with Pointers" model (this should be easily achievable, if only the source code needs to be scanned for a unary "&"), or
2. use another, less restrictive, model as default.
## Attachments
- [memmodel_default.c](/uploads/05c89d93d3c5c3dde72d94f83901958d/memmodel_default.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/334poor errors message texts for Hoare memory model checks2021-09-21T13:21:18ZJochen Burghardtpoor errors message texts for Hoare memory model checksID0002311:
**This issue was created automatically from Mantis Issue 2311. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002311:
**This issue was created automatically from Mantis Issue 2311. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002311 | Frama-C | Plug-in > wp | public | 2017-06-15 | 2017-06-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | text | **Reproducibility** | sometimes |
| **Platform** | Phosphorus-20170501-beta1 | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-rte -wp-model Hoare memmodel_Hoare.c" on the attached program produces the output:
...
[rte] annotating function foo
memmodel_Hoare.c:5:[wp] warning: Can not load value in Empty model
memmodel_Hoare.c:5:[wp] warning: Can not load value in Empty model
memmodel_Hoare.c:8:[wp] warning: Can not load value in Empty model
memmodel_Hoare.c:8:[wp] warning: No validity
memmodel_Hoare.c:4:[wp] warning: Can not load value in Empty model
memmodel_Hoare.c:3:[wp] warning: No validity
[wp] 4 goals scheduled
...
The name of the memory model is "Hoare" on the command line and in the WP manual (Sect.3.2, p.44), but it is called "Empty" in the error message output.
Moreover, the message "No validity" should be expanded to be more understandable. As an additional convenience, Frama-C could mention in each message the variable it refers to ("x" resp. "*x") in all cases in the example).
## Attachments
- [memmodel_Hoare.c](/uploads/913f6495cac3874938af5d592e39d609/memmodel_Hoare.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/336naming the default behavior influences proven obligations2021-04-15T09:29:03ZJochen Burghardtnaming the default behavior influences proven obligationsID0002309:
**This issue was created automatically from Mantis Issue 2309. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002309:
**This issue was created automatically from Mantis Issue 2309. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002309 | Frama-C | Plug-in > wp | public | 2017-06-01 | 2017-06-01 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Phosphorus-20170501-beta1 | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp ilog2_beh.c -wp-prop ilog2 -wp-prover alt-ergo -wp-prover cvc4" on the attached program proves everything except (the lemmas and) loop invariant "a".
However, when lines 16,27,30,36,41 are uncommented, i.e. the default behavior is assigned an explicit name, everything except (the lemmas and) the loop variant is proven instead.
Naming vs. not naming a behavior shouldn't have such an influence.
## Attachments
- [ilog2_beh.c](/uploads/61d5de2e4e4cfecc8959933e484a3108/ilog2_beh.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/337suggest to check (loop) assigns clauses by data flow analysis2021-08-05T09:22:29ZJochen Burghardtsuggest to check (loop) assigns clauses by data flow analysisID0002308:
**This issue was created automatically from Mantis Issue 2308. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002308:
**This issue was created automatically from Mantis Issue 2308. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002308 | Frama-C | Plug-in > wp | public | 2017-06-01 | 2017-06-01 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | low | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | n/a | **OS** | n/a | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp ifft_assigns.c -wp-prop check -wp-prover cvc4" on the attached file proved \false in line 339, which was intentionally inserted as a consistency check at the file's end. The reason for the inconsistency turned out to be a missing variable in a loop assigns clause (commented out for demo purposes in line 237). The detailled argument doesn't matter here; nevertheless it is given in (*) below for convenience.
I guess it would be easy for Frama-C to perform some coarse data-flow analysis and issue a warning about "nu2" being modified in line 295, but missing in the "loop assigns" clauses for the loop in line 242-302. Such an analysis could ignore nontrivial aliases, dead code, and array subranges, thus making it straight-forward to implement.
The example shows the value of warnings that such an analysis is able to issue. Already in this tiny example, it is easy to lose overview (cf. the many experimental "asserts", most of which a probably unncessary, or even nonsensical), and any tool help that doesn't cost much additional computation time is appreciated.
As a further application, it could print suggestions for "assigns" clauses of loops and procedure contracts.
(*): In fact, property "a2" from line 214 implies "nu1!=65536", if the latter variable remained unchanged during the loop in line 242-302, then property "c2" in line 232 boild down to "nu1+l==nu", which is false after the loop since then the termination condition "nu<l" has to hold, and "nu1" is unsigned.
## Attachments
- [ifft_assigns.c](/uploads/c813b7d252cb81e38d9f4fe871139244/ifft_assigns.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/347type of float parameter changed unexpectedly to double2021-02-22T12:59:54Zmantis-gitlab-migrationtype of float parameter changed unexpectedly to doubleID0002283:
**This issue was created automatically from Mantis Issue 2283. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002283:
**This issue was created automatically from Mantis Issue 2283. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002283 | Frama-C | Plug-in > wp | public | 2017-02-24 | 2017-05-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | widc | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | high | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Ubuntu | **OS Version** | 16.04 LTS |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | Frama-C 15-Phosphorus |
### Description :
Current source was: sgn.c:4
The full backtrace is:
Raised at file "hashtbl.ml", line 328, characters 23-32
Called from file "src/libraries/project/state_topological.ml", line 62, characters 23-38
Frama-C aborted: internal error.
Your Frama-C version is Silicon-20161101.
From the floating_point.ml the following message is reported:
Could not parse floating point number "-0x1.0000000000000p0"
The code in the main pane shows:
float sgn(float u)
...
if ((double)u > 0.0) {
...
### Additional Information :
Quick solution would be appreciated.
### Steps To Reproduce :
C code of sgn.c :
/*@
ensures A: \result == 1.0 || \result == 0.0 || \result == -1.0 ;
*/
float sgn(float u)
{
float p; /* return value */
if (u > 0.0) {
p = 1.0;
} else if (u < 0.0) {
p = -1.0;
} else {
p = 0.0;
}
return p;
}
1. Run:
frama-c-gui sgn.c
2. Select the post-condition
3. In context menu - Prove property by WP
(When the three "float" strings in the above code are changed to "double", the tool works fine, no error is reported.)https://git.frama-c.com/pub/frama-c/-/issues/350"loop assigns" clause ignored in presence of "for"-prefixed clauses2021-04-15T09:27:13ZJochen Burghardt"loop assigns" clause ignored in presence of "for"-prefixed clausesID0002298:
**This issue was created automatically from Mantis Issue 2298. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002298:
**This issue was created automatically from Mantis Issue 2298. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002298 | Frama-C | Plug-in > wp | public | 2017-05-08 | 2017-05-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Phosphorus-20170501-beta1 | **OS** | xubuntu 16.04.1 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp beh.c" on the attached program fails to prove ensures clause "x01" and assertion "x10". When the two clauses prefixed by "for five" are removed from the loop invariant, everything is proven (except ensures clause "x02", which is about behavior "five").
Apparently, the two "for five" clauses (in fact, the first of them alone does) make Frama-c ignore the following "loop assigns x06" clause.
If the two "for five" clauses are moved below the "loop assigns x06" clause, an internal error is raised (output see "Additional information" below). For this reason, I set the Severity to "crash".
### Additional Information :
Frama-C's output for the internal error:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing beh.c (with preprocessing)
[wp] failure: At most one loop assigns can be associated to a behavior
[kernel] Current source was: beh.c:11
The full backtrace is:
Raised at file "src/kernel_services/plugin_entry_points/log.ml", line 568, characters 30-31
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 15-16
Called from file "src/plugins/wp/wpAnnot.ml", line 855, characters 14-43
Called from file "list.ml", line 84, characters 24-34
Called from file "hashtbl.ml", line 200, characters 23-35
Called from file "hashtbl.ml", line 204, characters 12-33
Called from file "src/kernel_services/ast_data/annotations.ml", line 499, characters 4-187
Called from file "src/plugins/wp/wpAnnot.ml", line 865, characters 4-46
Called from file "src/plugins/wp/wpAnnot.ml", line 1015, characters 36-62
Called from file "map.ml", line 168, characters 20-25
Called from file "map.ml", line 168, characters 10-18
Called from file "map.ml", line 168, characters 10-18
Called from file "src/plugins/wp/wpAnnot.ml", line 1023, characters 2-39
Called from file "src/plugins/wp/wpAnnot.ml", line 1094, characters 15-41
Called from file "src/plugins/wp/wpAnnot.ml", line 1273, characters 14-39
Called from file "src/plugins/wp/wpAnnot.ml", line 1274, characters 9-22
Called from file "src/plugins/wp/wpAnnot.ml", line 1363, characters 2-47
Called from file "map.ml", line 168, 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 47-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 134, characters 6-20
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
Plug-in wp aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Phosphorus-20170501-beta1.
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
- [beh.c](/uploads/76212e7a4f3bee138c94f155a5d71946/beh.c)
- [beh2.c](/uploads/649046670c48074897a180a4e2785cc5/beh2.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/351Some ACSL mathematical functions crash WP2021-04-15T09:25:54Zmantis-gitlab-migrationSome ACSL mathematical functions crash WPID0002299:
**This issue was created automatically from Mantis Issue 2299. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002299:
**This issue was created automatically from Mantis Issue 2299. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002299 | Frama-C | Plug-in > wp | public | 2017-05-10 | 2017-05-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | boyer | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | high | **Severity** | block | **Reproducibility** | always |
| **Platform** | VirtualBox (Host Win7) | **OS** | Ubuntu | **OS Version** | 16.04.2 |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Some of the mathematical functions enumerated in http://frama-c.com/download/acsl.pdf, p24 are not correctly supported by Frama-c. For instance, the keywords \pow, \cos and \sin are recognized at parsing and supported by EVA whereas an error is reported for WP (builtin functions are not defined) followed by an internal error.
### Additional Information :
Console message:
[kernel] Parsing .opam/4.04.0/share/frama-c/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing ex.c (with preprocessing)
[wp] Running WP plugin...
[wp] warning: Missing RTE guards
[wp] user error: Builtin \round_error(float32) not defined
[wp] failure: Logic '\round_error' undefined
==================================================================================
Crash report:
Current source was: :0
The full backtrace is:
Raised at file "hashtbl.ml", line 440, characters 17-32
Called from file "src/libraries/project/state_topological.ml", line 62, characters 23-38
Plug-in wp aborted: internal error.
Reverting to previous state.
[...]
### Steps To Reproduce :
Using Example 2.9, p25 from the ACSL manual:
/*@ requires \abs(\exact(x)) <= 0x1p-5;
@ requires \round_error(x) <= 0x1p-20;
@ ensures \abs(\exact(\result)-\cos(\exact(x))) <= 0x1p-24;
@ ensures \round_error(\result) <= \round_error(x) + 0x3p-24;
@*/
float cosine(float x) {
return 1.0f - x * x * 0.5f;
}
Then:
frama-c-gui -wp cosine.c
## Attachments
- [wp-bug.zip](/uploads/df0c5400fe8b77153075db0a5a303098/wp-bug.zip)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/352axiom about bounds of lsl result needed in the long run2021-04-15T09:23:47ZJochen Burghardtaxiom about bounds of lsl result needed in the long runID0002296:
**This issue was created automatically from Mantis Issue 2296. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002296:
**This issue was created automatically from Mantis Issue 2296. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002296 | Frama-C | Plug-in > wp | public | 2017-05-08 | 2017-05-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | Phosphorus-20170501-beta1 | **OS** | xubuntu 16.04.1 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp and.c" on the attached program fails to prove the assertion in line 5, although it should follow immediately from the assignment in line 4.
Looking at the generated mlw file shows that "k=to_uint16(k)" can't be proven (variable name taken from c source). Apparently, the range boundaries of m from the contract in line 2 aren't propagated to m<<1.
In the long run, when bit operations will be handled in a satisfactory way, this issue should be resolved, too; the attached program can be used as a regeression test for it.
## Attachments
- [and.c](/uploads/5606c50a1cbb03c84ebc7bed8173b379/and.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/353Frama-C gives succeeding lemma, rather than preceding lemmas, as hypothesis t...2021-04-15T09:23:06ZJochen BurghardtFrama-C gives succeeding lemma, rather than preceding lemmas, as hypothesis to e.g. Cvc4ID0002293:
**This issue was created automatically from Mantis Issue 2293. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002293:
**This issue was created automatically from Mantis Issue 2293. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002293 | Frama-C | Plug-in > wp | public | 2017-03-16 | 2017-03-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Silicon-20161101 | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
I ran "frama-c -wp -wp-prover cvc4 -wp-prover alt-ergo -wp-prop bar gcd.c" and observed the input file "lemma_bar_Alt-Ergo.mlw" and "why_4e8b6a_Axiomatic-T-Q_bar.smt2" to Alt-ergo and Cvc4, respectively.
The former file contains as assumptions the lemmas "bar1" and "divisor1" (side remark: note the reversed order, compared to the Acsl source), which is ok.
However, the latter file contains as assumption just lemma "X", which imho is wrong.
In any case, the assumption sets given to Alt-ergo and Cvc4 should agree.
The problem might be a remainder of issue #2237, which is meanwhile closed.
## Attachments
- [gcd.c](/uploads/c50eb3ebd539d7224a0819fa7b628728/gcd.c)
- [lemma_bar_Alt-Ergo.mlw](/uploads/910b6b80e9ad2fdab9b8b30e5d212fbe/lemma_bar_Alt-Ergo.mlw)
- [why_4e8b6a_Axiomatic-T-Q_bar.smt2](/uploads/9612614ae617a11e9e3fd903e99f9020/why_4e8b6a_Axiomatic-T-Q_bar.smt2)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/354signature axiom omitted in Coq and Alt-ergo translation2021-04-15T09:22:17ZJochen Burghardtsignature axiom omitted in Coq and Alt-ergo translationID0002292:
**This issue was created automatically from Mantis Issue 2292. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002292:
**This issue was created automatically from Mantis Issue 2292. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002292 | Frama-C | Plug-in > wp | public | 2017-03-13 | 2017-03-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Silicon-20161101 | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-prover cvc4 -wp-prover alt-ergo -wp-prover coq -wp-script wp0.script -wp-prop incAdd input_it.c" on the attached file generates an insufficient translation to Coq: There is a clause "Parameter L_add : S1__Iter -> Z -> S1__Iter." in file "lemma_incAdd_Coq.v", but no corresponding "Hypothesis Q_TL_add". Both clauses are needed to describe the signature of the Acsl logic function "add". The hypothesis "Q_TL_add" would be needed in the Coq proof (see out-commented lines in file "wp0.script"). For the Acsl function "inc", which is defined in a different "axiomatic" block, both signature description clauses (viz. "Parameter L_inc" and "Hypothesis Q_TL_inc") are contained in file "A_IterAxioms.v".
When considering the output to Alt-Ergo, viz. file "lemma_incAdd_Alt-Ergo.mlw", the same problem appears: there is a declaration "logic L_inc" in line 606, an "axiom Q_TL_inc" in line 610, a declaration "logic L_add" in line 632, but no corresponding "axiom Q_TL_add".
When considering the output to Why3, everything appears to be ok: in file "A_addAxioms.why", both "function l_add" and "axiom Q_TL_add" is found, and in file "A_IterAxioms.why", both "function l_inc" and "axiom Q_TL_inc" is found.
## Attachments
- [input_it.c](/uploads/88e27e089e806bc7a33ec394a5a03895/input_it.c)
- [wp0.script](/uploads/072ee52979588420d483d6c91cde6dae/wp0.script)
- [lemma_incAdd_Coq.v](/uploads/9e66d6cd32f3c22f20024c64a684ac91/lemma_incAdd_Coq.v)
- [A_IterAxioms.v](/uploads/28dcafa275d9a551a511ca58577daba7/A_IterAxioms.v)
- [lemma_incAdd_Alt-Ergo.mlw](/uploads/284bc586b8a9569b8bd931c022fe93d5/lemma_incAdd_Alt-Ergo.mlw)
- [A_addAxioms.why](/uploads/5604dca431021ff929e54115829f47aa/A_addAxioms.why)
- [A_IterAxioms.why](/uploads/74423afd66c8b9493003003934166c7b/A_IterAxioms.why)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/356Axiomatic is recompiled when using severalprocesses2021-02-22T13:00:08ZJens GerlachAxiomatic is recompiled when using severalprocessesID0001685:
**This issue was created automatically from Mantis Issue 1685. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001685:
**This issue was created automatically from Mantis Issue 1685. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001685 | Frama-C | Plug-in > wp | public | 2014-03-12 | 2017-03-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
When verifying with alt-ergo and coq the file Axiomatic seems to be compiled again and again.
As far as I understood, alt-ergo seems to kill the coq process.
### Steps To Reproduce :
In fact, I noticed this problem in Neon.https://git.frama-c.com/pub/frama-c/-/issues/359Provide an option to run Coq from Frama-C2021-02-22T13:00:10ZJens GerlachProvide an option to run Coq from Frama-CID0001686:
**This issue was created automatically from Mantis Issue 1686. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001686:
**This issue was created automatically from Mantis Issue 1686. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001686 | Frama-C | Plug-in > wp | public | 2014-03-12 | 2017-03-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
When proving external Coq-lemma for WP it might be interesting to run Coq from Frama-C, e.g.,
frama-c -wp-coq Foo.vhttps://git.frama-c.com/pub/frama-c/-/issues/360suggestion: translate axioms and implication premises in forward order to coq2021-04-15T09:12:22ZJochen Burghardtsuggestion: translate axioms and implication premises in forward order to coqID0002291:
**This issue was created automatically from Mantis Issue 2291. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002291:
**This issue was created automatically from Mantis Issue 2291. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002291 | Frama-C | Plug-in > wp | public | 2017-03-13 | 2017-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Silicon-20161101 | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-prover coq -wp-out wp-out coqtest.c" on the attached file generates two Coq files, viz. "A_eqAxioms.v" and "lemma_goal_Coq.v".
The former contains the translation of "axiomatic eqAxioms", with the axioms ("eqRefl" and "eqTrns") appearing in the same order as in the source. The file "lemma_goal_Coq.v" contains the translation of "axiomatic incAxioms", however, with the axioms ("incLf" and "incRg") appearing in reverse order, compared to the source.
A similar issue concerns the translation of the body formula of axiom "eqTrns", where the first and second premise, viz. "eq(x,y)" and "eq(y,z)" in the source, appear in reverse order in the Coq translation.
(As a side remark: names of locally bound variables could be translated such that a target name closely resembles its source name; for example the source name could appear as a prefix of the target name.)
While probably easy to implement, these suggestions would considerably lower the overall complexity of the user's task.
## Attachments
- [coqtest.c](/uploads/74070de0221ca10812d16c76f7136c21/coqtest.c)
- [A_eqAxioms.v](/uploads/069306903f4c37b11f8f97b4a7df853c/A_eqAxioms.v)
- [lemma_goal_Coq.v](/uploads/231b70565ab0de2adf794e9662aae91e/lemma_goal_Coq.v)Loïc CorrensonLoïc Corrensonhttps://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/367lemma tacitly omitted from prover assumptions2021-08-05T09:00:11ZJochen Burghardtlemma tacitly omitted from prover assumptionsID0002286:
**This issue was created automatically from Mantis Issue 2286. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002286:
**This issue was created automatically from Mantis Issue 2286. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002286 | Frama-C | Plug-in > wp | public | 2017-02-27 | 2017-02-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Silicon-20161101 | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-rte -wp-prop=addIncAdd -wp-prover z3 bug1.c" on the attached file verifies the given goal "addIncAdd" in 40ms. However, when the closing brace is moved from line 35 up to line 30, no proof is found in 10s.
A "diff -r" on the wp-out directories shows that the translation of lemma "incAdd" is put into file "A_addAxioms.why" in the former, but into "Axiomatic2.why" in the latter case.
Intercepting the input if "z3" shows that only in the former case the translation is included in the input of "z3"; in the latter case it is missing.
I couldn't find the reason for just omitting "incAdd": exchanging lemmas "incAdd" and "addAdd" in the C source and comparing the "z3" inputs again shows that still "incAdd" is omitted; so the reason could be in it's name of form, but not in it place in source.
## Attachments
- [bug1.c](/uploads/506733bc64b39e2ab7b3c2d585f33515/bug1.c)
- [why_495d09_Axiomatic2-T-Q_addIncAdd.smt2](/uploads/1b12fd854a0d7471daf0f12f795dc5b4/why_495d09_Axiomatic2-T-Q_addIncAdd.smt2)
- [why_767c25_Axiomatic2-T-Q_addIncAdd.smt2](/uploads/8fbe26071875fc21dea8cfbef1aa6f8d/why_767c25_Axiomatic2-T-Q_addIncAdd.smt2)
- [why_54d12d_Axiomatic2-T-Q_addIncAdd.smt2](/uploads/d92a6c680802a47e1e35e8cd3c5810ad/why_54d12d_Axiomatic2-T-Q_addIncAdd.smt2)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/368applicability of Coq proof script depends on order of include files2021-04-15T08:02:31ZJochen Burghardtapplicability of Coq proof script depends on order of include filesID0002282:
**This issue was created automatically from Mantis Issue 2282. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002282:
**This issue was created automatically from Mantis Issue 2282. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002282 | Frama-C | Plug-in > wp | public | 2017-02-16 | 2017-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Silicon-20161101 | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
We run "frama-c -wp -wp-script wp0.script -wp-model Typed+ref -wp-prop HeapMaximum -wp-prover coq make_heap_cpp.c" on the attached files. In the current form, the Coq proof script "wp0.script" works fine and proved the lemma "HeapMaximum" from file "make_heap_cpp.c".
However, when that lemma is moved after the "axiomatic Count", which is completely unrelated, the same command doesn't work any longer. Using "-wp-out" shows that both versions differ in the location where lemma "HeapBounds" is available in Coq; this make it necessary to change the names used in the proof.
The problem originated from lemma "HeapMaximum" being used for the verification of two different function contracts. For software engineering reasons, the order of #include files was different (since different files were preferred to be included in the ".c", rather than already in the ".h" file). This resulted in "lemma HeapMaximum" appearing before and after an "axiomatic", making "wp0.script" work and not work, respectively.
## Attachments
- [make_heap_cpp.c](/uploads/256c2042ed0e2b08fc7901c42cdcbb49/make_heap_cpp.c)
- [wp0.script](/uploads/7277fc9a7ed0386527de3694d96817e5/wp0.script)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/369Frama-C sleeps too much when discharging trivial goals2021-04-15T09:08:16Zmantis-gitlab-migrationFrama-C sleeps too much when discharging trivial goalsID0002280:
**This issue was created automatically from Mantis Issue 2280. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002280:
**This issue was created automatically from Mantis Issue 2280. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002280 | Frama-C | Plug-in > wp | public | 2017-02-13 | 2017-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pkhuong | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | Linux/x86_64 | **OS** | Linux | **OS Version** | 4.9.0-1-amd64 #1 |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
I have a largish C functions that generates ~70K goals (that I'm refactoring away). Verification with WP and RTE assertions succeeds, but takes ~14 minutes of real time. strace shows the majority of that time is spent executing *no syscall* (i.e., not calling external solvers) except printing the progress on stderr, getrusage, and nanosleeping for half a second. I LD_PRELOADed a shared object to turn usleep into a no-op, and that improved the runtime from 14 minutes to 3 minutes.
Could Frama-C sleep less when Qed does all the work?
### Steps To Reproduce :
frama-c slow_qed.c -cpp-gnu-like -no-asm-contracts -constfold -machdep x86_64 -implicit-function-declaration error -wp -wp-rte -wp-extensional -wp-split -wp-init-const -wp-prop="-trustme,-freeable,-@assigns,-@lemma,-@variant" -wp-prover=alt-ergo,Z3:4.5.0
## Attachments
- [slow_qed.c](/uploads/df95dd235b294d5f24c6ca57181db9d4/slow_qed.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/371translation to why3 of int* argument to logic function2021-04-15T08:10:47ZJochen Burghardttranslation to why3 of int* argument to logic functionID0002275:
**This issue was created automatically from Mantis Issue 2275. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002275:
**This issue was created automatically from Mantis Issue 2275. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002275 | Frama-C | Plug-in > wp | public | 2017-02-02 | 2017-02-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Silicon-20161101 | **OS** | xubuntu 16.04.1 LTS | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-prover eprover foo.c" proves lemma "foo" in line 7, although it essentially says that no objects of type "int*" exist at all.
The problem disappears if either
(1) the result type "int" of "deref" is changed to "integer" in line 3,
(2) "deref" is inlined at line 5,
(3) "large" is inlined at line 7, or
(4) "large(s) && !large(s)" is simplified to "\false" in line 7.
Using option "-wp-out", and comparing the files "Axiomatic.why" before and after change (1), see attached files "Axiomatic_int.why" and "Axiomatic_integer.why", reveals that the former has an "axiom Q_TL_deref" while the latter does not. This axiom essentially says that any value fetched from an integer array (i.e. a "map addr int" in why3 language) is already an int (i.e. satisfies "is_sint32" in why3 language), which imho is wrong.
When using "-wp alt-ergo" instead of "-wp eprover", the generated mlw files before and after change (1) literally agree, see attached file "lemma_foo_Alt-Ergo_int.mlw" and "lemma_foo_Alt-Ergo_integer.mlw"; they contain no occurrence of "deref" or "large".
The input given to eprover has been intercepted and boiled down as far as possible, resulting in file "foo_eprover_input.p" which is attached for convenience. Its axiom "q_TL_deref" in line 18 is a boiled-down translation of axiom "Q_TL_deref" from the why3 file, and is wrong as argued above.
## Attachments
- [foo.c](/uploads/820f364a77e732e708ee0a21ae3d0123/foo.c)
- [Axiomatic_int.why](/uploads/10f847d1cf681d6ecde0ea21bab12d96/Axiomatic_int.why)
- [Axiomatic_integer.why](/uploads/3493da1d13894db1a171428f9e5c269e/Axiomatic_integer.why)
- [lemma_foo_Alt-Ergo_int.mlw](/uploads/ffc94494f9b1a25f6bc9ff99c712ec1e/lemma_foo_Alt-Ergo_int.mlw)
- [lemma_foo_Alt-Ergo_integer.mlw](/uploads/ee7e41ba4da81b0485dc5e5cc5d53a89/lemma_foo_Alt-Ergo_integer.mlw)
- [foo_eprover_input.p](/uploads/c00d2b593bcbd384b5bc9781d696e9b7/foo_eprover_input.p)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/384coq 8.5: cannot find Memory.v2021-02-22T13:00:50ZJens Gerlachcoq 8.5: cannot find Memory.vID0002208:
**This issue was created automatically from Mantis Issue 2208. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002208:
**This issue was created automatically from Mantis Issue 2208. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002208 | Frama-C | Plug-in > wp | public | 2016-02-11 | 2017-01-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | - |
### Description :
After updating my Frama-C installation through opam to coq.8.5 and why3.0.86.3 I observe the following error. When compiling the attached file with
coqc -R /Users/jens/.opam/system/share/frama-c/wp/coqwp -as "" WP_basics.v
I receive the following error message:
File "./WP_basics.v", line 3, characters 15-21:
Error: Unable to locate library Memory.
With coq.8.4.6 and earlier I did not observe this error.
### Additional Information :
The path '/Users/jens/.opam/system/share/frama-c' points to my Frama-C share.
ls -l /Users/jens/.opam/system/share/frama-c/wp/coqwp/Memory.v
produces
-rw-r--r-- 1 jens staff 10160 11 Feb 10:38 /Users/jens/.opam/system/share/frama-c/wp/coqwp/Memory.v
## Attachments
- [WP_basics.v](/uploads/e9bbf929a84471fcc0ca1d0a5755739b/WP_basics.v)https://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/387Why3 warning2021-04-15T09:00:01ZJens GerlachWhy3 warningID0002263:
**This issue was created automatically from Mantis Issue 2263. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002263:
**This issue was created automatically from Mantis Issue 2263. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002263 | Frama-C | Plug-in > wp | public | 2016-12-16 | 2016-12-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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 :
When running WP I observe the following warning
[Config] reading extra configuration file /Users/jens/.opam/4.04.0/share/frama-c/wp/why3/why3.conf
File "/Users/jens/.opam/4.04.0/share/why3/drivers/smt-libv2.drv", line 34, characters 7-14:
Library file not found: int
The problem occurs both under Linux and macOS.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/388more prover processes run than expected2021-04-15T08:59:30ZJens Gerlachmore prover processes run than expectedID0002262:
**This issue was created automatically from Mantis Issue 2262. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002262:
**This issue was created automatically from Mantis Issue 2262. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002262 | Frama-C | Plug-in > wp | public | 2016-12-15 | 2016-12-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | sometimes |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
When I start WP with '-wp-par 4' (for example) I often observe that more than 4 prover processes are actually running.
### Additional Information :
I am not sure this is related but:
It happens from time to time that a proof obligations that is verified with '-wp-par 1' and given timeout T
is not verified when using a greater number of processes and the same timeout T.
### Steps To Reproduce :
run WP on example with a sufficiently large number of proof obligations that require more than one theorem prover
## Attachments
- ![screen-shot](/uploads/64bc6ecf07003613b00fa43be854d6b3/screen-shot.png)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/394Frama-C is unsound when employing both alt-ergo and cvc42021-02-22T13:01:06ZJochen BurghardtFrama-C is unsound when employing both alt-ergo and cvc4ID0002237:
**This issue was created automatically from Mantis Issue 2237. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002237:
**This issue was created automatically from Mantis Issue 2237. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002237 | Frama-C | Plug-in > wp | public | 2016-06-30 | 2016-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | high | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | xubuntu |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-out out -wp-prover alt-ergo -wp-prover cvc4 bug.c" on the attached file "bug.c" proves both lemmas, although they are both obviously false. A look at file "lemma_Two_Alt-Ergo.mlw" shows that Alt-ergo proved in fact One==>Two, while a look at file "Axiomatic.why" indicates that cvc4 proved in fact Two==>One.
Apparently, the order of lemmas is reversed when piping through "why" - the output generated for coq amounts to "prove One" and "prove One==>Two", similar to that for Alt-ergo.
The problem disappeared when the type of the bound variable "x" was changed to "integer".
## Attachments
- [bug.c](/uploads/4c15388a22c29202e6cb9736f3dc73c9/bug.c)
- [lemma_Two_Alt-Ergo.mlw](/uploads/f03a7de730f37671825be7aed7c67b57/lemma_Two_Alt-Ergo.mlw)
- [Axiomatic.why](/uploads/1dcfeb3bf5a2935354dd3cae6d5c5e0a/Axiomatic.why)
- [0001-WP-Fix-definition-order.patch](/uploads/58c12a1488d50b4d416869447762e3e4/0001-WP-Fix-definition-order.patch)https://git.frama-c.com/pub/frama-c/-/issues/397Switch statements seem to be unsound2021-02-22T13:01:13Zmantis-gitlab-migrationSwitch statements seem to be unsoundID0002246:
**This issue was created automatically from Mantis Issue 2246. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002246:
**This issue was created automatically from Mantis Issue 2246. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002246 | Frama-C | Plug-in > wp | public | 2016-08-19 | 2016-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ghulette | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | Linux | **OS Version** | Ubuntu 16.04 |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
// Run the following to see the problem:
// $ frama-c -wp -wp-rte bad.c
//
// Frama-C does not detect the error in the ensures condition. You
// can cause WP to report the error by commenting out the case 0 line,
// or by passing the -simplify-cfg option. Maybe a problem with
// switch statements?
int x;
/*@
requires x != 1;
assigns x;
ensures x != 1;
*/
void bad (int e) {
switch (e) {
case 0: break;
case 1: x = 1; break;
}
}
### Additional Information :
$ frama-c --version
Aluminium-20160501
### Steps To Reproduce :
See comments in description.
## Attachments
- [bad.c](/uploads/c873fd1a6a052a79d2354129467bc6fe/bad.c)https://git.frama-c.com/pub/frama-c/-/issues/398"Builtin already registered" after Reparse2021-02-22T13:37:10Zmantis-gitlab-migration"Builtin already registered" after ReparseID0002242:
**This issue was created automatically from Mantis Issue 2242. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002242:
**This issue was created automatically from Mantis Issue 2242. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002242 | Frama-C | Plug-in > wp | public | 2016-07-30 | 2016-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | khar | **Assigned To** | bobot | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | lubuntu | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
When using frama-c-gui to analyze code that uses arrays or pointers to structs, after a Reparse, the GUI fails to perform further analysis.
### Additional Information :
Step 2 (selecting the function "Foo" rather than the file "repro.c") is needed to work around a possibly unrelated bug where the source viewer doesn't update properly after a Reparse. To reproduce that bug, simply click "repro.c" instead of "Foo" in step 2.
### Steps To Reproduce :
$ cat repro.c:
//@ ensures foo[1] == 1;
void Foo(int* foo) {
foo[1] = 1;
}
$ frama-c-gui repro.c
1. Expand "repro.c" on the file panel.
2. Click "Foo" on the file panel.
3. Right-click the "ensures" annotation in the source panel.
4. Click "Prove property by WP".
5. On the toolbar, click the "Reparse source files, and replay analyses" button.
6. Click "repro.c" on the file panel.
7. Right-click the "ensures" annotation in the source panel.
8. Click "Prove property by WP".
Results: an error dialog with the following text:
Current source was: repro.c:2
The full backtrace is:
Raised at file "hashtbl.ml", line 328, characters 23-32
Called from file "src/libraries/project/state_topological.ml", line 62, characters 23-38
Unexpected error (Failure("Builtin already registered for 'shift_sint32'")).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Aluminium-20160501.
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
- [repro.c](/uploads/5cc283fba4536bd3c0702a8ca68141b5/repro.c)https://git.frama-c.com/pub/frama-c/-/issues/403workaround for coq-8.5.1 issue?2021-02-22T13:01:28ZJochen Burghardtworkaround for coq-8.5.1 issue?ID0002233:
**This issue was created automatically from Mantis Issue 2233. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002233:
**This issue was created automatically from Mantis Issue 2233. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002233 | Frama-C | Plug-in > wp | public | 2016-06-16 | 2016-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | none | **Severity** | feature | **Reproducibility** | always |
| **Platform** | Aluminium-20160501 | **OS** | xubuntu16.04 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
We ran the command
frama-c-gui -cpp-extra-args='-I.' -pp-annot -no-unicode -wp -wp-rte -wp-script wp0.script -wp-model Typed+ref -wp-prop AdjacentDifferenceInverse -wp-coq-timeout 5 -wp-prover coq -wp-par 1 -wp-out adjacent_difference_inverse.wp adi.c
on the attached file "adi.c", using the attached Coq-script "wp0.script".
The goal isn't proven, and when manually starting the Coq Ide, it complains:
Error: The reference Q_UnchangedSection was not found in the current
environment.
However, the lemma "UnchangedSection" is present in lines 28-33 of file "adi.c", and a "Hypothesis Q_UnchangedSection" is present in lines 33-36 of the generated file "adjacent_difference_inverse.wp/typed_ref/Axiomatic.v", which is included in line 33 of file "adjacent_difference_inverse.wp/typed_ref/lemma_AdjacentDifferenceInverse_Coq.v" (i.e. of the file shown in the Coq Ide).
For these reasons, we believe that the behavior is a Coq-8.5.1 problem, not a Frama-c problem. Moreover, the same files cause no problems when Coq-8.5.1 is replaced by Coq-8.4.6.
Nevertheless, in an e-mail to Jens, Loic encouraged us to report the issue here, since Frama-C might provide a workaround for it.
## Attachments
- [adi.c](/uploads/c4c8150d300c94e05ae4078a54bb0388/adi.c)
- [wp0.script](/uploads/7a7bb805cc9c8332faccefd8ebe42e5d/wp0.script)
- [Axiomatic.v](/uploads/9ab08c5dc84284dc5f8412c7ddc95f09/Axiomatic.v)
- [lemma_AdjacentDifferenceInverse_Coq.v](/uploads/d61593407465c9df0f749dc04240e6ea/lemma_AdjacentDifferenceInverse_Coq.v)
- [adi.script](/uploads/9ab0f4bd54640d060c2292833e1bcd01/adi.script)https://git.frama-c.com/pub/frama-c/-/issues/405error in Coq file generation2021-04-15T08:59:05ZAlain Giorgettierror in Coq file generationID0002260:
**This issue was created automatically from Mantis Issue 2260. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002260:
**This issue was created automatically from Mantis Issue 2260. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002260 | Frama-C | Plug-in > wp | public | 2016-12-03 | 2016-12-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | giorgetti | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
When an ACSL axiomatic in a C file main.c contains a type declaration, say
type t;
the command
frama-c .. -wp main.c -wp-prover coqide ..
generates a wrong line
Parameter fct : Type.
in the file typed_fct/A_coq_.v.
### Additional Information :
Noticed during a meeting with L. CorrensonLoïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/409Nested scopes may cause issues with the validity of created pointers2021-04-15T08:57:59Zmantis-gitlab-migrationNested scopes may cause issues with the validity of created pointersID0002245:
**This issue was created automatically from Mantis Issue 2245. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002245:
**This issue was created automatically from Mantis Issue 2245. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002245 | Frama-C | Plug-in > wp | public | 2016-08-17 | 2016-08-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jrobbins | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Upon entering a nested scope (caused by conditional blocks, or even just wrapping parts of code in {}), pointers once known as valid may become unknown in validity. This only seems to occur when more than 1 pointer is being reasoned about in the scope.
### Additional Information :
This bug occurs on both Sodium in Cygwin and Aluminum on Linux.
### Steps To Reproduce :
== Program bug.c:
/*@
ensures \valid(\result);
*/
int* foo();
void main() {
int* x = foo();
{
int y;
//@ assert \valid(x);
//@ assert \valid(&y);
}
}
== Command to run:
frama-c bug.c -wp
== Output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing bug.c (with preprocessing)
bug.c:6:[kernel] warning: No code nor implicit assigns clause for function foo, generating default assigns from the prototype
[wp] warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_main_assert : Unknown (51ms)
[wp] Proved goals: 1 / 2
Qed: 1
Alt-Ergo: 0 (unknown: 1)
== Expected output:
Both assertions to pass, since x is ensures to be valid, and the & operator always returns a valid pointer.
== Real output:
The pointer we ensure to be valid could not be proven to be valid.
Moving the definition of y to the outer scope fixes this issue, as well as moving the definition of x inside.
## Attachments
- [bug.c](/uploads/cfc99feea8974ba3cb5097bed4bfb3d3/bug.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/410Logic with read clauses can have their values invalidated by writes to separa...2021-08-05T09:15:39Zmantis-gitlab-migrationLogic with read clauses can have their values invalidated by writes to separated memory locationsID0002244:
**This issue was created automatically from Mantis Issue 2244. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002244:
**This issue was created automatically from Mantis Issue 2244. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002244 | Frama-C | Plug-in > wp | public | 2016-08-08 | 2016-08-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jrobbins | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
In some cases, axiomatic logic using reads clauses can be true for a certain memory location, and then become unknown once an unrelated memory location is assigned to. You can even prove the memory locations as separate, but it does not fix the issue.
### Additional Information :
This bug is present on both Frama-C versions Sodium and Aluminum.
### Steps To Reproduce :
== File bug.c:
/*@
axiomatic Axiomatic {
logic boolean property_of_buffer(char *buffer) reads *buffer;
}
*/
/*@
assigns *buffer;
ensures property_of_buffer(buffer);
*/
void foo(char *buffer);
/*@
requires property_of_buffer(buffer);
assigns *buffer;
ensures property_of_buffer(buffer);
*/
int bar(char *buffer);
char buf1[1];
char buf2[1];
void main() {
foo(buf1);
bar(buf1);
foo(buf2);
bar(buf1);
}
== Command to run:
frama-c -wp bug.c
== Output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing bug.c (with preprocessing)
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Qed] Goal typed_main_call_bar_pre : Valid
[wp] [alt-ergo] Goal typed_main_call_bar_pre_2 : Unknown (562ms)
[wp] Proved goals: 1 / 2
Qed: 1
alt-ergo: 0 (unknown: 1)
== Expected behavior: For typed_main_call_bar_pre_2 to prove valid.
## Attachments
- [bug.c](/uploads/40ef28c81962575b7520fa0642241586/bug.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/413Implicit casting from integer to real causes failure in WP proof generation2021-04-15T06:54:30Zmantis-gitlab-migrationImplicit casting from integer to real causes failure in WP proof generationID0002241:
**This issue was created automatically from Mantis Issue 2241. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002241:
**This issue was created automatically from Mantis Issue 2241. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002241 | Frama-C | Plug-in > wp | public | 2016-07-29 | 2016-07-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jrobbins | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
ACSL defines the integer type as a subset of the real type. Therefore, it states, implicit casting from integers to reals is allowed, because one is the subset of another. However, when this is done in practice, the WP plugin will generate goals that provers cannot parse, giving a type error.
### Additional Information :
This is confirmed to occur with the alt-ergo and why3 provers.
Tested on both Frama-C Sodium and Aluminum. Sodium produces slightly different errors than Aluminum, but both produce errors.
### Steps To Reproduce :
== Input file (bug.c):
/*@
axiomatic Bug {
logic integer ibug;
logic real rbug = ibug;
}
*/
/*@
requires i == rbug;
*/
void foo(int i);
void main() {
foo(42);
}
== Command to reproduce
frama-c -wp bug.c
== Output
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing bug.c (with preprocessing)
bug.c:13:[kernel] warning: No code nor implicit assigns clause for function foo, generating default assigns from the prototype
[wp] warning: Missing RTE guards
[wp] 1 goal scheduled
/tmp/wp714796.dir/typed/A_Bug.ergo:7:[wp] user error: Alt-Ergo error:
characters 1-34:typing error: real and int cannot be unified
[wp] [Alt-Ergo] Goal typed_main_call_foo_pre : Failed
characters 1-34:typing error: real and int cannot be unified
[wp] Proved goals: 0 / 1
Alt-Ergo: 0 (failed: 1)
## Attachments
- [bug.c](/uploads/24ea9349eeb21558e55d63d94453b416/bug.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/425Creating a pointer to a local causes valid pointers above it to lose thier va...2021-04-15T08:03:30Zmantis-gitlab-migrationCreating a pointer to a local causes valid pointers above it to lose thier valid statusID0002234:
**This issue was created automatically from Mantis Issue 2234. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002234:
**This issue was created automatically from Mantis Issue 2234. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002234 | Frama-C | Plug-in > wp | public | 2016-06-21 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jrobbins | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Pointers that are \valid lose their status as \valid if there is code below it that assigns to a pointer. This only seems to happen when the pointer in question is wrapped in a struct.
### Additional Information :
Tested on Aluminum on a Linux machine.
### Steps To Reproduce :
== file bug.c:
struct s {
int* ptr;
};
/*@
requires \valid(t.ptr);
@*/
void foo(struct s t) {
//@ assert \valid(t.ptr);
int a;
int* x = &a;
}
== Run command:
frama-c bug.c -wp
== Output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing bug.c (with preprocessing)
[wp] warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_foo_assert : Unknown (51ms)
[wp] Proved goals: 0 / 1
Alt-Ergo: 0 (unknown: 1)
== File fixed.c:
struct s {
int* ptr;
};
/*@
requires \valid(t.ptr);
@*/
void foo(struct s t) {
//@ assert \valid(t.ptr);
int a;
int* x; // = &a;
}
== Run command:
frama-c bug.c -wp
== Output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing bug.c (with preprocessing)
[wp] warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] Proved goals: 1 / 1
Qed: 1Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/489alt-ergo: undefined symbol andb2021-02-22T13:37:55Zmantis-gitlab-migrationalt-ergo: undefined symbol andbID0002159:
**This issue was created automatically from Mantis Issue 2159. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002159:
**This issue was created automatically from Mantis Issue 2159. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002159 | Frama-C | Plug-in > wp | public | 2015-09-14 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | azaostro | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | 64 bit | **OS** | Ubuntu | **OS Version** | 14.04 |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | Frama-C Aluminium |
### Description :
WP fails to handle my recursive boolean function, defined as "full_rec":
/*@ logic integer size_rec{L}(int* busybits, integer capa) =
@ (capa == 0) ? 0 :
@ (busybits[capa-1] != 0) ? 1 + size_rec(busybits, capa - 1) : 0;
@
@ logic boolean full_rec{L}(int *busybits, integer capa) =
@ (capa == 0) ? \true :
@ (busybits[capa-1] != 0) ? full_rec(busybits, capa - 1) : \false;
@
@ lemma full_rec_size_rec: \forall int* busybits, integer capa;
@ size_rec(busybits, capa) == capa <==> full_rec(busybits, capa);
*/
The result:
$ frama-c -wp repr.c
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing repr.c (with preprocessing)
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] 1 goal scheduled
/tmp/wpfaa705.dir/typed/lemma_full_rec_size_rec.ergo:13:[wp] user error: Alt-Ergo error:
characters 5-94:typing error: undefined symbol andb
[wp] [Alt-Ergo] Goal typed_lemma_full_rec_size_rec : Failed
Error: characters 5-94:typing error: undefined symbol andb
[wp] Proved goals: 0 / 1
Alt-Ergo: 0 (failed: 1)
### Steps To Reproduce :
run
frama-c -wp repr.c
on the attached file repr.c
## Attachments
- [repr.c](/uploads/78cf3015b33886cf55680addd2e02316/repr.c)https://git.frama-c.com/pub/frama-c/-/issues/491Zombie processes2021-02-22T14:01:38Zmantis-gitlab-migrationZombie processesID0002154:
**This issue was created automatically from Mantis Issue 2154. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002154:
**This issue was created automatically from Mantis Issue 2154. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002154 | Frama-C | Plug-in > wp | public | 2015-09-01 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kroeckx | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | Frama-C Aluminium |
### Description :
I'm starting it using:
frama-c-gui -wp -wp-rte -wp-proof alt-ergo <file>
There are lots of goals, and some take a long time to run. I end up with lots of zombie processes. The number of zombie processes matches the number of "interrupted" in the summary. For some reason it's not cleaning up those properly.https://git.frama-c.com/pub/frama-c/-/issues/492Under windows, many times, Frama-c wp process doesn't kill alt-ergo process b...2021-02-22T14:01:38Zmantis-gitlab-migrationUnder windows, many times, Frama-c wp process doesn't kill alt-ergo process before finishingID0002132:
**This issue was created automatically from Mantis Issue 2132. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002132:
**This issue was created automatically from Mantis Issue 2132. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002132 | Frama-C | Plug-in > wp | public | 2015-06-11 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | gaggarwal | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C Aluminium |
### Description :
On Windows system, Frama-c wp process finished without finishing all the alt-ergo processes it created, because of this in few mins, my system starts thrashing because these lying around alt-ergo processes take up all the CPU time.
If I run the test with frama-c wp + why3, why3 finishes all the alt-ergo processes before finishing.
Is there an option, that should be used to make sure alt-ergo processes are finished with frama-c process?https://git.frama-c.com/pub/frama-c/-/issues/494missing lower bound of ACSL operator ".." not detected by Magnesium2021-02-22T13:04:01ZJochen Burghardtmissing lower bound of ACSL operator ".." not detected by MagnesiumID0002230:
**This issue was created automatically from Mantis Issue 2230. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002230:
**This issue was created automatically from Mantis Issue 2230. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002230 | Frama-C | Plug-in > wp | public | 2016-06-13 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | suspended |
| **Priority** | none | **Severity** | feature | **Reproducibility** | always |
| **Platform** | Magnesium | **OS** | xubuntu-14.04 | **OS Version** | - |
| **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | Frama-C Aluminium |
### Description :
The Frama-C Magnesium parser didn't complain about the missing lower bound of "..".
The Frama-C Aluminium parser does find the syntax error (in fact, this was the way we detected it).
We therefore intend this issue not as a bug report, but merely as another regression test on future Frama-C releases. There is nothing to be fixed now.
## Attachments
- [486.c](/uploads/3fc4fdf16d4ecfe42871670515e0ef32/486.c)
- [max_element.c](/uploads/c5be5280ef02a12d06e4b53b840cb0b9/max_element.c)https://git.frama-c.com/pub/frama-c/-/issues/498Suggest to supply values of global consts to provers2021-02-22T13:38:09ZJochen BurghardtSuggest to supply values of global consts to proversID0001179:
**This issue was created automatically from Mantis Issue 1179. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001179:
**This issue was created automatically from Mantis Issue 1179. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001179 | Frama-C | Plug-in > wp | public | 2012-05-10 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Aluminium |
### Description :
Wp/Simplify couldn't prove behavior-disjointness in line 5 of the attached program. The reason is that no information about the fixed values of c1 and c2 appears in the proof obligation. If the declarations in line 1-2 are replaced by #define-s, the proof is trivially found.
I suggest to replace in the proof obligation each const variable by its value, if it is known at compile time. The latter restriction is satisfied for all variables visible in contracts (as opposed e.g. to asserts).
Preferring C constants to macros is considered good software engineering practice; it shouldn't be discouraged by Frama-C/Wp.
## Attachments
- [ftest.c](/uploads/63c096ef4b4a9ed37296112df602eff4/ftest.c)
- [ftest2.c](/uploads/76bf2003b18bd8a2ec4845f0fe129d03/ftest2.c)https://git.frama-c.com/pub/frama-c/-/issues/499Unexpected error (Invalid_argument("Z.shift_left: count argument must be posi...2021-05-18T08:55:43Zmantis-gitlab-migrationUnexpected error (Invalid_argument("Z.shift_left: count argument must be positive"))ID0002201:
**This issue was created automatically from Mantis Issue 2201. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002201:
**This issue was created automatically from Mantis Issue 2201. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002201 | Frama-C | Plug-in > wp | public | 2016-01-22 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | rcl | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Linux | **OS** | Ubuntu | **OS Version** | 14.04 |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | Frama-C Aluminium |
### Description :
With the help of a custom csmith variant, a program was discovered that causes an unexpected error in the wp plugin. The following program is a reduced minimal example of the failing program discovered by csmith:
/*@ assigns \nothing; */
int main()
{
int foo = 1;
1 & (foo & 0x80000000000001LL) << 1;
return 0;
}
The crash message is:
Raised at file "src/wp/register.ml", line 579, characters 30-32
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 763, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Unexpected error (Invalid_argument("Z.shift_left: count argument must be positive")).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Sodium-20150201.
### Steps To Reproduce :
Save the aforementioned program into a file named test.c, then execute
frama-c -wp test.c
to cause the crash.
## Attachments
- [test.c](/uploads/1538550928d60f17405b687f59ab5e2b/test.c)https://git.frama-c.com/pub/frama-c/-/issues/501coq fails to compile Cint because Zbits is not found2021-02-22T13:04:18Zmantis-gitlab-migrationcoq fails to compile Cint because Zbits is not foundID0002155:
**This issue was created automatically from Mantis Issue 2155. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002155:
**This issue was created automatically from Mantis Issue 2155. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002155 | Frama-C | Plug-in > wp | public | 2015-09-02 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kroeckx | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | Frama-C Aluminium |
### Description :
As described in https://lists.gforge.inria.fr/pipermail/frama-c-discuss/2014-March/004380.html, I get the same error message that Cint can't be compiled because Zbits isn't compiled yet.
I'm getting this on a Debian system.
I attached a patch based on the mail that seems to fix the issue for me.
## Attachments
- [wp.driver.patch](/uploads/a497ab58ae4dc3b1ac4220b14fafbd1d/wp.driver.patch)https://git.frama-c.com/pub/frama-c/-/issues/504Reals are bad encoded for coq2021-02-22T13:04:23Zmantis-gitlab-migrationReals are bad encoded for coqID0002214:
**This issue was created automatically from Mantis Issue 2214. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002214:
**This issue was created automatically from Mantis Issue 2214. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002214 | Frama-C | Plug-in > wp | public | 2016-03-03 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | davyg | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | All | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | Frama-C Aluminium |
### Description :
The definition of real_base(Qedlib) in the coq exporter of wp is incorrect :
There is :
Definition real_base e a n :=
match n with
| 0 => 1%R
| Zpos n => (a * pow e (Pos.to_nat n))%R
| Zneg n => (a / pow e (Pos.to_nat n))%R
end.
in stead of
Definition real_base e a n :=
match n with
| 0 => a
| Zpos n => (a * pow e (Pos.to_nat n))%R
| Zneg n => (a / pow e (Pos.to_nat n))%R
end.
### Steps To Reproduce :
I think that any coq proof you try to prove with wp containing real constant should have the errorhttps://git.frama-c.com/pub/frama-c/-/issues/507Use of very large real constants cause failures in proof generation in WP2021-04-14T15:49:36Zmantis-gitlab-migrationUse of very large real constants cause failures in proof generation in WPID0002232:
**This issue was created automatically from Mantis Issue 2232. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002232:
**This issue was created automatically from Mantis Issue 2232. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002232 | Frama-C | Plug-in > wp | public | 2016-06-14 | 2016-06-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jrobbins | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Ununtu 64-bit | **OS** | Linux | **OS Version** | 16.04 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Code that uses real constants larger than the size of a double cause a failure to prove, even with true assertions. When WP tries to create the proof for files containing those constants, the kernel crashes with the message of Invalid_argument("Unrecognized constant \"inf\"") in the middle of generating the files to send to the prover.
### Additional Information :
This was tested in the public Aluminum version, on both a Linux and Cygwin build.
### Steps To Reproduce :
== File bug.c (attached):
int main() {
//@ assert 1.0 < 0x1.0p2047;
}
== Run command:
frama-c bug.c -wp -wp-print
== Output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing bug.c (with preprocessing)
[wp] warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_main_assert : Failed
Invalid_argument("Unrecognized constant \"inf\"")
[wp] Proved goals: 0 / 1
Alt-Ergo: 0 (failed: 1)
------------------------------------------------------------
Function main
------------------------------------------------------------
Goal Assertion (file bug.c, line 2):
Prove: .1e0 < [kernel] Current source was: bug.c:1
The full backtrace is:
Raised at file "src/kernel_services/plugin_entry_points/log.ml", line 159, characters 51-56
Called from file "src/plugins/wp/register.ml", line 535, characters 8-22
Called from file "src/libraries/stdlib/extlib.ml", line 334, characters 14-17
Re-raised at file "src/libraries/stdlib/extlib.ml", line 334, characters 47-48
Called from file "src/libraries/stdlib/extlib.ml", line 335, characters 2-12
Called from file "src/libraries/stdlib/extlib.ml", line 335, characters 2-12
Called from file "queue.ml", line 134, characters 6-20
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 787, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 817, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8
Unexpected error (Invalid_argument("Unrecognized constant \"inf\"")).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Aluminium-20160501.
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
== Note that the constant "0x1.0p2047" can be replaced with any value greater than or equal to 0x2.0p1023; even other forms of real constant other than hexadecimal.
## Attachments
- [bug.c](/uploads/8354bd56c66b755df3ee5650534570dd/bug.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/508Validation fails when predicate is used with implicit type conversion.2021-04-15T08:54:27Zmantis-gitlab-migrationValidation fails when predicate is used with implicit type conversion.ID0002229:
**This issue was created automatically from Mantis Issue 2229. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002229:
**This issue was created automatically from Mantis Issue 2229. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002229 | Frama-C | Plug-in > wp | public | 2016-05-31 | 2016-05-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Ian | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Ubuntu | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | - |
### Description :
When there is an implicit type conversion on a parameter, and the value is checked by a predicate, validation fails when it should succeed.
In the example below, the functions foo and foo_pred have the same precondition, except foo_pred has the statement in a predicate. foo validates while foo_pred does not.
run2 validates the assertion, showing the precondition should be true, but foo_pred still fails.
run3 is similar to run2 except a ghost variable is used. This causes foo_pred to validate.
### Steps To Reproduce :
File foo.c (attached):
/*@
predicate bar_req(int i) = ((unsigned char) i) == i;
*/
//@ requires ((unsigned char) i) == i;
void foo(int i) {
}
//@ requires bar_req(i);
void foo_pred(int i) {
}
void run(char c) {
unsigned char uc = c;
foo(uc); // Valid
foo_pred(uc); // Fails
}
void run2(char c) {
unsigned char uc = c;
//@ assert ((unsigned char) ((int) uc)) == uc;
foo_pred(uc); // Fails
}
void run3(char c) {
unsigned char uc = c;
//@ ghost int ic = uc;
//@ assert ((unsigned char) ic) == uc;
foo_pred(uc); // Valid
}
Run command:
frama-c foo.c -wp -wp-prover why3:alt-ergo -wp-model=typed+Cast
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing foo.c (with preprocessing)
[wp] warning: Missing RTE guards
[wp] 6 goals scheduled
[wp] [alt-ergo] Goal typed_cast_run2_call_foo_pred_pre : Unknown (158ms)
[wp] [alt-ergo] Goal typed_cast_run_call_foo_pred_pre : Unknown (Qed:0.54ms) (157ms)
[wp] Proved goals: 4 / 6
Qed: 3
alt-ergo: 1 (10ms) (unknown: 2)
## Attachments
- [foo.c](/uploads/792c293c47386d643589dcebe3f4d174/foo.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/509Oddities in the modeling of floats and doubles2021-04-15T08:53:31Zmantis-gitlab-migrationOddities in the modeling of floats and doublesID0002228:
**This issue was created automatically from Mantis Issue 2228. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002228:
**This issue was created automatically from Mantis Issue 2228. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002228 | Frama-C | Plug-in > wp | public | 2016-05-16 | 2016-05-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Ian | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Ubuntu | **OS Version** | - |
| **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | - |
### Description :
I a unsure of the modeling of floats and doubles provided in magnesium. There are three unexpected results I encountered.
1.
The following program proves the contradiction with the command:
frama-c -wp -wp-timeout 60 -wp-prover why3:z3-4.4.0 getNaN.c -no-tty
/*@ assigns \result;
ensures \is_NaN(\result);
*/
extern float getNaN();
void main() {
getNaN();
//@ assert Contradiction: \false;
}
2.
The following assertions are not proven (although I would expect them to be trivial) using the command:
frama-c -wp -wp-timeout 60 -wp-prover alt-ergo -no-tty fin.c
void foo() {
float a = 1.0;
//@ assert \is_finite(a);
}
void bar() {
double a = 1.0;
//@ assert \is_finite(a);
}
3.
The values for + or - INF are not modeled for floats or doubles. The following lemmas validate:
/*@
lemma inf_float:
\forall float x; \is_finite(x) || \is_NaN(x);
*/
/*@
lemma inf_double:
\forall double x; \is_finite(x) || \is_NaN(x);
*/Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/513Make find(1) command POSIX-compliant2021-08-05T14:12:49Zmantis-gitlab-migrationMake find(1) command POSIX-compliantID0002222:
**This issue was created automatically from Mantis Issue 2222. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002222:
**This issue was created automatically from Mantis Issue 2222. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002222 | Frama-C | Plug-in > wp | public | 2016-04-09 | 2016-04-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mmcc | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | All | **OS** | OpenBSD | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
src/plugins/wp/share/Makefile uses the -delete option of find(1), which is a GNU extension. The same behavior can be achieved using the POSIX-specified -exec option. The attached patch changes this Makefile to use -exec, fixing 'make clean' on systems that don't use GNU find.
Thanks,
Mike
### Steps To Reproduce :
Run 'make clean' on a system that uses a non-GNU find(1) utility.
## Attachments
- [t.diff](/uploads/095f86b8d788cfe86e200c4ce7eec41b/t.diff)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/514Crash with large array initialisation2021-04-15T08:48:55Zmantis-gitlab-migrationCrash with large array initialisationID0002219:
**This issue was created automatically from Mantis Issue 2219. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002219:
**This issue was created automatically from Mantis Issue 2219. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002219 | Frama-C | Plug-in > wp | public | 2016-03-18 | 2016-03-22 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | szt | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | x86-64 | **OS** | GNU/Linux | **OS Version** | Ubuntu 14.04.4 |
| **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | - |
### Description :
wp plugin crashes when I try to check code
### Additional Information :
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing ../../prog/array_testcase.c (with preprocessing)
[kernel] Current source was: ../../prog/array_testcase.c:1
The full backtrace is:
Raised at file "src/plugins/wp/register.ml", line 607, characters 30-32
Called from file "queue.ml", line 134, characters 6-20
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 778, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 227, characters 4-8
Unexpected error (Stack overflow).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Magnesium-20151002.
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 :
just run
frama-c -wp -wp-proof alt-ergo array_testcase.c
## Attachments
- [array_testcase.c](/uploads/38b172c0d08b3e77a7af8dddf97dc43f/array_testcase.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/522provide option "-wp-lemma"2021-02-22T13:04:45ZJens Gerlachprovide option "-wp-lemma"ID0002202:
**This issue was created automatically from Mantis Issue 2202. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002202:
**This issue was created automatically from Mantis Issue 2202. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002202 | Frama-C | Plug-in > wp | public | 2016-01-23 | 2016-02-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
WP has several options to consider only individual functions, properties, or behaviors during verification.
It would be nice if there were an option "-wp-lemma 'name' " which would allow to consider only the names lemma.