summaryrefslogtreecommitdiff
path: root/tests/coq
diff options
context:
space:
mode:
authorSon HO2024-03-09 01:12:20 +0100
committerGitHub2024-03-09 01:12:20 +0100
commit14171474f9a4a45874d181cdb6567c7af7dc32cd (patch)
treef4c7dcd5b172e8922487dec83070e2c38e7b441a /tests/coq
parent169d011cbfa83d853d0148bbf6b946e6ccbe4c4c (diff)
parent46f2f1c0c4c37f089e42c82d76d79817101c5407 (diff)
Merge pull request #85 from AeneasVerif/son/fix_loops3
Fix some issues with the loops
Diffstat (limited to '')
-rw-r--r--tests/coq/arrays/Arrays.v69
-rw-r--r--tests/coq/misc/Loops.v64
2 files changed, 133 insertions, 0 deletions
diff --git a/tests/coq/arrays/Arrays.v b/tests/coq/arrays/Arrays.v
index 3a6fb02f..79be3678 100644
--- a/tests/coq/arrays/Arrays.v
+++ b/tests/coq/arrays/Arrays.v
@@ -516,4 +516,73 @@ Definition ite : result unit :=
Return tt
.
+(** [arrays::zero_slice]: loop 0:
+ Source: 'src/arrays.rs', lines 303:0-310:1 *)
+Fixpoint zero_slice_loop
+ (n : nat) (a : slice u8) (i : usize) (len : usize) : result (slice u8) :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n1 =>
+ if i s< len
+ then (
+ p <- slice_index_mut_usize u8 a i;
+ let (_, index_mut_back) := p in
+ i1 <- usize_add i 1%usize;
+ a1 <- index_mut_back 0%u8;
+ zero_slice_loop n1 a1 i1 len)
+ else Return a
+ end
+.
+
+(** [arrays::zero_slice]:
+ Source: 'src/arrays.rs', lines 303:0-303:31 *)
+Definition zero_slice (n : nat) (a : slice u8) : result (slice u8) :=
+ let len := slice_len u8 a in zero_slice_loop n a 0%usize len
+.
+
+(** [arrays::iter_mut_slice]: loop 0:
+ Source: 'src/arrays.rs', lines 312:0-318:1 *)
+Fixpoint iter_mut_slice_loop
+ (n : nat) (len : usize) (i : usize) : result unit :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n1 =>
+ if i s< len
+ then (
+ i1 <- usize_add i 1%usize; _ <- iter_mut_slice_loop n1 len i1; Return tt)
+ else Return tt
+ end
+.
+
+(** [arrays::iter_mut_slice]:
+ Source: 'src/arrays.rs', lines 312:0-312:35 *)
+Definition iter_mut_slice (n : nat) (a : slice u8) : result (slice u8) :=
+ let len := slice_len u8 a in _ <- iter_mut_slice_loop n len 0%usize; Return a
+.
+
+(** [arrays::sum_mut_slice]: loop 0:
+ Source: 'src/arrays.rs', lines 320:0-328:1 *)
+Fixpoint sum_mut_slice_loop
+ (n : nat) (a : slice u32) (i : usize) (s : u32) : result u32 :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n1 =>
+ let i1 := slice_len u32 a in
+ if i s< i1
+ then (
+ i2 <- slice_index_usize u32 a i;
+ s1 <- u32_add s i2;
+ i3 <- usize_add i 1%usize;
+ sum_mut_slice_loop n1 a i3 s1)
+ else Return s
+ end
+.
+
+(** [arrays::sum_mut_slice]:
+ Source: 'src/arrays.rs', lines 320:0-320:42 *)
+Definition sum_mut_slice
+ (n : nat) (a : slice u32) : result (u32 * (slice u32)) :=
+ i <- sum_mut_slice_loop n a 0%usize 0%u32; Return (i, a)
+.
+
End Arrays.
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 8260db02..e235b60d 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -688,4 +688,68 @@ Definition list_nth_shared_mut_loop_pair_merge
Return (p1, back_'a)
.
+(** [loops::ignore_input_mut_borrow]: loop 0:
+ Source: 'src/loops.rs', lines 345:0-349:1 *)
+Fixpoint ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n1 =>
+ if i s> 0%u32
+ then (
+ i1 <- u32_sub i 1%u32; _ <- ignore_input_mut_borrow_loop n1 i1; Return tt)
+ else Return tt
+ end
+.
+
+(** [loops::ignore_input_mut_borrow]:
+ Source: 'src/loops.rs', lines 345:0-345:56 *)
+Definition ignore_input_mut_borrow
+ (n : nat) (_a : u32) (i : u32) : result u32 :=
+ _ <- ignore_input_mut_borrow_loop n i; Return _a
+.
+
+(** [loops::incr_ignore_input_mut_borrow]: loop 0:
+ Source: 'src/loops.rs', lines 353:0-358:1 *)
+Fixpoint incr_ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n1 =>
+ if i s> 0%u32
+ then (
+ i1 <- u32_sub i 1%u32;
+ _ <- incr_ignore_input_mut_borrow_loop n1 i1;
+ Return tt)
+ else Return tt
+ end
+.
+
+(** [loops::incr_ignore_input_mut_borrow]:
+ Source: 'src/loops.rs', lines 353:0-353:60 *)
+Definition incr_ignore_input_mut_borrow
+ (n : nat) (a : u32) (i : u32) : result u32 :=
+ a1 <- u32_add a 1%u32; _ <- incr_ignore_input_mut_borrow_loop n i; Return a1
+.
+
+(** [loops::ignore_input_shared_borrow]: loop 0:
+ Source: 'src/loops.rs', lines 362:0-366:1 *)
+Fixpoint ignore_input_shared_borrow_loop (n : nat) (i : u32) : result unit :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n1 =>
+ if i s> 0%u32
+ then (
+ i1 <- u32_sub i 1%u32;
+ _ <- ignore_input_shared_borrow_loop n1 i1;
+ Return tt)
+ else Return tt
+ end
+.
+
+(** [loops::ignore_input_shared_borrow]:
+ Source: 'src/loops.rs', lines 362:0-362:59 *)
+Definition ignore_input_shared_borrow
+ (n : nat) (_a : u32) (i : u32) : result u32 :=
+ _ <- ignore_input_shared_borrow_loop n i; Return _a
+.
+
End Loops.