Wiki Agenda Contact Version française

A Formal Proof of a Unix Path Resolution Algorithm

A Path Resolution Algorithm is shown terminating, correct and complete.


Authors: Claude Marché / Martin Clochard / Ran Chen

Topics: Inductive predicates

Tools: Why3

see also the index (by topic, by tool, by reference, by year)


download ZIP archive

A Formal Proof of an Unix Path Resolution Algorithm


Formalization of File Systems and Path Resolution

module FileSystem

  use import int.Int
  use import int.MinMax

  use export list.List
  use export option.Option

Pathnames

  type filename
  type pathcomponent = Down filename | Up | Here

Up denotes ".." and Here denotes "."

  type path = list pathcomponent

File System

  type dirnode
  type child =
    | Absent
    | Dir dirnode
    | AbsLink path
    | RelLink path
  constant root : dirnode
  function lookup dirnode filename : child
  function parent dirnode : dirnode
    axiom parent_root: parent root = root
    axiom parent_non_root: forall d1 f d2. lookup d1 f = Dir d2 -> parent d2 = d1

Resolution Predicates

  inductive resolve_to dirnode path dirnode =
    | ResolveNil : forall d. resolve_to d Nil d
    | ResolveDir : forall d1 fn d2 p d3.
      lookup d1 fn = Dir d2 -> resolve_to d2 p d3 -> resolve_to d1 (Cons (Down fn) p) d3
    | ResolveAbsLink : forall d1 fn ps pr d2 d3.
      lookup d1 fn = AbsLink ps -> resolve_to root ps d2 -> resolve_to d2 pr d3 ->
      resolve_to d1 (Cons (Down fn) pr) d3
    | ResolveRelLink : forall d1 fn ps pr d2 d3.
      lookup d1 fn = RelLink ps -> resolve_to d1 ps d2 -> resolve_to d2 pr d3 ->
      resolve_to d1 (Cons (Down fn) pr) d3
    | ResolveUp: forall d1 d2 d3 p.
      parent d1 = d2 -> resolve_to d2 p d3 -> resolve_to d1 (Cons Up p) d3
    | ResolveHere: forall d1 p d2.
      resolve_to d1 p d2 -> resolve_to d1 (Cons Here p) d2

  inductive resolve_with_height dirnode path (option (dirnode,int)) =
    | ResolveHeightAbsent: forall d p. (forall d1. not resolve_to d p d1) ->
                        resolve_with_height d p None
    | ResolveHeightNil : forall d. resolve_with_height d Nil (Some (d,0))
    | ResolveHeightDir : forall d1 fn d2 p d3 h.
      lookup d1 fn = Dir d2 -> resolve_with_height d2 p (Some(d3,h)) ->
      resolve_with_height d1 (Cons (Down fn) p) (Some (d3,h + 1))
    | ResolveHeightAbsLink : forall d1 fn ps pr d2 d3 h1 h2.
      lookup d1 fn = AbsLink ps -> resolve_with_height root ps (Some (d2,h1)) ->
      resolve_with_height d2 pr (Some (d3,h2)) ->
      resolve_with_height d1 (Cons (Down fn) pr) (Some (d3, max h1 h2 + 1))
    | ResolveHeightRelLink : forall d1 fn ps pr d2 d3 h1 h2.
      lookup d1 fn = RelLink ps -> resolve_with_height d1 ps (Some (d2,h1)) ->
      resolve_with_height d2 pr (Some (d3,h2)) ->
      resolve_with_height d1 (Cons (Down fn) pr) (Some (d3,max h1 h2 + 1))
    | ResolveHeightUp : forall d1 d2 d3 p h.
      parent d1 = d2 -> resolve_with_height d2 p (Some(d3, h)) ->
      resolve_with_height d1 (Cons Up p) (Some (d3,h + 1))
    | ResolveHeightHere : forall d1 p d2 h.
      resolve_with_height d1 p (Some (d2,h)) ->
      resolve_with_height d1 (Cons Here p) (Some (d2,h + 1))

  lemma resolve_height_resolve : forall d1 p d2 h.
    resolve_with_height d1 p (Some(d2, h)) -> resolve_to d1 p d2

  lemma resolve_height_pos : forall d1 p d2 h.
    resolve_with_height d1 p (Some (d2,h)) -> h >= 0

  lemma resolve_make_height : forall d1 p d2. resolve_to d1 p d2 ->
    exists h. resolve_with_height d1 p (Some(d2, h))

