frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2022-09-26T13:57:21Zhttps://git.frama-c.com/pub/frama-c/-/issues/2607Unexpected timeout2022-09-26T13:57:21ZsuperymkUnexpected 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.