GitLab

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.