Skip to content

Commit

Permalink
Update gold
Browse files Browse the repository at this point in the history
  • Loading branch information
upamanyus committed Oct 29, 2024
1 parent 7293887 commit a58ccc8
Show file tree
Hide file tree
Showing 6 changed files with 327 additions and 327 deletions.
36 changes: 18 additions & 18 deletions testdata/examples/append_log/append_log.gold.v
Original file line number Diff line number Diff line change
Expand Up @@ -148,23 +148,23 @@ Definition Init : val :=
exception_do (let: "diskSz" := (ref_ty uint64T "diskSz") in
(if: (![uint64T] "diskSz") < #(W64 1)
then
return: (ref_ty Log (let: "m" := (ref_ty sync.Mutex (zero_val sync.Mutex)) in
let: "sz" := #(W64 0) in
let: "diskSz" := #(W64 0) in
return: (ref_ty Log (let: "$m" := (ref_ty sync.Mutex (zero_val sync.Mutex)) in
let: "$sz" := #(W64 0) in
let: "$diskSz" := #(W64 0) in
struct.make Log [{
"m" ::= "m";
"sz" ::= "sz";
"diskSz" ::= "diskSz"
"m" ::= "$m";
"sz" ::= "$sz";
"diskSz" ::= "$diskSz"
}]), #false)
else do: #());;;
let: "log" := (ref_ty ptrT (zero_val ptrT)) in
let: "$r0" := (ref_ty Log (let: "m" := (ref_ty sync.Mutex (zero_val sync.Mutex)) in
let: "sz" := #(W64 0) in
let: "diskSz" := (![uint64T] "diskSz") in
let: "$r0" := (ref_ty Log (let: "$m" := (ref_ty sync.Mutex (zero_val sync.Mutex)) in
let: "$sz" := #(W64 0) in
let: "$diskSz" := (![uint64T] "diskSz") in
struct.make Log [{
"m" ::= "m";
"sz" ::= "sz";
"diskSz" ::= "diskSz"
"m" ::= "$m";
"sz" ::= "$sz";
"diskSz" ::= "$diskSz"
}])) in
do: ("log" <-[ptrT] "$r0");;;
do: ((Log__writeHdr (![ptrT] "log")) #());;;
Expand All @@ -187,11 +187,11 @@ Definition Open : val :=
let: "diskSz" := (ref_ty uint64T (zero_val uint64T)) in
let: "$r0" := ((marshal.Dec__GetInt (![marshal.Dec] "dec")) #()) in
do: ("diskSz" <-[uint64T] "$r0");;;
return: (ref_ty Log (let: "m" := (ref_ty sync.Mutex (zero_val sync.Mutex)) in
let: "sz" := (![uint64T] "sz") in
let: "diskSz" := (![uint64T] "diskSz") in
return: (ref_ty Log (let: "$m" := (ref_ty sync.Mutex (zero_val sync.Mutex)) in
let: "$sz" := (![uint64T] "sz") in
let: "$diskSz" := (![uint64T] "diskSz") in
struct.make Log [{
"m" ::= "m";
"sz" ::= "sz";
"diskSz" ::= "diskSz"
"m" ::= "$m";
"sz" ::= "$sz";
"diskSz" ::= "$diskSz"
}]))).
36 changes: 18 additions & 18 deletions testdata/examples/logging2/logging2.gold.v
Original file line number Diff line number Diff line change
Expand Up @@ -302,21 +302,21 @@ Definition Init : val :=
rec: "Init" "logSz" :=
exception_do (let: "logSz" := (ref_ty uint64T "logSz") in
let: "log" := (ref_ty Log (zero_val Log)) in
let: "$r0" := (let: "logLock" := (ref_ty sync.Mutex (zero_val sync.Mutex)) in
let: "memLock" := (ref_ty sync.Mutex (zero_val sync.Mutex)) in
let: "logSz" := (![uint64T] "logSz") in
let: "memLog" := (ref_ty sliceT (zero_val sliceT)) in
let: "memLen" := (ref_ty uint64T (zero_val uint64T)) in
let: "memTxnNxt" := (ref_ty uint64T (zero_val uint64T)) in
let: "logTxnNxt" := (ref_ty uint64T (zero_val uint64T)) in
let: "$r0" := (let: "$logLock" := (ref_ty sync.Mutex (zero_val sync.Mutex)) in
let: "$memLock" := (ref_ty sync.Mutex (zero_val sync.Mutex)) in
let: "$logSz" := (![uint64T] "logSz") in
let: "$memLog" := (ref_ty sliceT (zero_val sliceT)) in
let: "$memLen" := (ref_ty uint64T (zero_val uint64T)) in
let: "$memTxnNxt" := (ref_ty uint64T (zero_val uint64T)) in
let: "$logTxnNxt" := (ref_ty uint64T (zero_val uint64T)) in
struct.make Log [{
"logLock" ::= "logLock";
"memLock" ::= "memLock";
"logSz" ::= "logSz";
"memLog" ::= "memLog";
"memLen" ::= "memLen";
"memTxnNxt" ::= "memTxnNxt";
"logTxnNxt" ::= "logTxnNxt"
"logLock" ::= "$logLock";
"memLock" ::= "$memLock";
"logSz" ::= "$logSz";
"memLog" ::= "$memLog";
"memLen" ::= "$memLen";
"memTxnNxt" ::= "$memTxnNxt";
"logTxnNxt" ::= "$logTxnNxt"
}]) in
do: ("log" <-[Log] "$r0");;;
do: (let: "$a0" := #(W64 0) in
Expand Down Expand Up @@ -422,11 +422,11 @@ Definition Begin : val :=
rec: "Begin" "log" :=
exception_do (let: "log" := (ref_ty ptrT "log") in
let: "txn" := (ref_ty Txn (zero_val Txn)) in
let: "$r0" := (let: "log" := (![ptrT] "log") in
let: "blks" := (map.make uint64T sliceT #()) in
let: "$r0" := (let: "$log" := (![ptrT] "log") in
let: "$blks" := (map.make uint64T sliceT #()) in
struct.make Txn [{
"log" ::= "log";
"blks" ::= "blks"
"log" ::= "$log";
"blks" ::= "$blks"
}]) in
do: ("txn" <-[Txn] "$r0");;;
return: (![Txn] "txn")).
Loading

0 comments on commit a58ccc8

Please sign in to comment.