Unexpected timeout
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.