Rerun axiomgen

mit-pdos · Dec 18, 2024 · 47029f4 · 47029f4
1 parent 1984ccf
commit 47029f4
Show file tree

Hide file tree

Showing 20 changed files with 60 additions and 20 deletions.
diff --git a/new_code_axioms/bytes.v b/new_code_axioms/bytes.v
@@ -7,6 +7,7 @@ Context `{ffi_syntax}.
 Axiom Buffer : go_type.
 Axiom Buffer__mset : list (string * val).
 Axiom Buffer__mset_ptr : list (string * val).
+Axiom ErrTooLarge : (string * string).
 Axiom Buffer__Bytes : val.
 Axiom Buffer__AvailableBuffer : val.
 Axiom Buffer__String : val.
@@ -100,5 +101,5 @@ Axiom Reader__Seek : val.
 Axiom Reader__WriteTo : val.
 Axiom Reader__Reset : val.
 Axiom NewReader : val.
-
+Axiom initialize' : val.
 End axioms.
diff --git a/new_code_axioms/context.v b/new_code_axioms/context.v
@@ -7,6 +7,8 @@ Context `{ffi_syntax}.
 Axiom Context : go_type.
 Axiom Context__mset : list (string * val).
 Axiom Context__mset_ptr : list (string * val).
+Axiom Canceled : (string * string).
+Axiom DeadlineExceeded : (string * string).
 Axiom deadlineExceededError__Error : val.
 Axiom deadlineExceededError__Timeout : val.
 Axiom deadlineExceededError__Temporary : val.
@@ -47,5 +49,5 @@ Axiom WithTimeoutCause : val.
 Axiom WithValue : val.
 Axiom valueCtx__String : val.
 Axiom valueCtx__Value : val.
-
+Axiom initialize' : val.
 End axioms.
diff --git a/new_code_axioms/crypto/rand.v b/new_code_axioms/crypto/rand.v
@@ -4,10 +4,11 @@ From New.golang Require Import defn.
 Section axioms.
 Context `{ffi_syntax}.
 
+Axiom Reader : (string * string).
 Axiom Read : val.
 Axiom reader__Read : val.
 Axiom hideAgainReader__Read : val.
 Axiom Prime : val.
 Axiom Int : val.
-
+Axiom initialize' : val.
 End axioms.
diff --git a/new_code_axioms/errors.v b/new_code_axioms/errors.v
@@ -6,11 +6,12 @@ Context `{ffi_syntax}.
 
 Axiom New : val.
 Axiom errorString__Error : val.
+Axiom ErrUnsupported : (string * string).
 Axiom Join : val.
 Axiom joinError__Error : val.
 Axiom joinError__Unwrap : val.
 Axiom Unwrap : val.
 Axiom Is : val.
 Axiom As : val.
-
+Axiom initialize' : val.
 End axioms.
diff --git a/new_code_axioms/github_com/stretchr/testify/assert.v b/new_code_axioms/github_com/stretchr/testify/assert.v
@@ -325,6 +325,7 @@ Axiom Never : val.
 Axiom ErrorIs : val.
 Axiom NotErrorIs : val.
 Axiom ErrorAs : val.
+Axiom AnError : (string * string).
 Axiom Assertions : go_type.
 Axiom Assertions__mset : list (string * val).
 Axiom Assertions__mset_ptr : list (string * val).
@@ -336,5 +337,5 @@ Axiom HTTPStatusCode : val.
 Axiom HTTPBody : val.
 Axiom HTTPBodyContains : val.
 Axiom HTTPBodyNotContains : val.
-
+Axiom initialize' : val.
 End axioms.
diff --git a/new_code_axioms/go_etcd_io/raft/v3/confchange.v b/new_code_axioms/go_etcd_io/raft/v3/confchange.v
@@ -12,5 +12,5 @@ Axiom Changer__LeaveJoint : val.
 Axiom Changer__Simple : val.
 Axiom Describe : val.
 Axiom Restore : val.
-
+Axiom initialize' : val.
 End axioms.
diff --git a/new_code_axioms/go_etcd_io/raft/v3/quorum/slices64.v b/new_code_axioms/go_etcd_io/raft/v3/quorum/slices64.v
@@ -5,5 +5,5 @@ Section axioms.
 Context `{ffi_syntax}.
 
 Axiom Sort : val.
-
+Axiom initialize' : val.
 End axioms.
diff --git a/new_code_axioms/io.v b/new_code_axioms/io.v
@@ -7,6 +7,11 @@ Context `{ffi_syntax}.
 Axiom SeekStart : Z.
 Axiom SeekCurrent : Z.
 Axiom SeekEnd : Z.
+Axiom ErrShortWrite : (string * string).
+Axiom ErrShortBuffer : (string * string).
+Axiom EOF : (string * string).
+Axiom ErrUnexpectedEOF : (string * string).
+Axiom ErrNoProgress : (string * string).
 Axiom Reader : go_type.
 Axiom Reader__mset : list (string * val).
 Axiom Reader__mset_ptr : list (string * val).
