From 082661f0d9d1bb1196ef8e1d57b3f2b4922b3d8e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 18 Jun 2024 12:12:05 +0200 Subject: Bump charon --- tests/coq/arrays/Arrays.v | 10 +++++----- tests/coq/betree/Betree_Funs.v | 8 ++++---- tests/coq/hashmap/Hashmap_Funs.v | 2 +- tests/coq/misc/Loops.v | 10 +++++----- 4 files changed, 15 insertions(+), 15 deletions(-) (limited to 'tests/coq') diff --git a/tests/coq/arrays/Arrays.v b/tests/coq/arrays/Arrays.v index 5ff17341..cd6a4b87 100644 --- a/tests/coq/arrays/Arrays.v +++ b/tests/coq/arrays/Arrays.v @@ -376,7 +376,7 @@ Definition non_copyable_array : result unit := . (** [arrays::sum]: loop 0: - Source: 'tests/src/arrays.rs', lines 245:0-253:1 *) + Source: 'tests/src/arrays.rs', lines 247:4-253:1 *) Fixpoint sum_loop (n : nat) (s : slice u32) (sum1 : u32) (i : usize) : result u32 := match n with @@ -400,7 +400,7 @@ Definition sum (n : nat) (s : slice u32) : result u32 := . (** [arrays::sum2]: loop 0: - Source: 'tests/src/arrays.rs', lines 255:0-264:1 *) + Source: 'tests/src/arrays.rs', lines 258:4-264:1 *) Fixpoint sum2_loop (n : nat) (s : slice u32) (s2 : slice u32) (sum1 : u32) (i : usize) : result u32 @@ -508,7 +508,7 @@ Definition ite : result unit := . (** [arrays::zero_slice]: loop 0: - Source: 'tests/src/arrays.rs', lines 306:0-313:1 *) + Source: 'tests/src/arrays.rs', lines 308:4-313:1 *) Fixpoint zero_slice_loop (n : nat) (a : slice u8) (i : usize) (len : usize) : result (slice u8) := match n with @@ -532,7 +532,7 @@ Definition zero_slice (n : nat) (a : slice u8) : result (slice u8) := . (** [arrays::iter_mut_slice]: loop 0: - Source: 'tests/src/arrays.rs', lines 315:0-321:1 *) + Source: 'tests/src/arrays.rs', lines 317:4-321:1 *) Fixpoint iter_mut_slice_loop (n : nat) (len : usize) (i : usize) : result unit := match n with @@ -551,7 +551,7 @@ Definition iter_mut_slice (n : nat) (a : slice u8) : result (slice u8) := . (** [arrays::sum_mut_slice]: loop 0: - Source: 'tests/src/arrays.rs', lines 323:0-331:1 *) + Source: 'tests/src/arrays.rs', lines 325:4-331:1 *) Fixpoint sum_mut_slice_loop (n : nat) (a : slice u32) (i : usize) (s : u32) : result u32 := match n with diff --git a/tests/coq/betree/Betree_Funs.v b/tests/coq/betree/Betree_Funs.v index 1c6092ba..bb9fe90e 100644 --- a/tests/coq/betree/Betree_Funs.v +++ b/tests/coq/betree/Betree_Funs.v @@ -89,7 +89,7 @@ Definition betree_upsert_update . (** [betree::betree::{betree::betree::List#1}::len]: loop 0: - Source: 'src/betree.rs', lines 276:4-284:5 *) + Source: 'src/betree.rs', lines 278:8-284:5 *) Fixpoint betree_List_len_loop (T : Type) (n : nat) (self : betree_List_t T) (len : u64) : result u64 := match n with @@ -111,7 +111,7 @@ Definition betree_List_len . (** [betree::betree::{betree::betree::List#1}::reverse]: loop 0: - Source: 'src/betree.rs', lines 304:4-312:5 *) + Source: 'src/betree.rs', lines 305:8-312:5 *) Fixpoint betree_List_reverse_loop (T : Type) (n : nat) (self : betree_List_t T) (out : betree_List_t T) : result (betree_List_t T) @@ -135,7 +135,7 @@ Definition betree_List_reverse . (** [betree::betree::{betree::betree::List#1}::split_at]: loop 0: - Source: 'src/betree.rs', lines 287:4-302:5 *) + Source: 'src/betree.rs', lines 289:8-302:5 *) Fixpoint betree_List_split_at_loop (T : Type) (n : nat) (n1 : u64) (beg : betree_List_t T) (self : betree_List_t T) : @@ -204,7 +204,7 @@ Definition betree_ListPairU64T_head_has_key . (** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: loop 0: - Source: 'src/betree.rs', lines 355:4-370:5 *) + Source: 'src/betree.rs', lines 358:8-370:5 *) Fixpoint betree_ListPairU64T_partition_at_pivot_loop (T : Type) (n : nat) (pivot : u64) (beg : betree_List_t (u64 * T)) (end1 : betree_List_t (u64 * T)) (self : betree_List_t (u64 * T)) : diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v index d63c6f72..39bd5098 100644 --- a/tests/coq/hashmap/Hashmap_Funs.v +++ b/tests/coq/hashmap/Hashmap_Funs.v @@ -70,7 +70,7 @@ Definition hashMap_new (T : Type) (n : nat) : result (HashMap_t T) := . (** [hashmap::{hashmap::HashMap}::clear]: loop 0: - Source: 'tests/src/hashmap.rs', lines 91:4-99:5 *) + Source: 'tests/src/hashmap.rs', lines 94:8-99:5 *) Fixpoint hashMap_clear_loop (T : Type) (n : nat) (slots : alloc_vec_Vec (AList_t T)) (i : usize) : result (alloc_vec_Vec (AList_t T)) diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v index 87b05193..a29394e1 100644 --- a/tests/coq/misc/Loops.v +++ b/tests/coq/misc/Loops.v @@ -9,7 +9,7 @@ Local Open Scope Primitives_scope. Module Loops. (** [loops::sum]: loop 0: - Source: 'tests/src/loops.rs', lines 8:0-18:1 *) + Source: 'tests/src/loops.rs', lines 10:4-18:1 *) Fixpoint sum_loop (n : nat) (max : u32) (i : u32) (s : u32) : result u32 := match n with | O => Fail_ OutOfFuel @@ -27,7 +27,7 @@ Definition sum (n : nat) (max : u32) : result u32 := . (** [loops::sum_with_mut_borrows]: loop 0: - Source: 'tests/src/loops.rs', lines 23:0-35:1 *) + Source: 'tests/src/loops.rs', lines 25:4-35:1 *) Fixpoint sum_with_mut_borrows_loop (n : nat) (max : u32) (i : u32) (s : u32) : result u32 := match n with @@ -49,7 +49,7 @@ Definition sum_with_mut_borrows (n : nat) (max : u32) : result u32 := . (** [loops::sum_with_shared_borrows]: loop 0: - Source: 'tests/src/loops.rs', lines 38:0-52:1 *) + Source: 'tests/src/loops.rs', lines 40:4-52:1 *) Fixpoint sum_with_shared_borrows_loop (n : nat) (max : u32) (i : u32) (s : u32) : result u32 := match n with @@ -71,7 +71,7 @@ Definition sum_with_shared_borrows (n : nat) (max : u32) : result u32 := . (** [loops::sum_array]: loop 0: - Source: 'tests/src/loops.rs', lines 54:0-62:1 *) + Source: 'tests/src/loops.rs', lines 56:4-62:1 *) Fixpoint sum_array_loop (N : usize) (n : nat) (a : array u32 N) (i : usize) (s : u32) : result u32 := match n with @@ -94,7 +94,7 @@ Definition sum_array (N : usize) (n : nat) (a : array u32 N) : result u32 := . (** [loops::clear]: loop 0: - Source: 'tests/src/loops.rs', lines 66:0-72:1 *) + Source: 'tests/src/loops.rs', lines 67:4-72:1 *) Fixpoint clear_loop (n : nat) (v : alloc_vec_Vec u32) (i : usize) : result (alloc_vec_Vec u32) := match n with -- cgit v1.2.3