end

Conformance with POSIX informal definition

module POSIX_resolution

  use import FileSystem
  use import list.Append

  lemma resolve_to_append : forall d1 d2 d3 p q.
     ("induction" resolve_to d1 p d2) ->
     resolve_to d2 q d3 ->
     resolve_to d1 (p ++ q) d3

  lemma resolve_to_cons : forall d1 d2 d3 c p.
     resolve_to d1 (Cons c Nil) d2 ->
     resolve_to d2 p d3 ->
     resolve_to d1 (Cons c p) d3

  let lemma resolve_to_decomp (d1 d3:dirnode) (c:pathcomponent) (p2:path)
    requires { resolve_to d1 (Cons c p2) d3 }
    ensures { exists d2. resolve_to d1 (Cons c Nil) d2 /\ resolve_to d2 p2 d3 }
  = ()

  let lemma resolve_to_decomposition (p1 p2:path) (d1 d3:dirnode)
    requires { resolve_to d1 (p1 ++ p2) d3 }
    ensures { exists d2. resolve_to d1 p1 d2 /\ resolve_to d2 p2 d3 }
  = ()

  inductive resolve_to_POSIX dirnode path dirnode =
    | ResolveNilPOSIX : forall d. resolve_to_POSIX d Nil d
    | ResolveDirPOSIX : forall d1 fn d2 p d3.
      lookup d1 fn = Dir d2 -> resolve_to_POSIX d2 p d3 ->
      resolve_to_POSIX d1 (Cons (Down fn) p) d3
    | ResolveAbsLinkPOSIX : forall d1 fn ps pr d2.
      lookup d1 fn = AbsLink ps -> resolve_to_POSIX root (ps ++ pr) d2 ->
      resolve_to_POSIX d1 (Cons (Down fn) pr) d2
    | ResolveRelLinkPOSIX : forall d1 fn ps pr d2.
      lookup d1 fn = RelLink ps -> resolve_to_POSIX d1 (ps ++ pr) d2 ->
      resolve_to_POSIX d1 (Cons (Down fn) pr) d2
    | ResolveUpPOSIX: forall d1 d2 d3 p.
      parent d1 = d2 -> resolve_to_POSIX d2 p d3 ->
      resolve_to_POSIX d1 (Cons Up p) d3
    | ResolveHerePOSIX: forall d1 p d2.
      resolve_to_POSIX d1 p d2 -> resolve_to_POSIX d1 (Cons Here p) d2

  lemma resolve_to_POSIX_append:
    forall d1 d2 p1. resolve_to_POSIX d1 p1 d2 ->
      forall p2 d3. resolve_to_POSIX d2 p2 d3 ->
      resolve_to_POSIX d1 (p1 ++ p2) d3

  lemma resolve_to_equivalence:
    forall d1 d2 p. resolve_to_POSIX d1 p d2 <-> resolve_to d1 p d2

end

Determinism of Path Resolution

theory Determinism

  use import int.Int
  use import FileSystem

  lemma resolve_unique : forall d1 p d2.
    resolve_to d1 p d2 -> forall d3. resolve_to d1 p d3 -> d2 = d3

  lemma resolve_with_height_unique:
      forall d p h1. resolve_with_height d p h1 ->
      forall h2. resolve_with_height d p h2 -> h1 = h2
      by match h1, h2 with
      | None, None -> true
      | _, None | None, _ -> false
      | Some(_,u), Some(_,v) -> u = v end

  lemma resolve_with_height_exists :
    forall d p. exists h. resolve_with_height d p h

end

Path Resolution Algorithm

module Resolution

  use import int.Int
  use import FileSystem
  use Determinism

