Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 209
    • Issues 209
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #2607

Closed
Open
Created Apr 05, 2022 by superymk@superymk

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.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking