frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-08-05T13:14:10Zhttps://git.frama-c.com/pub/frama-c/-/issues/2098suggest to provide FILE,LINE references for proof obligations in WP cmd-line ...2021-08-05T13:14:10ZJochen Burghardtsuggest to provide FILE,LINE references for proof obligations in WP cmd-line outputID0001011:
**This issue was created automatically from Mantis Issue 1011. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001011:
**This issue was created automatically from Mantis Issue 1011. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001011 | Frama-C | Plug-in > wp | public | 2011-11-04 | 2011-11-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Currently, the command-line (i.e. non-gui) version of WP gives internally-generated names of proof obligations, like e.g.
[wp] [Simplify] Goal store_axiom_pop_of_push_pre31_push_stack_s1 : Valid
[wp] [Simplify] Goal store_axiom_pop_of_push_pre26_pop_stack_s2 : Timeout
In order to support the user in improving his program to get it verified, it should be made clear where an unproven obligation originated from, by providing file name and line number. Although a lot of information can be found in the directory specified with "-wp-out", the FILE,LINE information cannot.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1028Extend smoke tests to incoherent specification of declared functions2023-07-21T13:48:46ZDillon ParienteExtend smoke tests to incoherent specification of declared functionsID0001537:
**This issue was created automatically from Mantis Issue 1537. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001537:
**This issue was created automatically from Mantis Issue 1537. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001537 | Frama-C | Plug-in > wp | public | 2013-10-28 | 2014-06-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
[STANCE]
The following code:
```
//@ assigns \result \from p; ensures sizeof(\result)==5;
char*g(char*p);
void f()
{
char *p=g(p);
//@ assert sizeof(p)==5;
//@ assert \false;
}
```
analyzed by:
frama-c foo.c -no-unicode -wp
Qed proves the 2nd assert in f():
[wp] [Qed] Goal typed_f_assert_2 : ValidLoïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1023WP crash when type casting in lemma2021-04-15T15:42:55Zmantis-gitlab-migrationWP crash when type casting in lemmaID0001804:
**This issue was created automatically from Mantis Issue 1804. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001804:
**This issue was created automatically from Mantis Issue 1804. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001804 | Frama-C | Plug-in > wp | public | 2014-06-06 | 2014-06-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Ian | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | Ubuntu | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
When using Typed+cast, a cast in a lemma can cause wp to crash.
In the below example, removing the lemma will cause the assert to validate.
### Steps To Reproduce :
Create file ptr_cast.c :
/*@
lemma valid_pointers:
\forall int **ptr; sizeof(int *) >= sizeof(int) ==> \valid(ptr) ==> \valid((int *) ptr);
*/
void f(int **ptr){
//@ assert sizeof(int *) >= sizeof(int) ==> \valid(ptr) ==> \valid((int *) ptr);
}
Run :
frama-c -cpp-command 'gcc -C -E' -pp-annot -wp -wp-model Typed+cast ptr_cast.c
Receive output :
[kernel] preprocessing with "gcc -C -E -dD ptr_cast.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
ptr_cast.c:4:[wp] warning: Cast with incompatible pointers types (source: int**) (target: sint32*)
[wp] failure: Context 'Warning' non-initialized.
[kernel] Current source was: ptr_cast.c:7
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "src/wp/Warning.ml", line 117, characters 10-31
Called from file "src/wp/MemTyped.ml", line 799, characters 3-111
Called from file "src/wp/MemVar.ml", line 374, characters 23-51
Called from file "src/wp/Cvalues.ml", line 433, characters 30-42
Called from file "src/wp/LogicSemantics.ml", line 768, characters 12-27
Called from file "src/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/wp/Context.ml", line 34, characters 41-46
Called from file "src/wp/LogicCompiler.ml", line 358, characters 20-35
Called from file "src/wp/LogicSemantics.ml", line 779, characters 12-37
Called from file "src/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/wp/Context.ml", line 34, characters 41-46
Called from file "src/wp/LogicCompiler.ml", line 357, characters 28-51
Called from file "src/wp/LogicSemantics.ml", line 779, characters 12-37
Called from file "src/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/wp/Context.ml", line 34, characters 41-46
Called from file "src/wp/LogicCompiler.ml", line 357, characters 28-51
Called from file "src/wp/LogicSemantics.ml", line 779, characters 12-37
Called from file "src/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/wp/Context.ml", line 34, characters 41-46
Called from file "src/wp/Lang.ml", line 869, characters 33-38
Re-raised at file "src/wp/Lang.ml", line 870, characters 40-43
Called from file "src/wp/LogicSemantics.ml", line 684, characters 11-54
Called from file "src/wp/LogicSemantics.ml", line 779, characters 12-37
Called from file "src/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/wp/Context.ml", line 34, characters 41-46
Called from file "src/wp/LogicCompiler.ml", line 326, characters 14-25
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/LogicCompiler.ml", line 401, characters 24-83
Called from file "src/wp/LogicCompiler.ml", line 673, characters 6-97
Called from file "src/wp/LogicCompiler.ml", line 690, characters 19-41
Called from file "src/wp/cfgWP.ml", line 1294, characters 31-42
Called from file "map.ml", line 169, characters 20-25
Called from file "src/wp/cfgWP.ml", line 1369, characters 14-54
Called from file "src/wp/Model.ml", line 111, characters 17-20
Re-raised at file "src/wp/Model.ml", line 116, characters 25-28
Called from file "src/wp/Model.ml", line 117, characters 19-36
Called from file "src/wp/register.ml", line 435, characters 17-42
Called from file "src/wp/register.ml", line 574, characters 17-24
Re-raised at file "src/wp/register.ml", line 578, characters 29-31
Called from file "src/wp/register.ml", line 575, characters 17-24
Re-raised at file "src/wp/register.ml", line 579, characters 32-34
Called from file "src/wp/register.ml", line 575, characters 17-24
Re-raised at file "src/wp/register.ml", line 579, characters 32-34
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 37, characters 4-20
Called from file "src/kernel/cmdline.ml", line 735, characters 2-9
Called from file "src/kernel/cmdline.ml", line 214, characters 4-8
Plug-in wp aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelinesAllan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/907axiom "addr_le_def" given to Alt-Ergo considered too weak2021-08-05T14:15:00ZJochen Burghardtaxiom "addr_le_def" given to Alt-Ergo considered too weakID0002047:
**This issue was created automatically from Mantis Issue 2047. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002047:
**This issue was created automatically from Mantis Issue 2047. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002047 | Frama-Clang | Plug-in > wp | public | 2015-01-12 | 2015-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Jan2015-Neon-20140301+dev-STANC | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The loop invariant "xx5" of the attached program "fill1.c" can't be proven with Alt-Ergo. The goal reads fine, viz.:
goal fill_loop_inv_xx5_preserved:
forall a_3,a_2,a_1,a : addr.
(a_1 <> a_2) ->
addr_le(a_3, a_2) ->
(region(a.base) <= 0) ->
(region(a_3.base) <= 0) ->
addr_le(a_3, shift_sint16(a_2, 1))
However, the axiom "addr_le_def" appears to be too weak, it currently reads:
axiom addr_le_def :
(forall p:addr. forall q:addr [addr_le(p, q)]. (((p).base = (q).base) ->
(addr_le(p, q) -> ((p).offset <= (q).offset))))
While the loop inveriant certainly should be provable, I don't see any way to prove a_3.base=a_2.base with the current version of the file.
Moreover, in order for axioms "addr_le_def" and "addr_le_def1" to be a definition of "addr_le(.,.)" in terms of "=" and "<=" etc., axiom "addr_le_def" should be changed to:
axiom addr_le_def :
(forall p:addr. forall q:addr [addr_le(p, q)].
(addr_le(p, q) -> p.base = q.base and p.offset <= q.offset))
After that change, Alt-Ergo proves the goal without any problems. The attached file "fill_loop_inv_xx5_preserved_Alt-Ergo.mlw" contains the changed version in a comment at line 408.
If my argument is right, the whole axiomatization should be reviewed to remove similar flaws, which give Frama-C a rather poor performance on address arithmetic. (For that reason, I assigned a higher severity.)
### Additional Information :
Originally, I'd submitted this issue to the Alt-Ergo issue tracker, see https://github.com/OCamlPro/alt-ergo/issues/9. I'm indebted to Mohamed Iguernelala for hinting at the weak axiom "addr_le_def", where I had a blind spot.
## Attachments
- [fill1.c](/uploads/e5ff187165a5e10b7858e1f325eea68a/fill1.c)
- [fill_loop_inv_xx5_preserved_Alt-Ergo.mlw](/uploads/6292554fc2953d67792737e6dac31199/fill_loop_inv_xx5_preserved_Alt-Ergo.mlw)
- [fill.c](/uploads/c1dcc11d568e2e09d95aeabf0b9df093/fill.c)
- [fill4.c](/uploads/5ce99f117503a2df12c827af1b439520/fill4.c)
- [fill5.c](/uploads/ece00cbe919a18c0800d32b0adb27fb2/fill5.c)
- [fill4r.c](/uploads/81225ff5f9ecee0d89645919cbe59e44/fill4r.c)
- [find_arr.c](/uploads/fec90cf4fecefaee9a7cea344c14b693/find_arr.c)
- [find_ptr.c](/uploads/8430a7bbd76c8f263bd433d3cfd746d8/find_ptr.c)
- [find_ptr_foo_post_Alt-Ergo_modified.mlw](/uploads/d52e028cdf21562b07c9e340031cef8c/find_ptr_foo_post_Alt-Ergo_modified.mlw)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/370problem with Qed's simplification power2021-02-22T13:00:23ZJochen Burghardtproblem with Qed's simplification powerID0002278:
**This issue was created automatically from Mantis Issue 2278. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002278:
**This issue was created automatically from Mantis Issue 2278. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002278 | Frama-C | Plug-in > wp | public | 2017-02-06 | 2017-02-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Silicon-20161101 | **OS** | Ubuntu 16.04.1 LTS | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-out wp-out shift.c" on the attached file and inspecting the file "wp-out/typed/foo_post_Alt-Ergo.mlw" shows that lemma "ShiftAssociative" is simplified to "true" (see line 360) by Qed. (The postcondition of foo doesn't matter here, except that it is intentionally unprovable in order to demonstrate the lemma's simplification.)
This situation doesn't change even when all options to disable Qed functionality (i.e. "-wp-no-bits -wp-no-clean -wp-no-core -wp-no-filter -wp-no-init-summarize-array -wp-no-let -wp-no-pruning -wp-no-simpl -wp-no-simplify-forall -wp-no-simplify-is-cint -wp-no-simplify-type") are given. (In contrast, in the somewhat related issue #1751, providing option "-wp-no-bits" is sufficient to circumvent the problem.)
While Qed's simplification capabilities are appreciated in general, the disappearance of the lemma can be a problem:
* In many Coq proofs related to C address computation, a similar lemma has to be stated and proven again and again. There seems to be no easy way to make Coq see what is considered trivial by Qed.
* Considering the discussion at https://github.com/OCamlPro/alt-ergo/issues/19, if I understood the Alt-Ergo people right, Alt-Ergo isn't complete on linear arithmetic with arrays (except for quantifier-free formulas). Therefore it sometimes needs trivial lemmas. In the particular example, to make Alt-Ergo prove the goal "reverse", a kind of associtivity property (axiom "arith") is needed that Qed would simplify also to "true", and even Alt-Ergo would.
Generally speaking, Qed should be (configurable such that it is) no stronger than any of the external provers, such as Coq and Alt-Ergo. This would enable the user to provide appropriate prover hints that are not simplified away by Qed. Maybe a command line option to completely switch off Qed is sufficient. As an alternative, a command-line switch could reduce the capabilities of Qed when applied to lemmas, assuming that the user is responsible to give them in an optimal form.
## Attachments
- [shift.c](/uploads/572d124b06bee30721a80150255027ac/shift.c)
- [foo_post_Alt-Ergo.mlw](/uploads/746bbaa9bc36a947691d7be190773542/foo_post_Alt-Ergo.mlw)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/54An option to return error code if there are any problems with the analysis, s...2021-03-29T11:49:28ZvarosiAn option to return error code if there are any problems with the analysis, so that frama-c is easier to be used in CI/CD workflowsFeature Request
- [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 old
[BTS](https://bts.frama-c.com) (*note: the old BTS is deprecated*...Feature Request
- [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 old
[BTS](https://bts.frama-c.com) (*note: the old BTS is deprecated*);
- [X] you installed Frama-C as prescribed in the [instructions](INSTALL.md).
# Contextual information
- Frama-C installation mode: Docker: framac/frama-c:22.0
- Frama-C version: 22.0
- Plug-in used: WP and EVA
- OS name: macOS
- OS version: 11.1
# Steps to reproduce the issue
I put frama-c in a BitBucket CI pipeline. With calling directly frama-c executable. CI pipelines fail when error code returned from executables is different than 0. That way it stops you from pushing erroneous code.
# Expected behaviour
It would be great if there is an option so that frama-c executable return non-zero error code if in EVA found any error in my code, or in WP not all conditions are met.
# Actual behaviour
frama-c return 0 even if EVA show errors from the analysed code. It returns 0 if WP have found non correct behaviour also.https://git.frama-c.com/pub/frama-c/-/issues/47Why3 configuration for Frama-C2021-03-31T10:31:21ZAllan BlanchardWhy3 configuration for Frama-C#### Why3 configuration
We should clarify how we should produce the Why3 configuration file in the case of Frama-C. For opam installation we have added a message at the end of the installation but it is easy to ignore (or miss) this mes...#### Why3 configuration
We should clarify how we should produce the Why3 configuration file in the case of Frama-C. For opam installation we have added a message at the end of the installation but it is easy to ignore (or miss) this message. Furthermore, it is not applicable for Linux distribution packages.
One possibility for us could be to generate a Why3 configuration for Frama-C, that would always be used (unless some environment variable or option is set for example).
#### How to get a prover?
Currently, we use:
- `Why3.Whyconf.parse_filter_prover`
- `Why3.Whyconf.filter_one_prover`
However we currently can call them 3 times *for each* prover. One of them is due to the fact that we can have a composed name like "shortname,version,other_info", but for the two others we have a first call with the received name and the second for this same name but in lower case, and both are necessary (see: https://git.frama-c.com/pub/frama-c/-/issues/41#note_99186).
This shoul be simpler on both Frama-C and Why3 sides.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/32Known WP limitation: Dynamic allocation is not supported2023-07-21T13:06:10ZBob RubbensKnown WP limitation: Dynamic allocation is not supportedHello everyone,
A colleague of mine tried to use variables as a length argument for an array:
```c
int const n = 4;
int main() {
int xs[n];
}
```
This yielded the following frama-c output:
```bash
[nix-shell:~]$ frama-c -wp program...Hello everyone,
A colleague of mine tried to use variables as a length argument for an array:
```c
int const n = 4;
int main() {
int xs[n];
}
```
This yielded the following frama-c output:
```bash
[nix-shell:~]$ frama-c -wp program.c
[kernel] Parsing program.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] program.c:4: Warning:
Cast with incompatible pointers types (source: sint32*) (target: sint8*)
[wp] program.c:4: Warning:
Cast with incompatible pointers types (source: sint8*) (target: sint32*)
[wp] 1 goal scheduled
[wp] Proved goals: 1 / 1
Qed: 1
```
Frama-c version (for completeness, I'm using the version from nixpkgs unstable):
```bash
[nix-shell:~]$ frama-c --version
21.1 (Scandium)
```
The warning seems strange, as I use only ints in this program. With my limited knowledge of C, I'd say this program does no such casting. Is this a bug or is this somehow a subtle edge case in C? Or is it benign and can it be ignored?Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/30Wanted features related to Why3-Coq2020-10-02T11:00:15ZAllan BlanchardWanted features related to Why3-CoqThis is a follow up on frama-c/frama-c#956 and discussion we had with Jens on the ACSL by Example GitLab about Coq via Why3 in Frama-C.
At least two features could be added to make it easier to use (in particular for ACSL by Example):
...This is a follow up on frama-c/frama-c#956 and discussion we had with Jens on the ACSL by Example GitLab about Coq via Why3 in Frama-C.
At least two features could be added to make it easier to use (in particular for ACSL by Example):
1. drivers that are only applied to Coq (or any prover), an that can be verified,
2. user defined (restricted) context for the proof of lemmas in Coq.
### Drivers
This shall be the job of the driver. We probably need to a way to refine the why3 context *per prover*. Then, it is easy to enrich the Task generated by `ProverWhy3`, which is already « prepared » in a specific way for each prover.
Currently, the supported import directives for WP drivers are:
```
why3.file="mydir/foo.why"
why3.file="mydir/foo.why:Bar"
why3.file="mydir/foo.why:Bar:T"
why3.import="foo.Bar"
why3.import="foo.Bar:T"
```
@lcorrenson suggests to reformulate all of them into something fully understandable from why3 users:
```
[for "myProver",...] loadpath "path/to/dir";
[for "myProver",...] import foo.Bar [as T];
```
This is indeed more flexible than using our custom `meta` directives.
### Restricted context
If we have two files like:
```c
lemma Foo: // ...
lemma To_Prove: // uses Foo
```
```c
lemma Bar: // ...
lemma Foo: // ...
lemma To_Prove: // uses Foo
```
The two files generate different proof contexts for lemmas, because even if `To_Prove` only needs `Foo`, WP collects all lemmas that appear before `To_Prove`. This is why I suggest to provide the user with a way to specify precisely the proof context so that it can remain the same from a file to another.
I think we could create an ACSL extension like:
```c
/*@
lemma Foo: ...
lemma Bar: ...
lemma Proved_with_Coq: ...
lemma_dependencies Proved_with_Coq: Foo ;
*/
```
So that the user can restrict the proof context of the lemma can be as simple and predictable as possible. Note that we should check that it compatible with the `RefUsage` analysis.Allan BlanchardAllan Blanchard