@@ -102,6 +107,7 @@ Axiom OffsetWriter__WriteAt : val.
 Axiom OffsetWriter__Seek : val.
 Axiom TeeReader : val.
 Axiom teeReader__Read : val.
+Axiom Discard : (string * string).
 Axiom discard__Write : val.
 Axiom discard__WriteString : val.
 Axiom discard__ReadFrom : val.
@@ -119,6 +125,7 @@ Axiom multiWriter__WriteString : val.
 Axiom MultiWriter : val.
 Axiom onceError__Store : val.
 Axiom onceError__Load : val.
+Axiom ErrClosedPipe : (string * string).
 Axiom PipeReader : go_type.
 Axiom PipeReader__mset : list (string * val).
 Axiom PipeReader__mset_ptr : list (string * val).
@@ -132,5 +139,5 @@ Axiom PipeWriter__Write : val.
 Axiom PipeWriter__Close : val.
 Axiom PipeWriter__CloseWithError : val.
 Axiom Pipe : val.
-
+Axiom initialize' : val.
 End axioms.
diff --git a/new_code_axioms/math.v b/new_code_axioms/math.v
@@ -101,5 +101,5 @@ Axiom Float32bits : val.
 Axiom Float32frombits : val.
 Axiom Float64bits : val.
 Axiom Float64frombits : val.
-
+Axiom initialize' : val.
 End axioms.
diff --git a/new_code_axioms/math/big.v b/new_code_axioms/math/big.v
@@ -185,5 +185,5 @@ Axiom Rat__MarshalText : val.
 Axiom Rat__UnmarshalText : val.
 Axiom RoundingMode__String : val.
 Axiom Float__Sqrt : val.
-
+Axiom initialize' : val.
 End axioms.
diff --git a/new_code_axioms/math/rand.v b/new_code_axioms/math/rand.v
@@ -61,5 +61,5 @@ Axiom Zipf__mset : list (string * val).
 Axiom Zipf__mset_ptr : list (string * val).
 Axiom NewZipf : val.
 Axiom Zipf__Uint64 : val.
-
+Axiom initialize' : val.
 End axioms.
diff --git a/new_code_axioms/os.v b/new_code_axioms/os.v
@@ -20,6 +20,13 @@ Axiom Setenv : val.
 Axiom Unsetenv : val.
 Axiom Clearenv : val.
 Axiom Environ : val.
+Axiom ErrInvalid : (string * string).
+Axiom ErrPermission : (string * string).
+Axiom ErrExist : (string * string).
+Axiom ErrNotExist : (string * string).
+Axiom ErrClosed : (string * string).
+Axiom ErrNoDeadline : (string * string).
+Axiom ErrDeadlineExceeded : (string * string).
 Axiom PathError : go_type.
 Axiom PathError__mset : list (string * val).
 Axiom PathError__mset_ptr : list (string * val).
@@ -34,6 +41,7 @@ Axiom IsExist : val.
 Axiom IsNotExist : val.
 Axiom IsPermission : val.
 Axiom IsTimeout : val.
+Axiom ErrProcessDone : (string * string).
 Axiom Process : go_type.
 Axiom Process__mset : list (string * val).
 Axiom Process__mset_ptr : list (string * val).
@@ -57,6 +65,8 @@ Axiom ProcessState__Exited : val.
 Axiom ProcessState__Success : val.
 Axiom ProcessState__Sys : val.
 Axiom ProcessState__SysUsage : val.
+Axiom Interrupt : (string * string).
+Axiom Kill : (string * string).
 Axiom ProcessState : go_type.
 Axiom ProcessState__mset : list (string * val).
 Axiom ProcessState__mset_ptr : list (string * val).
@@ -65,6 +75,9 @@ Axiom ProcessState__String : val.
 Axiom ProcessState__ExitCode : val.
 Axiom Executable : val.
 Axiom File__Name : val.
+Axiom Stdin : (string * string).
+Axiom Stdout : (string * string).
+Axiom Stderr : (string * string).
 Axiom O_RDONLY : expr.
 Axiom O_WRONLY : expr.
 Axiom O_RDWR : expr.
@@ -142,6 +155,7 @@ Axiom PathSeparator : expr.
 Axiom PathListSeparator : expr.
 Axiom IsPathSeparator : val.
 Axiom Pipe : val.
+Axiom Args : (string * string).
 Axiom Getuid : val.
 Axiom Geteuid : val.
 Axiom Getgid : val.
@@ -189,5 +203,5 @@ Axiom fileStat__Size : val.
 Axiom fileStat__Mode : val.
 Axiom fileStat__ModTime : val.
 Axiom fileStat__Sys : val.
-
+Axiom initialize' : val.
 End axioms.
diff --git a/new_code_axioms/slices.v b/new_code_axioms/slices.v
@@ -45,5 +45,5 @@ Axiom MaxFunc : val.
 Axiom BinarySearch : val.
 Axiom BinarySearchFunc : val.
 Axiom xorshift__Next : val.
-
+Axiom initialize' : val.
 End axioms.
