heap_lang.ref 3.94 KB
Newer Older
1 2 3
1 subgoal
  
  Σ : gFunctors
4
  heapG0 : heapG Σ
5 6 7 8 9 10 11 12
  E : coPset
  ============================
  --------------------------------------∗
  WP let: "x" := ref #1 in "x" <- ! "x" + #1;; ! "x" @ E {{ v, ⌜v = #2⌝ }}
  
1 subgoal
  
  Σ : gFunctors
13
  heapG0 : heapG Σ
14 15 16 17 18 19 20
  E : coPset
  l : loc
  ============================
  _ : l ↦ #1
  --------------------------------------∗
  WP #l <- #1 + #1;; ! #l @ E {{ v, ⌜v = #2⌝ }}
  
21 22 23
1 subgoal
  
  Σ : gFunctors
24
  heapG0 : heapG Σ
25 26 27 28 29 30 31 32
  E : coPset
  l : loc
  ============================
  "Hl" : l ↦ #1
  --------------------------------------∗
  WP let: "x" := #l in let: "y" := ref #1 in "x" <- ! "x" + #1;; ! "x"
  @ E [{ v, ⌜v = #2⌝ }]
  
33 34 35 36 37
"heap_e7_spec"
     : string
1 subgoal
  
  Σ : gFunctors
38
  heapG0 : heapG Σ
39 40 41 42
  l : loc
  ============================
  _ : ▷ l ↦ #0
  --------------------------------------∗
43
  WP CmpXchg #l #0 #1 {{ _, l ↦ #1 }}
44 45 46 47
  
1 subgoal
  
  Σ : gFunctors
48
  heapG0 : heapG Σ
49 50 51 52 53 54
  l : loc
  ============================
  _ : l ↦ #1
  --------------------------------------∗
  l ↦ #1
  
Ralf Jung's avatar
Ralf Jung committed
55 56 57
1 subgoal
  
  Σ : gFunctors
58
  heapG0 : heapG Σ
Ralf Jung's avatar
Ralf Jung committed
59 60 61 62 63 64 65 66 67 68
  l : loc
  ============================
  "Hl1" : l ↦{1 / 2} #0
  "Hl2" : l ↦{1 / 2} #0
  --------------------------------------∗
  True
  
1 subgoal
  
  Σ : gFunctors
69
  heapG0 : heapG Σ
Ralf Jung's avatar
Ralf Jung committed
70 71 72 73 74
  l : loc
  ============================
  --------------------------------------∗
  True
  
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
75 76
"wp_nonclosed_value"
     : string
77 78 79 80 81 82 83
The command has indeed failed with message:
Ltac call to "wp_pure (open_constr)" failed.
Tactic failure: wp_pure: cannot find ?y in (Var "x") or 
?y is not a redex.
1 subgoal
  
  Σ : gFunctors
84
  heapG0 : heapG Σ
85 86 87 88
  ============================
  --------------------------------------∗
  WP "x" {{ _, True }}
  
89 90 91 92 93 94 95 96 97 98
The command has indeed failed with message:
In nested Ltac calls to "iIntros (constr)", "iIntros_go",
"iDestructHyp (constr) as (constr)",
"<iris.proofmode.ltac_tactics.iDestructHypFindPat>",
"<iris.proofmode.ltac_tactics.iDestructHypGo>" and
"iAndDestruct (constr) as (constr) (constr)", last call failed.
Tactic failure: iAndDestruct: cannot destruct (l ↦∗ (vs1 ++ vs2))%I.
The command has indeed failed with message:
Ltac call to "iSplitL (constr)" failed.
Tactic failure: iSplitL: (l ↦∗ (vs1 ++ vs2))%I not a separating conjunction.
99 100 101 102 103 104 105 106
1 subgoal
  
  Σ : gFunctors
  heapG0 : heapG Σ
  ============================
  --------------------------------------∗
  WP let: "f" := λ: "x", "x" in ref ("f" #10) {{ _, True }}
  
107 108 109
1 subgoal
  
  Σ : gFunctors
110
  heapG0 : heapG Σ
111 112 113 114 115 116 117 118
  fun1, fun2, fun3 : expr
  ============================
  --------------------------------------∗
  WP let: "val1" := fun1 #() in
     let: "val2" := fun2 "val1" in
     let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
  {{ _, True }}
  
119 120 121
1 subgoal
  
  Σ : gFunctors
122
  heapG0 : heapG Σ
123
  fun1, fun2, fun3 : expr
124
  Φ : language.val heap_lang → iPropI Σ
125 126 127 128 129 130 131 132 133 134
  ============================
  --------------------------------------∗
  WP let: "val1" := fun1 #() in
     let: "val2" := fun2 "val1" in
     let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v" 
  {{ v, Φ v }}
  
1 subgoal
  
  Σ : gFunctors
135
  heapG0 : heapG Σ
136
  fun1, fun2, fun3 : expr
137
  Φ : language.val heap_lang → iPropI Σ
138 139 140 141 142 143 144 145
  E : coPset
  ============================
  --------------------------------------∗
  WP let: "val1" := fun1 #() in
     let: "val2" := fun2 "val1" in
     let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v" 
  @ E {{ v, Φ v }}
  
146 147 148
1 subgoal
  
  Σ : gFunctors
149
  heapG0 : heapG Σ
150 151 152 153 154 155 156
  fun1, fun2, fun3 : expr
  ============================
  {{{ True }}}
    let: "val1" := fun1 #() in
    let: "val2" := fun2 "val1" in
    let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
  {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}
157
"not_cmpxchg"
158 159
     : string
The command has indeed failed with message:
160 161
Ltac call to "wp_cmpxchg_suc" failed.
Tactic failure: wp_cmpxchg_suc: cannot find 'CmpXchg' in 
162
(#() #()).