frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2022-04-06T16:19:00Zhttps://git.frama-c.com/pub/frama-c/-/issues/2607Unexpected timeout2022-04-06T16:19:00ZsuperymkUnexpected timeout<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
Source file: swap1.h
```
/*@
@ requires \valid(a) && \valid(b);
@ requires a != b;
@ ensures P1: *a == \old(*b) ;
@ assigns *a;
@*/
void fn_a(int *a,int *b) ;
/*@ ghost
/@ ensures LP1: 2 > 1;
@/
void lemma_abc(int a, int b)
{
}
*/
```
Source file: swap.c
```
#include "swap1.h"
void fn_a(int *a,int *b)
{
*a = *b ;
//@ assert AP1: *a == *b;
//@ ghost lemma_abc(1,2);
return ;
}
```
### Expected behaviour
Verification succeed
### Actual behaviour
Verification times out.
I use the command "frama-c -wp -wp-rte -wp-timeout 10 swap.c swap1.h -then -report", the output is:
```
[kernel] Parsing swap.c (with preprocessing)
[kernel] Parsing swap1.h (with preprocessing)
[kernel] swap1.h:13: Warning:
dropping duplicate def'n of func lemma_abc at swap1.h:13 in favor of that at swap1.h:13
[rte] annotating function fn_a
[rte] annotating function lemma_abc
[wp] 9 goals scheduled
[wp] [Alt-Ergo 2.4.1] Goal typed_fn_a_ensures_P1 : Timeout (Qed:3ms) (10s)
[wp] [Alt-Ergo 2.4.1] Goal typed_fn_a_assigns_exit_part2 : Timeout (Qed:3ms) (10s)
[wp] [Alt-Ergo 2.4.1] Goal typed_fn_a_assigns_normal_part2 : Timeout (Qed:3ms) (10s)
[wp] Proved goals: 6 / 9
Qed: 4 (0.63ms-1ms-2ms)
Alt-Ergo 2.4.1: 2 (7ms) (30) (interrupted: 3)
[wp:pedantic-assigns] swap1.h:13: Warning:
No 'assigns' specification for function 'lemma_abc'.
Callers assumptions might be imprecise.
[report] Computing properties status...
--------------------------------------------------------------------------------
--- Properties of Function 'fn_a'
--------------------------------------------------------------------------------
[ - ] Post-condition 'P1'
tried with Wp.typed.
[ - ] Assigns (file swap1.h, line 5)
tried with Wp.typed.
[ Valid ] Assertion 'AP1' (file swap.c, line 7)
by Wp.typed.
[ Valid ] Assertion 'rte,mem_access' (file swap.c, line 5)
by Wp.typed.
[ Valid ] Assertion 'rte,mem_access' (file swap.c, line 5)
by Wp.typed.
[ - ] Default behavior
tried with Frama-C kernel.
--------------------------------------------------------------------------------
--- Properties of Function 'lemma_abc'
--------------------------------------------------------------------------------
[ Valid ] Post-condition 'LP1'
by Wp.typed.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
5 Completely validated
3 To be validated
8 Total
--------------------------------------------------------------------------------
```
### Contextual information
- Frama-C installation mode: Opam 2.0.5, (opam switch: 4.14.0 ocaml-base-compiler.4.14.0 4.14.0)
- Frama-C version: 24.0 (Chromium)
- Plug-in used: WP
- OS name: Ubuntu 20.04.4 LTS x64
- OS version: *OS version*
### Additional information (optional)
Comment out the line "//@ ghost lemma_abc(1,2);" works good. But calling this ghost function causes timeout. The post-condition of lemma_abc is true, so the timeout issue looks weird.
My lemmas need parameters and non-trivial steps to prove; e.g., an equivalence of "lemma" in Dafny. If I understand correctly, the lemma keyword in frama-c does not take parameters.https://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