obvious technical lemmas, but needed to help provers

  lemma resolve_height_absLink:
    forall d x p r h ps d' h'. resolve_with_height d (Cons (Down x) p) (Some(r, h)) ->
      lookup d x = AbsLink ps -> resolve_with_height root ps (Some(d', h')) -> h' <= h

  lemma resolve_height_relLink:
    forall d x p r h ps d' h'. resolve_with_height d (Cons (Down x) p) (Some(r, h)) ->
      lookup d x = RelLink ps -> resolve_with_height d ps (Some(d', h')) -> h' <= h

  use import set.Fset
  use import map.Map

  type lnk = (dirnode,filename)
  constant alllinks : set lnk
  axiom alllinks_in : forall d fn ps.
    lookup d fn = AbsLink ps \/ lookup d fn = RelLink ps -> mem (d,fn) alllinks

  exception Error

  let rec aux_resolve (d: dirnode) (p:path) (active:set lnk) : dirnode
    requires { subset active alllinks }
    requires { forall d1 fn ps d2.
               mem (d1, fn) active -> lookup d1 fn = AbsLink ps ->
               resolve_to root ps d2 -> exists r. resolve_to d p r}
    requires { forall d1 fn ps d2.
               mem (d1, fn) active -> lookup d1 fn = RelLink ps ->
               resolve_to d1 ps d2 -> exists r. resolve_to d p r}
    requires { forall d1 fn ps d2 h1 d' h.
               mem (d1,fn) active -> lookup d1 fn = AbsLink ps ->
               resolve_with_height root ps (Some(d2, h1)) ->
               resolve_with_height d p (Some(d', h)) -> h <= h1 }
    requires { forall d1 fn ps d2 h1 d' h.
               mem (d1,fn) active -> lookup d1 fn = RelLink ps ->
               resolve_with_height d1 ps (Some(d2, h1)) ->
               resolve_with_height d p (Some (d',h)) -> h <= h1 }
    ensures { resolve_to d p result }
    raises { Error -> forall d'. not resolve_to d p d' }
    variant { cardinal alllinks - cardinal active, p }
  = assert {exists h. resolve_with_height d p h }; (* to help provers *)
    match p with
    | Nil -> d
    | Cons Up pr -> let d' = parent d in aux_resolve d' pr active
    | Cons Here pr -> aux_resolve d pr active
    | Cons (Down fn) pr ->
      match lookup d fn with
      | Absent -> raise Error
      | Dir d' -> aux_resolve d' pr active
      | AbsLink ps ->
        if mem (d,fn) active
        then raise Error
        else begin
          let actadd = add (d,fn) active in
          let d' = aux_resolve root ps actadd in
          aux_resolve d' pr active
        end
      | RelLink ps ->
        if mem (d, fn) active
        then raise Error
        else begin
          let actadd = add (d, fn) active in
          let d' = aux_resolve d ps actadd in
          aux_resolve d' pr active
        end
      end
    end

  let resolve (d: dirnode) (p:path) : dirnode
    ensures { resolve_to d p result }
    raises { Error -> forall d2. not resolve_to d p d2 }
  = aux_resolve d p empty

end

Why3 Proof Results for Project "path_resolution"

Theory "path_resolution.FileSystem": fully verified in 25.88 s

ObligationsAlt-Ergo (1.01)CVC3 (2.4.1)CVC4 (1.4)Eprover (1.8-001)Z3 (4.4.1)
resolve_height_resolve---------------
induction_pr
  1.---------------
simplify_trivial_quantification_in_goal
  1.0.010.020.040.020.02
2.---------------
simplify_trivial_quantification_in_goal
  1.0.010.030.040.170.01
3.---------------
simplify_trivial_quantification_in_goal
  1.0.040.060.056.440.02
4.---------------
simplify_trivial_quantification_in_goal
  1.1.06Timeout (10s)0.066.100.02
5.---------------
simplify_trivial_quantification_in_goal
  1.1.00Timeout (10s)0.05Timeout (10s)0.02
6.---------------
simplify_trivial_quantification_in_goal
  1.0.030.030.040.170.02
7.---------------
simplify_trivial_quantification_in_goal
  1.0.010.020.040.160.02
resolve_height_pos---------------
induction_pr
  1.---------------
simplify_trivial_quantification_in_goal
  1.0.010.020.040.020.01
2.---------------
simplify_trivial_quantification_in_goal
  1.0.010.020.030.160.01
3.---------------
simplify_trivial_quantification_in_goal
  1.0.010.040.030.160.01
4.---------------
simplify_trivial_quantification_in_goal
  1.0.020.030.040.180.04
5.---------------
simplify_trivial_quantification_in_goal
  1.0.010.020.030.180.03
6.---------------
simplify_trivial_quantification_in_goal
  1.0.010.020.030.170.02
7.---------------
simplify_trivial_quantification_in_goal
  1.0.010.020.040.170.02
resolve_make_height---------------
induction_pr
  1.---------------
simplify_trivial_quantification_in_goal
  1.0.02Timeout (10s)4.980.06Timeout (10s)
2.---------------
simplify_trivial_quantification_in_goal
  1.0.03Timeout (10s)0.051.260.01
3.---------------
simplify_trivial_quantification_in_goal
  1.Timeout (10s)Timeout (10s)0.132.550.02
4.---------------
simplify_trivial_quantification_in_goal
  1.Timeout (10s)Timeout (10s)0.123.570.02
5.---------------
simplify_trivial_quantification_in_goal
  1.0.04Timeout (10s)0.050.170.02
6.---------------
simplify_trivial_quantification_in_goal
  1.0.020.030.050.170.01

Theory "path_resolution.POSIX_resolution": fully verified in 24.09 s

ObligationsAlt-Ergo (1.01)CVC3 (2.4.1)CVC4 (1.4)Coq (8.5pl1)Eprover (1.8-001)Z3 (4.4.1)
resolve_to_append------------------
induction_pr
  1.0.010.030.05---0.020.01
2.Timeout (10s)Timeout (10s)0.04---0.21Timeout (10s)
3.Timeout (10s)Timeout (10s)0.05---0.52Timeout (10s)
4.Timeout (10s)Timeout (10s)0.07---0.23Timeout (10s)
5.Timeout (10s)Timeout (10s)0.04---0.20Timeout (10s)
6.0.13Timeout (10s)0.05---0.20Timeout (10s)
resolve_to_consTimeout (10s)2.620.05---0.220.04
VC for resolve_to_decomp------------------
induction_pr
  1. VC for resolve_to_decomp0.010.020.07---0.020.02
2. VC for resolve_to_decompTimeout (10s)Timeout (10s)Timeout (10s)---0.26Timeout (10s)
3. VC for resolve_to_decompTimeout (10s)Timeout (10s)Timeout (10s)---0.670.04
4. VC for resolve_to_decompTimeout (10s)Timeout (10s)Timeout (10s)---0.830.04
5. VC for resolve_to_decompTimeout (10s)Timeout (10s)1.14---0.20Timeout (10s)
6. VC for resolve_to_decomp1.200.080.71---0.190.05
VC for resolve_to_decomposition------------------
induction_ty_lex
  1. VC for resolve_to_decomposition------------------
split_goal_wp
  1. postcondition0.150.030.09---0.160.03
2. postconditionTimeout (10s)Timeout (10s)7.221.61Timeout (10s)Timeout (10s)
resolve_to_POSIX_append------------------
induction_pr
  1.0.020.030.05---0.020.03
2.Timeout (10s)Timeout (10s)0.04---0.43Timeout (10s)
3.Timeout (10s)Timeout (10s)2.10---0.42Timeout (10s)
4.Timeout (10s)Timeout (10s)1.23---0.36Timeout (10s)
5.Timeout (10s)Timeout (10s)0.04---0.28Timeout (10s)
6.Timeout (10s)Timeout (10s)0.04---0.283.14
resolve_to_equivalence------------------
split_goal_wp
  1.------------------
induction_pr
  1.0.020.030.04---0.020.02
2.Timeout (10s)Timeout (10s)0.04---0.27Timeout (10s)
3.Timeout (10s)Timeout (10s)0.06---Timeout (10s)Timeout (10s)
4.Timeout (10s)Timeout (10s)0.08---Timeout (10s)Timeout (10s)
5.Timeout (10s)Timeout (10s)0.07---0.27Timeout (10s)
6.0.020.040.04---0.260.03
2.------------------
induction_pr
  1.0.020.030.04---0.030.02
2.Timeout (10s)Timeout (10s)0.04---0.28Timeout (10s)
3.Timeout (10s)Timeout (10s)0.05---0.29Timeout (10s)
4.Timeout (10s)Timeout (10s)0.05---0.31Timeout (10s)
5.Timeout (10s)Timeout (10s)0.05---0.27Timeout (10s)
6.0.020.040.03---0.260.03

Theory "path_resolution.Determinism": fully verified in 34.98 s

ObligationsAlt-Ergo (1.01)CVC3 (2.4.1)CVC4 (1.4)Eprover (1.8-001)Z3 (4.4.1)
resolve_unique---------------
induction_pr
  1.---------------
simplify_trivial_quantification_in_goal
  1.0.03Timeout (10s)7.000.17Timeout (10s)
2.---------------
simplify_trivial_quantification_in_goal
  1.Timeout (10s)0.85Timeout (10s)Timeout (10s)Timeout (10s)
3.---------------
simplify_trivial_quantification_in_goal
  1.---------------
inversion_pr
  1.0.010.020.040.020.01
2.0.010.020.040.170.02
3.Timeout (10s)0.781.630.170.07
4.0.010.020.030.170.01
5.0.010.030.040.060.02
6.0.020.060.040.060.02
4.---------------
simplify_trivial_quantification_in_goal
  1.---------------
inversion_pr
  1.0.010.020.040.020.02
2.0.010.030.040.180.02
3.0.010.020.040.180.02
4.Timeout (10s)0.061.310.180.06
5.0.010.020.040.060.02
6.0.010.070.040.060.02
5.---------------
simplify_trivial_quantification_in_goal
  1.4.080.916.28Timeout (10s)Timeout (10s)
6.---------------
simplify_trivial_quantification_in_goal
  1.3.520.314.09Timeout (10s)Timeout (10s)
resolve_with_height_unique---------------
split_goal_wp
  1.0.03Timeout (10s)Timeout (10s)Timeout (10s)Timeout (10s)
2.0.05Timeout (10s)Timeout (10s)7.87Timeout (10s)
3.---------------
induction_pr
  1.---------------
inversion_pr
  1.0.020.020.040.020.02
2.0.020.020.030.020.02
3.0.020.030.040.020.02
4.0.020.030.040.020.02
5.0.020.030.040.010.02
6.0.020.030.040.020.02
7.0.020.030.140.020.02
2.0.01Timeout (10s)Timeout (10s)0.17Timeout (10s)
3.---------------
inversion_pr
  1.0.020.030.050.020.02
2.0.020.030.040.020.02
3.Timeout (10s)Timeout (10s)0.050.24Timeout (10s)
4.0.020.030.050.240.02
5.0.020.030.050.190.02
6.0.020.020.040.180.02
7.0.020.080.040.180.02
4.---------------
inversion_pr
  1.0.020.030.040.020.02
2.0.020.030.050.020.03
3.0.020.030.060.190.02
4.Timeout (10s)Timeout (10s)0.12Timeout (10s)Timeout (10s)
5.0.020.040.050.180.02
6.0.020.030.050.190.02
7.0.020.150.050.190.02
5.---------------
inversion_pr
  1.0.020.030.050.020.02
2.0.020.030.040.020.02
3.0.020.030.050.180.02
4.0.020.030.060.180.03
5.Timeout (10s)Timeout (10s)0.13Timeout (10s)Timeout (10s)
6.0.020.030.050.110.03
7.0.020.200.050.190.02
6.---------------
inversion_pr
  1.0.020.020.040.020.02
2.0.020.020.040.020.02
3.0.020.020.050.170.03
4.0.020.030.050.180.02
5.0.020.030.050.180.02
6.Timeout (10s)Timeout (10s)0.140.20Timeout (10s)
7.0.020.080.040.180.02
7.---------------
inversion_pr
  1.0.020.030.040.020.02
2.0.020.030.040.010.02
3.0.020.080.030.170.02
4.0.020.140.050.180.02
5.0.020.140.050.180.02
6.0.020.090.040.180.03
7.Timeout (10s)Timeout (10s)0.040.21Timeout (10s)
4.0.18Timeout (10s)0.050.180.03
resolve_with_height_exists0.02Timeout (10s)0.030.17Timeout (10s)

Theory "path_resolution.Resolution": fully verified in 91.32 s

ObligationsAlt-Ergo (1.01)CVC3 (2.4.1)CVC4 (1.4)Eprover (1.8-001)Z3 (4.4.1)
resolve_height_absLinkTimeout (10s)0.18Timeout (10s)Timeout (10s)Timeout (10s)
resolve_height_relLinkTimeout (10s)0.16Timeout (10s)Timeout (10s)Timeout (10s)
VC for aux_resolve---------------
split_goal_wp
  1. assertion0.05Timeout (10s)4.740.12Timeout (10s)
2. postcondition0.010.040.060.030.03
3. variant decrease0.010.040.070.230.03
4. precondition0.010.040.060.070.03
5. precondition0.230.24Timeout (10s)Timeout (10s)Timeout (10s)
6. precondition0.210.24Timeout (10s)Timeout (10s)Timeout (10s)
7. preconditionTimeout (10s)Timeout (10s)0.14Timeout (10s)0.03
8. preconditionTimeout (10s)Timeout (10s)0.14Timeout (10s)0.04
9. postcondition0.020.040.070.080.03
10. exceptional postcondition0.110.114.76Timeout (10s)2.33
11. variant decrease0.020.040.060.220.04
12. precondition0.020.040.050.070.03
13. precondition0.190.24Timeout (10s)Timeout (10s)Timeout (10s)
14. precondition0.190.23Timeout (10s)Timeout (10s)Timeout (10s)
15. precondition2.45Timeout (10s)0.15Timeout (10s)0.03
16. precondition2.16Timeout (10s)0.14Timeout (10s)0.03
17. postcondition0.020.040.070.250.02
18. exceptional postcondition0.100.114.66Timeout (10s)2.29
19. exceptional postcondition0.040.08Timeout (10s)Timeout (10s)1.71
20. variant decrease0.020.040.060.230.04
21. precondition0.020.030.050.070.02
22. precondition0.150.28Timeout (10s)Timeout (10s)Timeout (10s)
23. precondition0.130.27Timeout (10s)Timeout (10s)Timeout (10s)
24. preconditionTimeout (10s)Timeout (10s)0.12Timeout (10s)0.03
25. preconditionTimeout (10s)Timeout (10s)0.13Timeout (10s)0.04
26. postcondition0.020.040.060.260.03
27. exceptional postcondition0.050.127.92Timeout (10s)Timeout (10s)
28. exceptional postcondition4.50Timeout (10s)Timeout (10s)Timeout (10s)Timeout (10s)
29. variant decrease0.030.050.07Timeout (10s)0.03
30. preconditionTimeout (10s)0.130.07Timeout (10s)0.02
31. precondition0.550.34Timeout (10s)Timeout (10s)Timeout (10s)
32. precondition0.450.37Timeout (10s)Timeout (10s)Timeout (10s)
33. precondition8.17Timeout (10s)Timeout (10s)Timeout (10s)Timeout (10s)
34. precondition3.90Timeout (10s)Timeout (10s)Timeout (10s)Timeout (10s)
35. variant decrease0.030.050.070.24Timeout (10s)
36. precondition0.020.040.050.080.02
37. preconditionTimeout (10s)1.65Timeout (10s)Timeout (10s)Timeout (10s)
38. preconditionTimeout (10s)1.81Timeout (10s)Timeout (10s)Timeout (10s)
39. preconditionTimeout (10s)Timeout (10s)2.37Timeout (10s)4.80
40. preconditionTimeout (10s)Timeout (10s)2.35Timeout (10s)1.46
41. postcondition0.03Timeout (10s)0.07Timeout (10s)0.03
42. exceptional postconditionTimeout (10s)0.96Timeout (10s)Timeout (10s)Timeout (10s)
43. exceptional postcondition0.050.24Timeout (10s)Timeout (10s)Timeout (10s)
44. exceptional postcondition1.62Timeout (10s)Timeout (10s)Timeout (10s)6.25
45. variant decrease0.030.040.07Timeout (10s)0.03
46. precondition0.03Timeout (10s)4.79Timeout (10s)Timeout (10s)
47. precondition0.480.31Timeout (10s)Timeout (10s)Timeout (10s)
48. precondition0.470.316.07Timeout (10s)Timeout (10s)
49. precondition4.27Timeout (10s)Timeout (10s)Timeout (10s)Timeout (10s)
50. precondition7.45Timeout (10s)Timeout (10s)Timeout (10s)Timeout (10s)
51. variant decrease0.030.040.080.250.30
52. precondition0.020.040.060.070.03
53. preconditionTimeout (10s)1.92Timeout (10s)Timeout (10s)Timeout (10s)
54. preconditionTimeout (10s)2.89Timeout (10s)Timeout (10s)Timeout (10s)
55. preconditionTimeout (10s)Timeout (10s)2.04Timeout (10s)3.09
56. preconditionTimeout (10s)Timeout (10s)1.73Timeout (10s)0.47
57. postcondition0.03Timeout (10s)0.080.290.02
58. exceptional postconditionTimeout (10s)0.94Timeout (10s)Timeout (10s)Timeout (10s)
59. exceptional postcondition0.160.23Timeout (10s)Timeout (10s)Timeout (10s)
VC for resolve---------------
split_goal_wp
  1. precondition0.030.030.060.210.03
2. precondition0.020.040.050.020.02
3. precondition0.010.040.060.020.02
4. precondition0.030.040.050.020.03
5. precondition0.030.030.060.030.03
6. postcondition0.030.030.050.030.01
7. exceptional postcondition0.030.040.070.030.00