Commit d95e8b34 authored by Rodolphe Lepigre's avatar Rodolphe Lepigre Committed by Michael Sammler
Browse files

Ensure variable names do not clash with Coq keywords.

This fixes the third point of #30.
parent 468275c3
Pipeline #39335 passed with stage
in 14 minutes and 54 seconds
......@@ -339,7 +339,7 @@ Section code.
|}.
(* Definition of function [test]. *)
Definition impl_test (alloc binary_search compare_int free : loc): function := {|
Definition impl_test (global_alloc global_binary_search global_compare_int global_free : loc): function := {|
f_args := [
];
f_local_vars := [
......@@ -351,31 +351,31 @@ Section code.
f_code := (
<[ "#0" :=
locinfo: loc_248 ;
"$5" <- LocInfoE loc_250 (alloc) with
"$5" <- LocInfoE loc_250 (global_alloc) with
[ LocInfoE loc_251 (i2v (it_layout size_t).(ly_size) size_t) ] ;
locinfo: loc_85 ;
LocInfoE loc_244 ((LocInfoE loc_246 ("ptrs")) at_offset{LPtr, PtrOp, IntOp i32} (LocInfoE loc_247 (i2v 0 i32))) <-{ LPtr }
LocInfoE loc_248 ("$5") ;
locinfo: loc_239 ;
"$4" <- LocInfoE loc_241 (alloc) with
"$4" <- LocInfoE loc_241 (global_alloc) with
[ LocInfoE loc_242 (i2v (it_layout size_t).(ly_size) size_t) ] ;
locinfo: loc_86 ;
LocInfoE loc_235 ((LocInfoE loc_237 ("ptrs")) at_offset{LPtr, PtrOp, IntOp i32} (LocInfoE loc_238 (i2v 1 i32))) <-{ LPtr }
LocInfoE loc_239 ("$4") ;
locinfo: loc_230 ;
"$3" <- LocInfoE loc_232 (alloc) with
"$3" <- LocInfoE loc_232 (global_alloc) with
[ LocInfoE loc_233 (i2v (it_layout size_t).(ly_size) size_t) ] ;
locinfo: loc_87 ;
LocInfoE loc_226 ((LocInfoE loc_228 ("ptrs")) at_offset{LPtr, PtrOp, IntOp i32} (LocInfoE loc_229 (i2v 2 i32))) <-{ LPtr }
LocInfoE loc_230 ("$3") ;
locinfo: loc_221 ;
"$2" <- LocInfoE loc_223 (alloc) with
"$2" <- LocInfoE loc_223 (global_alloc) with
[ LocInfoE loc_224 (i2v (it_layout size_t).(ly_size) size_t) ] ;
locinfo: loc_88 ;
LocInfoE loc_217 ((LocInfoE loc_219 ("ptrs")) at_offset{LPtr, PtrOp, IntOp i32} (LocInfoE loc_220 (i2v 3 i32))) <-{ LPtr }
LocInfoE loc_221 ("$2") ;
locinfo: loc_212 ;
"$1" <- LocInfoE loc_214 (alloc) with
"$1" <- LocInfoE loc_214 (global_alloc) with
[ LocInfoE loc_215 (i2v (it_layout size_t).(ly_size) size_t) ] ;
locinfo: loc_89 ;
LocInfoE loc_208 ((LocInfoE loc_210 ("ptrs")) at_offset{LPtr, PtrOp, IntOp i32} (LocInfoE loc_211 (i2v 4 i32))) <-{ LPtr }
......@@ -398,8 +398,8 @@ Section code.
"needle" <-{ it_layout size_t }
LocInfoE loc_164 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_164 (i2v 2 i32))) ;
locinfo: loc_152 ;
"$0" <- LocInfoE loc_154 (binary_search) with
[ LocInfoE loc_155 (compare_int) ;
"$0" <- LocInfoE loc_154 (global_binary_search) with
[ LocInfoE loc_155 (global_compare_int) ;
LocInfoE loc_156 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_157 (&(LocInfoE loc_158 ("ptrs"))))) ;
LocInfoE loc_159 (i2v 5 i32) ;
LocInfoE loc_160 (&(LocInfoE loc_161 ("needle"))) ] ;
......@@ -407,23 +407,23 @@ Section code.
locinfo: loc_97 ;
assert: (LocInfoE loc_148 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_148 ((LocInfoE loc_149 (use{it_layout i32} (LocInfoE loc_150 ("res")))) ={IntOp i32, IntOp i32} (LocInfoE loc_151 (i2v 3 i32)))))) ;
locinfo: loc_98 ;
"_" <- LocInfoE loc_140 (free) with
"_" <- LocInfoE loc_140 (global_free) with
[ LocInfoE loc_141 (i2v (it_layout size_t).(ly_size) size_t) ;
LocInfoE loc_142 (use{LPtr} (LocInfoE loc_144 ((LocInfoE loc_146 ("ptrs")) at_offset{LPtr, PtrOp, IntOp i32} (LocInfoE loc_147 (i2v 0 i32))))) ] ;
locinfo: loc_99 ;
"_" <- LocInfoE loc_131 (free) with
"_" <- LocInfoE loc_131 (global_free) with
[ LocInfoE loc_132 (i2v (it_layout size_t).(ly_size) size_t) ;
LocInfoE loc_133 (use{LPtr} (LocInfoE loc_135 ((LocInfoE loc_137 ("ptrs")) at_offset{LPtr, PtrOp, IntOp i32} (LocInfoE loc_138 (i2v 1 i32))))) ] ;
locinfo: loc_100 ;
"_" <- LocInfoE loc_122 (free) with
"_" <- LocInfoE loc_122 (global_free) with
[ LocInfoE loc_123 (i2v (it_layout size_t).(ly_size) size_t) ;
LocInfoE loc_124 (use{LPtr} (LocInfoE loc_126 ((LocInfoE loc_128 ("ptrs")) at_offset{LPtr, PtrOp, IntOp i32} (LocInfoE loc_129 (i2v 2 i32))))) ] ;
locinfo: loc_101 ;
"_" <- LocInfoE loc_113 (free) with
"_" <- LocInfoE loc_113 (global_free) with
[ LocInfoE loc_114 (i2v (it_layout size_t).(ly_size) size_t) ;
LocInfoE loc_115 (use{LPtr} (LocInfoE loc_117 ((LocInfoE loc_119 ("ptrs")) at_offset{LPtr, PtrOp, IntOp i32} (LocInfoE loc_120 (i2v 3 i32))))) ] ;
locinfo: loc_102 ;
"_" <- LocInfoE loc_104 (free) with
"_" <- LocInfoE loc_104 (global_free) with
[ LocInfoE loc_105 (i2v (it_layout size_t).(ly_size) size_t) ;
LocInfoE loc_106 (use{LPtr} (LocInfoE loc_108 ((LocInfoE loc_110 ("ptrs")) at_offset{LPtr, PtrOp, IntOp i32} (LocInfoE loc_111 (i2v 4 i32))))) ] ;
Return (VOID)
......
......@@ -9,12 +9,12 @@ Section proof_test.
Context `{!typeG Σ} `{!globalG Σ}.
(* Typing proof for [test]. *)
Lemma type_test (alloc binary_search compare_int free : loc) :
alloc ◁ᵥ alloc @ function_ptr type_of_alloc -
binary_search ◁ᵥ binary_search @ function_ptr type_of_binary_search -
compare_int ◁ᵥ compare_int @ function_ptr type_of_compare_int -
free ◁ᵥ free @ function_ptr type_of_free -
typed_function (impl_test alloc binary_search compare_int free) type_of_test.
Lemma type_test (global_alloc global_binary_search global_compare_int global_free : loc) :
global_alloc ◁ᵥ global_alloc @ function_ptr type_of_alloc -
global_binary_search ◁ᵥ global_binary_search @ function_ptr type_of_binary_search -
global_compare_int ◁ᵥ global_compare_int @ function_ptr type_of_compare_int -
global_free ◁ᵥ global_free @ function_ptr type_of_free -
typed_function (impl_test global_alloc global_binary_search global_compare_int global_free) type_of_test.
Proof.
start_function "test" ([]) => local_res local_ptrs local_needle.
split_blocks ((
......
......@@ -1573,7 +1573,7 @@ Section code.
Solve Obligations with solve_struct_obligations.
(* Definition of function [new_btree]. *)
Definition impl_new_btree (alloc : loc): function := {|
Definition impl_new_btree (global_alloc : loc): function := {|
f_args := [
];
f_local_vars := [
......@@ -1583,7 +1583,7 @@ Section code.
f_code := (
<[ "#0" :=
locinfo: loc_11 ;
"$0" <- LocInfoE loc_13 (alloc) with
"$0" <- LocInfoE loc_13 (global_alloc) with
[ LocInfoE loc_14 (i2v (LPtr).(ly_size) size_t) ] ;
"t" <-{ LPtr }
LocInfoE loc_11 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_11 ("$0"))) ;
......@@ -1597,7 +1597,7 @@ Section code.
|}.
(* Definition of function [free_btree]. *)
Definition impl_free_btree (free free_btree_nodes : loc): function := {|
Definition impl_free_btree (global_free global_free_btree_nodes : loc): function := {|
f_args := [
("t", LPtr)
];
......@@ -1607,10 +1607,10 @@ Section code.
f_code := (
<[ "#0" :=
locinfo: loc_19 ;
"_" <- LocInfoE loc_27 (free_btree_nodes) with
"_" <- LocInfoE loc_27 (global_free_btree_nodes) with
[ LocInfoE loc_28 (use{LPtr} (LocInfoE loc_29 ("t"))) ] ;
locinfo: loc_20 ;
"_" <- LocInfoE loc_22 (free) with
"_" <- LocInfoE loc_22 (global_free) with
[ LocInfoE loc_23 (i2v (LPtr).(ly_size) size_t) ;
LocInfoE loc_24 (use{LPtr} (LocInfoE loc_25 ("t"))) ] ;
Return (VOID)
......@@ -1619,7 +1619,7 @@ Section code.
|}.
(* Definition of function [btree_member]. *)
Definition impl_btree_member (key_index : loc): function := {|
Definition impl_btree_member (global_key_index : loc): function := {|
f_args := [
("t", LPtr);
("k", it_layout i32)
......@@ -1650,7 +1650,7 @@ Section code.
]> $
<[ "#2" :=
locinfo: loc_84 ;
"$0" <- LocInfoE loc_86 (key_index) with
"$0" <- LocInfoE loc_86 (global_key_index) with
[ LocInfoE loc_87 (&(LocInfoE loc_88 ((LocInfoE loc_89 (!{LPtr} (LocInfoE loc_91 (!{LPtr} (LocInfoE loc_92 ("cur")))))) at{struct_btree} "keys"))) ;
LocInfoE loc_93 (use{it_layout i32} (LocInfoE loc_94 ((LocInfoE loc_95 (!{LPtr} (LocInfoE loc_97 (!{LPtr} (LocInfoE loc_98 ("cur")))))) at{struct_btree} "nb_keys"))) ;
LocInfoE loc_99 (use{it_layout i32} (LocInfoE loc_100 ("k"))) ] ;
......@@ -1700,7 +1700,7 @@ Section code.
|}.
(* Definition of function [btree_find]. *)
Definition impl_btree_find (key_index : loc): function := {|
Definition impl_btree_find (global_key_index : loc): function := {|
f_args := [
("t", LPtr);
("k", it_layout i32)
......@@ -1729,7 +1729,7 @@ Section code.
]> $
<[ "#2" :=
locinfo: loc_181 ;
"$0" <- LocInfoE loc_183 (key_index) with
"$0" <- LocInfoE loc_183 (global_key_index) with
[ LocInfoE loc_184 (&(LocInfoE loc_185 ((LocInfoE loc_186 (!{LPtr} (LocInfoE loc_188 (!{LPtr} (LocInfoE loc_189 ("cur")))))) at{struct_btree} "keys"))) ;
LocInfoE loc_190 (use{it_layout i32} (LocInfoE loc_191 ((LocInfoE loc_192 (!{LPtr} (LocInfoE loc_194 (!{LPtr} (LocInfoE loc_195 ("cur")))))) at{struct_btree} "nb_keys"))) ;
LocInfoE loc_196 (use{it_layout i32} (LocInfoE loc_197 ("k"))) ] ;
......@@ -1779,7 +1779,7 @@ Section code.
|}.
(* Definition of function [btree_insert]. *)
Definition impl_btree_insert (alloc btree_make_root free insert_br key_index : loc): function := {|
Definition impl_btree_insert (global_alloc global_btree_make_root global_free global_insert_br global_key_index : loc): function := {|
f_args := [
("t", LPtr);
("k", it_layout i32);
......@@ -1813,12 +1813,12 @@ Section code.
]> $
<[ "#1" :=
locinfo: loc_479 ;
"$4" <- LocInfoE loc_481 (alloc) with
"$4" <- LocInfoE loc_481 (global_alloc) with
[ LocInfoE loc_482 ((LocInfoE loc_483 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_483 ((LocInfoE loc_484 (use{it_layout i32} (LocInfoE loc_485 ((LocInfoE loc_486 (!{LPtr} (LocInfoE loc_488 (!{LPtr} (LocInfoE loc_489 ("t")))))) at{struct_btree} "height")))) +{IntOp i32, IntOp i32} (LocInfoE loc_490 (i2v 1 i32)))))) ×{IntOp size_t, IntOp size_t} (LocInfoE loc_491 (i2v (LPtr).(ly_size) size_t))) ] ;
"path_ptrs" <-{ LPtr }
LocInfoE loc_479 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_479 ("$4"))) ;
locinfo: loc_466 ;
"$3" <- LocInfoE loc_468 (alloc) with
"$3" <- LocInfoE loc_468 (global_alloc) with
[ LocInfoE loc_469 ((LocInfoE loc_470 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_470 (use{it_layout i32} (LocInfoE loc_471 ((LocInfoE loc_472 (!{LPtr} (LocInfoE loc_474 (!{LPtr} (LocInfoE loc_475 ("t")))))) at{struct_btree} "height")))))) ×{IntOp size_t, IntOp size_t} (LocInfoE loc_476 (i2v (it_layout i32).(ly_size) size_t))) ] ;
"path_keys" <-{ LPtr }
LocInfoE loc_466 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_466 ("$3"))) ;
......@@ -1869,7 +1869,7 @@ Section code.
]> $
<[ "#15" :=
locinfo: loc_501 ;
"$5" <- LocInfoE loc_503 (btree_make_root) with
"$5" <- LocInfoE loc_503 (global_btree_make_root) with
[ LocInfoE loc_504 (NULL) ; LocInfoE loc_505 (NULL) ;
LocInfoE loc_506 (use{it_layout i32} (LocInfoE loc_507 ("k"))) ;
LocInfoE loc_508 (use{LPtr} (LocInfoE loc_509 ("v"))) ] ;
......@@ -1895,7 +1895,7 @@ Section code.
"cur_node" <-{ LPtr }
LocInfoE loc_434 (use{LPtr} (LocInfoE loc_436 ((LocInfoE loc_437 (!{LPtr} (LocInfoE loc_438 ("path_ptrs")))) at_offset{LPtr, PtrOp, IntOp i32} (LocInfoE loc_439 (use{it_layout i32} (LocInfoE loc_440 ("cur"))))))) ;
locinfo: loc_415 ;
"$2" <- LocInfoE loc_417 (key_index) with
"$2" <- LocInfoE loc_417 (global_key_index) with
[ LocInfoE loc_418 (&(LocInfoE loc_419 ((LocInfoE loc_420 (!{LPtr} (LocInfoE loc_422 (!{LPtr} (LocInfoE loc_423 ("cur_node")))))) at{struct_btree} "keys"))) ;
LocInfoE loc_424 (use{it_layout i32} (LocInfoE loc_425 ((LocInfoE loc_426 (!{LPtr} (LocInfoE loc_428 (!{LPtr} (LocInfoE loc_429 ("cur_node")))))) at{struct_btree} "nb_keys"))) ;
LocInfoE loc_430 (use{it_layout i32} (LocInfoE loc_431 ("k"))) ] ;
......@@ -1931,7 +1931,7 @@ Section code.
"node" <-{ LPtr }
LocInfoE loc_313 (use{LPtr} (LocInfoE loc_315 ((LocInfoE loc_316 (!{LPtr} (LocInfoE loc_317 ("path_ptrs")))) at_offset{LPtr, PtrOp, IntOp i32} (LocInfoE loc_318 ((LocInfoE loc_319 (use{it_layout i32} (LocInfoE loc_320 ("cur")))) -{IntOp i32, IntOp i32} (LocInfoE loc_321 (i2v 1 i32))))))) ;
locinfo: loc_298 ;
"$1" <- LocInfoE loc_300 (insert_br) with
"$1" <- LocInfoE loc_300 (global_insert_br) with
[ LocInfoE loc_301 (use{LPtr} (LocInfoE loc_302 ("node"))) ;
LocInfoE loc_303 (use{it_layout i32} (LocInfoE loc_304 ("ins_k"))) ;
LocInfoE loc_305 (use{LPtr} (LocInfoE loc_306 ("ins_v"))) ;
......@@ -1951,7 +1951,7 @@ Section code.
]> $
<[ "#7" :=
locinfo: loc_257 ;
"$0" <- LocInfoE loc_259 (btree_make_root) with
"$0" <- LocInfoE loc_259 (global_btree_make_root) with
[ LocInfoE loc_260 (use{LPtr} (LocInfoE loc_262 (!{LPtr} (LocInfoE loc_263 ("t"))))) ;
LocInfoE loc_264 (use{LPtr} (LocInfoE loc_265 ("new"))) ;
LocInfoE loc_266 (use{it_layout i32} (LocInfoE loc_267 ("med_k"))) ;
......@@ -1992,11 +1992,11 @@ Section code.
]> $
<[ "done" :=
locinfo: loc_226 ;
"_" <- LocInfoE loc_241 (free) with
"_" <- LocInfoE loc_241 (global_free) with
[ LocInfoE loc_242 ((LocInfoE loc_243 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_243 ((LocInfoE loc_244 (use{it_layout i32} (LocInfoE loc_245 ((LocInfoE loc_246 (!{LPtr} (LocInfoE loc_248 (!{LPtr} (LocInfoE loc_249 ("t")))))) at{struct_btree} "height")))) +{IntOp i32, IntOp i32} (LocInfoE loc_250 (i2v 1 i32)))))) ×{IntOp size_t, IntOp size_t} (LocInfoE loc_251 (i2v (LPtr).(ly_size) size_t))) ;
LocInfoE loc_252 (use{LPtr} (LocInfoE loc_253 ("path_ptrs"))) ] ;
locinfo: loc_227 ;
"_" <- LocInfoE loc_229 (free) with
"_" <- LocInfoE loc_229 (global_free) with
[ LocInfoE loc_230 ((LocInfoE loc_231 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_231 (use{it_layout i32} (LocInfoE loc_232 ((LocInfoE loc_233 (!{LPtr} (LocInfoE loc_235 (!{LPtr} (LocInfoE loc_236 ("t")))))) at{struct_btree} "height")))))) ×{IntOp size_t, IntOp size_t} (LocInfoE loc_237 (i2v (it_layout i32).(ly_size) size_t))) ;
LocInfoE loc_238 (use{LPtr} (LocInfoE loc_239 ("path_keys"))) ] ;
Return (VOID)
......@@ -2005,7 +2005,7 @@ Section code.
|}.
(* Definition of function [free_btree_nodes]. *)
Definition impl_free_btree_nodes (free free_btree_nodes : loc): function := {|
Definition impl_free_btree_nodes (global_free global_free_btree_nodes : loc): function := {|
f_args := [
("t", LPtr)
];
......@@ -2040,14 +2040,14 @@ Section code.
]> $
<[ "#3" :=
locinfo: loc_537 ;
"_" <- LocInfoE loc_542 (free_btree_nodes) with
"_" <- LocInfoE loc_542 (global_free_btree_nodes) with
[ LocInfoE loc_543 (&(LocInfoE loc_545 ((LocInfoE loc_547 ((LocInfoE loc_548 (!{LPtr} (LocInfoE loc_550 (!{LPtr} (LocInfoE loc_551 ("t")))))) at{struct_btree} "children")) at_offset{LPtr, PtrOp, IntOp i32} (LocInfoE loc_552 (use{it_layout i32} (LocInfoE loc_553 ("i"))))))) ] ;
locinfo: loc_538 ;
Goto "continue4"
]> $
<[ "#4" :=
locinfo: loc_523 ;
"_" <- LocInfoE loc_530 (free) with
"_" <- LocInfoE loc_530 (global_free) with
[ LocInfoE loc_531 (i2v (layout_of struct_btree).(ly_size) size_t) ;
LocInfoE loc_532 (use{LPtr} (LocInfoE loc_534 (!{LPtr} (LocInfoE loc_535 ("t"))))) ] ;
locinfo: loc_524 ;
......@@ -2126,7 +2126,7 @@ Section code.
|}.
(* Definition of function [insert_br]. *)
Definition impl_insert_br (alloc key_index : loc): function := {|
Definition impl_insert_br (global_alloc global_key_index : loc): function := {|
f_args := [
("node", LPtr);
("k", it_layout i32);
......@@ -2148,7 +2148,7 @@ Section code.
"n" <-{ it_layout i32 }
LocInfoE loc_1530 (use{it_layout i32} (LocInfoE loc_1531 ((LocInfoE loc_1532 (!{LPtr} (LocInfoE loc_1534 (!{LPtr} (LocInfoE loc_1535 ("node")))))) at{struct_btree} "nb_keys"))) ;
locinfo: loc_1515 ;
"$1" <- LocInfoE loc_1517 (key_index) with
"$1" <- LocInfoE loc_1517 (global_key_index) with
[ LocInfoE loc_1518 (&(LocInfoE loc_1519 ((LocInfoE loc_1520 (!{LPtr} (LocInfoE loc_1522 (!{LPtr} (LocInfoE loc_1523 ("node")))))) at{struct_btree} "keys"))) ;
LocInfoE loc_1524 (use{it_layout i32} (LocInfoE loc_1525 ("n"))) ;
LocInfoE loc_1526 (use{it_layout i32} (LocInfoE loc_1527 ("k"))) ] ;
......@@ -2164,7 +2164,7 @@ Section code.
]> $
<[ "#1" :=
locinfo: loc_1362 ;
"$0" <- LocInfoE loc_1364 (alloc) with
"$0" <- LocInfoE loc_1364 (global_alloc) with
[ LocInfoE loc_1365 (i2v (layout_of struct_btree).(ly_size) size_t) ] ;
"new_node" <-{ LPtr }
LocInfoE loc_1362 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_1362 ("$0"))) ;
......@@ -2521,7 +2521,7 @@ Section code.
|}.
(* Definition of function [btree_make_root]. *)
Definition impl_btree_make_root (alloc : loc): function := {|
Definition impl_btree_make_root (global_alloc : loc): function := {|
f_args := [
("l", LPtr);
("r", LPtr);
......@@ -2535,7 +2535,7 @@ Section code.
f_code := (
<[ "#0" :=
locinfo: loc_1621 ;
"$0" <- LocInfoE loc_1623 (alloc) with
"$0" <- LocInfoE loc_1623 (global_alloc) with
[ LocInfoE loc_1624 (i2v (layout_of struct_btree).(ly_size) size_t) ] ;
"root" <-{ LPtr }
LocInfoE loc_1621 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_1621 ("$0"))) ;
......
......@@ -10,9 +10,9 @@ Section proof_btree_member.
Context `{!typeG Σ} `{!globalG Σ}.
(* Typing proof for [btree_member]. *)
Lemma type_btree_member (key_index : loc) :
key_index ◁ᵥ key_index @ function_ptr type_of_key_index -
typed_function (impl_btree_member key_index) type_of_btree_member.
Lemma type_btree_member (global_key_index : loc) :
global_key_index ◁ᵥ global_key_index @ function_ptr type_of_key_index -
typed_function (impl_btree_member global_key_index) type_of_btree_member.
Proof.
start_function "btree_member" ([[[p h] m] k]) => arg_t arg_k local_i local_cur.
split_blocks ((
......
......@@ -10,10 +10,10 @@ Section proof_free_btree.
Context `{!typeG Σ} `{!globalG Σ}.
(* Typing proof for [free_btree]. *)
Lemma type_free_btree (free free_btree_nodes : loc) :
free ◁ᵥ free @ function_ptr type_of_free -
free_btree_nodes ◁ᵥ free_btree_nodes @ function_ptr type_of_free_btree_nodes -
typed_function (impl_free_btree free free_btree_nodes) type_of_free_btree.
Lemma type_free_btree (global_free global_free_btree_nodes : loc) :
global_free ◁ᵥ global_free @ function_ptr type_of_free -
global_free_btree_nodes ◁ᵥ global_free_btree_nodes @ function_ptr type_of_free_btree_nodes -
typed_function (impl_free_btree global_free global_free_btree_nodes) type_of_free_btree.
Proof.
start_function "free_btree" ([]) => arg_t.
split_blocks ((
......
......@@ -10,9 +10,9 @@ Section proof_new_btree.
Context `{!typeG Σ} `{!globalG Σ}.
(* Typing proof for [new_btree]. *)
Lemma type_new_btree (alloc : loc) :
alloc ◁ᵥ alloc @ function_ptr type_of_alloc -
typed_function (impl_new_btree alloc) type_of_new_btree.
Lemma type_new_btree (global_alloc : loc) :
global_alloc ◁ᵥ global_alloc @ function_ptr type_of_alloc -
typed_function (impl_new_btree global_alloc) type_of_new_btree.
Proof.
start_function "new_btree" ([]) => local_t.
split_blocks ((
......
......@@ -203,7 +203,7 @@ Section code.
Solve Obligations with solve_struct_obligations.
(* Definition of function [init]. *)
Definition impl_init (sl_init : loc): function := {|
Definition impl_init (global_sl_init : loc): function := {|
f_args := [
("t", LPtr)
];
......@@ -225,7 +225,7 @@ Section code.
LocInfoE loc_13 ((LocInfoE loc_14 ((LocInfoE loc_15 (!{LPtr} (LocInfoE loc_16 ("t")))) at{struct_lock_test} "locked_struct")) at{struct_lock_test_inner} "b") <-{ it_layout size_t }
LocInfoE loc_17 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_17 (i2v 10 i32))) ;
locinfo: loc_6 ;
"_" <- LocInfoE loc_8 (sl_init) with
"_" <- LocInfoE loc_8 (global_sl_init) with
[ LocInfoE loc_9 (&(LocInfoE loc_10 ((LocInfoE loc_11 (!{LPtr} (LocInfoE loc_12 ("t")))) at{struct_lock_test} "lock"))) ] ;
Return (VOID)
]> $
......@@ -268,7 +268,7 @@ Section code.
|}.
(* Definition of function [write_locked]. *)
Definition impl_write_locked (sl_lock sl_unlock : loc): function := {|
Definition impl_write_locked (global_sl_lock global_sl_unlock : loc): function := {|
f_args := [
("t", LPtr);
("n", it_layout size_t)
......@@ -279,7 +279,7 @@ Section code.
f_code := (
<[ "#0" :=
locinfo: loc_48 ;
"_" <- LocInfoE loc_69 (sl_lock) with
"_" <- LocInfoE loc_69 (global_sl_lock) with
[ LocInfoE loc_70 (&(LocInfoE loc_71 ((LocInfoE loc_72 (!{LPtr} (LocInfoE loc_73 ("t")))) at{struct_lock_test} "lock"))) ] ;
locinfo: loc_49 ;
annot: (UnlockA) ;
......@@ -288,7 +288,7 @@ Section code.
LocInfoE loc_59 ((LocInfoE loc_60 (!{LPtr} (LocInfoE loc_61 ("t")))) at{struct_lock_test} "locked_int") <-{ it_layout size_t }
LocInfoE loc_62 (use{it_layout size_t} (LocInfoE loc_63 ("n"))) ;
locinfo: loc_52 ;
"_" <- LocInfoE loc_54 (sl_unlock) with
"_" <- LocInfoE loc_54 (global_sl_unlock) with
[ LocInfoE loc_55 (AnnotExpr 1%nat LockA (LocInfoE loc_55 (&(LocInfoE loc_56 ((LocInfoE loc_57 (!{LPtr} (LocInfoE loc_58 ("t")))) at{struct_lock_test} "lock"))))) ] ;
Return (VOID)
]> $
......@@ -296,7 +296,7 @@ Section code.
|}.
(* Definition of function [read_locked]. *)
Definition impl_read_locked (sl_lock sl_unlock : loc): function := {|
Definition impl_read_locked (global_sl_lock global_sl_unlock : loc): function := {|
f_args := [
("t", LPtr)
];
......@@ -307,7 +307,7 @@ Section code.
f_code := (
<[ "#0" :=
locinfo: loc_76 ;
"_" <- LocInfoE loc_101 (sl_lock) with
"_" <- LocInfoE loc_101 (global_sl_lock) with
[ LocInfoE loc_102 (&(LocInfoE loc_103 ((LocInfoE loc_104 (!{LPtr} (LocInfoE loc_105 ("t")))) at{struct_lock_test} "lock"))) ] ;
locinfo: loc_77 ;
annot: (UnlockA) ;
......@@ -315,7 +315,7 @@ Section code.
"ret" <-{ it_layout size_t }
LocInfoE loc_90 (use{it_layout size_t} (LocInfoE loc_91 ((LocInfoE loc_92 (!{LPtr} (LocInfoE loc_93 ("t")))) at{struct_lock_test} "locked_int"))) ;
locinfo: loc_80 ;
"_" <- LocInfoE loc_85 (sl_unlock) with
"_" <- LocInfoE loc_85 (global_sl_unlock) with
[ LocInfoE loc_86 (AnnotExpr 1%nat LockA (LocInfoE loc_86 (&(LocInfoE loc_87 ((LocInfoE loc_88 (!{LPtr} (LocInfoE loc_89 ("t")))) at{struct_lock_test} "lock"))))) ] ;
locinfo: loc_81 ;
Return (LocInfoE loc_82 (use{it_layout size_t} (LocInfoE loc_83 ("ret"))))
......@@ -324,7 +324,7 @@ Section code.
|}.
(* Definition of function [increment]. *)
Definition impl_increment (sl_lock sl_unlock : loc): function := {|
Definition impl_increment (global_sl_lock global_sl_unlock : loc): function := {|
f_args := [
("t", LPtr)
];
......@@ -335,7 +335,7 @@ Section code.
f_code := (
<[ "#0" :=
locinfo: loc_108 ;
"_" <- LocInfoE loc_169 (sl_lock) with
"_" <- LocInfoE loc_169 (global_sl_lock) with
[ LocInfoE loc_170 (&(LocInfoE loc_171 ((LocInfoE loc_172 (!{LPtr} (LocInfoE loc_173 ("t")))) at{struct_lock_test} "lock"))) ] ;
locinfo: loc_109 ;
annot: (UnlockA) ;
......@@ -352,7 +352,7 @@ Section code.
"ret" <-{ it_layout size_t }
LocInfoE loc_123 (use{it_layout size_t} (LocInfoE loc_124 ((LocInfoE loc_125 ((LocInfoE loc_126 (!{LPtr} (LocInfoE loc_127 ("t")))) at{struct_lock_test} "locked_struct")) at{struct_lock_test_inner} "a"))) ;
locinfo: loc_113 ;
"_" <- LocInfoE loc_118 (sl_unlock) with
"_" <- LocInfoE loc_118 (global_sl_unlock) with
[ LocInfoE loc_119 (AnnotExpr 1%nat LockA (LocInfoE loc_119 (&(LocInfoE loc_120 ((LocInfoE loc_121 (!{LPtr} (LocInfoE loc_122 ("t")))) at{struct_lock_test} "lock"))))) ] ;
locinfo: loc_114 ;
Return (LocInfoE loc_115 (use{it_layout size_t} (LocInfoE loc_116 ("ret"))))
......
......@@ -10,10 +10,10 @@ Section proof_increment.
Context `{!lockG Σ}.
(* Typing proof for [increment]. *)
Lemma type_increment (sl_lock sl_unlock : loc) :
sl_lock ◁ᵥ sl_lock @ function_ptr type_of_sl_lock -
sl_unlock ◁ᵥ sl_unlock @ function_ptr type_of_sl_unlock -
typed_function (impl_increment sl_lock sl_unlock) type_of_increment.
Lemma type_increment (global_sl_lock global_sl_unlock : loc) :
global_sl_lock ◁ᵥ global_sl_lock @ function_ptr type_of_sl_lock -
global_sl_unlock ◁ᵥ global_sl_unlock @ function_ptr type_of_sl_unlock -
typed_function (impl_increment global_sl_lock global_sl_unlock) type_of_increment.
Proof.
start_function "increment" ([[[[p q] n1] n2] n3]) => arg_t local_ret.
split_blocks ((
......
......@@ -10,9 +10,9 @@ Section proof_init.
Context `{!lockG Σ}.
(* Typing proof for [init]. *)
Lemma type_init (sl_init : loc) :
sl_init ◁ᵥ sl_init @ function_ptr type_of_sl_init -
typed_function (impl_init sl_init) type_of_init.
Lemma type_init (global_sl_init : loc) :
global_sl_init ◁ᵥ global_sl_init @ function_ptr type_of_sl_init -
typed_function (impl_init global_sl_init) type_of_init.
Proof.
start_function "init" (p) => arg_t.
split_blocks ((
......
......@@ -10,10 +10,10 @@ Section proof_read_locked.
Context `{!lockG Σ}.
(* Typing proof for [read_locked]. *)
Lemma type_read_locked (sl_lock sl_unlock : loc) :
sl_lock ◁ᵥ sl_lock @ function_ptr type_of_sl_lock -
sl_unlock ◁ᵥ sl_unlock @ function_ptr type_of_sl_unlock -
typed_function (impl_read_locked sl_lock sl_unlock) type_of_read_locked.
Lemma type_read_locked (global_sl_lock global_sl_unlock : loc) :
global_sl_lock ◁ᵥ global_sl_lock @ function_ptr type_of_sl_lock -
global_sl_unlock ◁ᵥ global_sl_unlock @ function_ptr type_of_sl_unlock -
typed_function (impl_read_locked global_sl_lock global_sl_unlock) type_of_read_locked.
Proof.
start_function "read_locked" ([[[[p q] n1] n2] n3]) => arg_t local_ret.
split_blocks ((
......
......@@ -10,10 +10,10 @@ Section proof_write_locked.
Context `{!lockG Σ}.
(* Typing proof for [write_locked]. *)
Lemma type_write_locked (sl_lock sl_unlock : loc) :
sl_lock ◁ᵥ sl_lock @ function_ptr type_of_sl_lock -
sl_unlock ◁ᵥ sl_unlock @ function_ptr type_of_sl_unlock -
typed_function (impl_write_locked sl_lock sl_unlock) type_of_write_locked.
Lemma type_write_locked (global_sl_lock global_sl_unlock : loc) :
global_sl_lock ◁ᵥ global_sl_lock @ function_ptr type_of_sl_lock -
global_sl_unlock ◁ᵥ global_sl_unlock @ function_ptr type_of_sl_unlock -
typed_function (impl_write_locked global_sl_lock global_sl_unlock) type_of_write_locked.
Proof.
start_function "write_locked" ([[[[[p n] q] n1] n2] n3]) => arg_t arg_n.
split_blocks ((
......
......@@ -849,7 +849,7 @@ Section code.
Solve Obligations with solve_struct_obligations.