diff --git a/new_code_axioms/sort.v b/new_code_axioms/sort.v
@@ -51,5 +51,5 @@ Axiom IntsAreSorted : val.
 Axiom Float64sAreSorted : val.
 Axiom StringsAreSorted : val.
 Axiom Stable : val.
-
+Axiom initialize' : val.
 End axioms.
diff --git a/new_code_axioms/strconv.v b/new_code_axioms/strconv.v
@@ -9,6 +9,8 @@ Axiom FormatBool : val.
 Axiom AppendBool : val.
 Axiom ParseComplex : val.
 Axiom ParseFloat : val.
+Axiom ErrRange : (string * string).
+Axiom ErrSyntax : (string * string).
 Axiom NumError : go_type.
 Axiom NumError__mset : list (string * val).
 Axiom NumError__mset_ptr : list (string * val).
@@ -51,5 +53,5 @@ Axiom QuotedPrefix : val.
 Axiom Unquote : val.
 Axiom IsPrint : val.
 Axiom IsGraphic : val.
-
+Axiom initialize' : val.
 End axioms.
diff --git a/new_code_axioms/strings.v b/new_code_axioms/strings.v
@@ -98,5 +98,5 @@ Axiom Index : val.
 Axiom Cut : val.
 Axiom CutPrefix : val.
 Axiom CutSuffix : val.
-
+Axiom initialize' : val.
 End axioms.
diff --git a/new_code_axioms/testing.v b/new_code_axioms/testing.v
@@ -127,5 +127,5 @@ Axiom M__mset_ptr : list (string * val).
 Axiom MainStart : val.
 Axiom M__Run : val.
 Axiom RunTests : val.
-
+Axiom initialize' : val.
 End axioms.
diff --git a/new_partial_axioms/fmt.v b/new_partial_axioms/fmt.v
@@ -63,5 +63,5 @@ Axiom ss__Token : val.
 Axiom readRune__ReadRune : val.
 Axiom readRune__UnreadRune : val.
 Axiom ss__SkipSpace : val.
-
+Axiom initialize' : val.
 End axioms.
diff --git a/new_partial_axioms/go_etcd_io/raft/v3/raftpb.v b/new_partial_axioms/go_etcd_io/raft/v3/raftpb.v
@@ -23,6 +23,8 @@ Axiom EntryType__mset_ptr : list (string * val).
 Axiom EntryNormal : expr.
 Axiom EntryConfChange : expr.
 Axiom EntryConfChangeV2 : expr.
+Axiom EntryType_name : (string * string).
+Axiom EntryType_value : (string * string).
 Axiom EntryType__Enum : val.
 Axiom EntryType__String : val.
 Axiom EntryType__UnmarshalJSON : val.
@@ -54,6 +56,8 @@ Axiom MsgStorageAppendResp : expr.
 Axiom MsgStorageApply : expr.
 Axiom MsgStorageApplyResp : expr.
 Axiom MsgForgetLeader : expr.
+Axiom MessageType_name : (string * string).
+Axiom MessageType_value : (string * string).
 Axiom MessageType__Enum : val.
 Axiom MessageType__String : val.
 Axiom MessageType__UnmarshalJSON : val.
@@ -64,6 +68,8 @@ Axiom ConfChangeTransition__mset_ptr : list (string * val).
 Axiom ConfChangeTransitionAuto : expr.
 Axiom ConfChangeTransitionJointImplicit : expr.
 Axiom ConfChangeTransitionJointExplicit : expr.
+Axiom ConfChangeTransition_name : (string * string).
+Axiom ConfChangeTransition_value : (string * string).
 Axiom ConfChangeTransition__Enum : val.
 Axiom ConfChangeTransition__String : val.
 Axiom ConfChangeTransition__UnmarshalJSON : val.
@@ -75,6 +81,8 @@ Axiom ConfChangeAddNode : expr.
 Axiom ConfChangeRemoveNode : expr.
 Axiom ConfChangeUpdateNode : expr.
 Axiom ConfChangeAddLearnerNode : expr.
+Axiom ConfChangeType_name : (string * string).
+Axiom ConfChangeType_value : (string * string).
 Axiom ConfChangeType__Enum : val.
 Axiom ConfChangeType__String : val.
 Axiom ConfChangeType__UnmarshalJSON : val.
@@ -232,5 +240,8 @@ Axiom ConfState__Unmarshal : val.
 Axiom ConfChange__Unmarshal : val.
 Axiom ConfChangeSingle__Unmarshal : val.
 Axiom ConfChangeV2__Unmarshal : val.
-
+Axiom ErrInvalidLengthRaft : (string * string).
+Axiom ErrIntOverflowRaft : (string * string).
+Axiom ErrUnexpectedEndOfGroupRaft : (string * string).
+Axiom initialize' : val.
 End axioms.
diff --git a/new_partial_axioms/log.v b/new_partial_axioms/log.v
@@ -49,5 +49,5 @@ Axiom Panic : val.
 Axiom Panicf : val.
 Axiom Panicln : val.
 Axiom Output : val.
-
+Axiom initialize' : val.
 End axioms.