summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorSon HO2024-05-28 18:50:52 +0200
committerGitHub2024-05-28 18:50:52 +0200
commit95cb0eee7f9af0a0fd0d24a2531b5395b98b861f (patch)
tree4f8cea8688c85603ca250afa0b581aa4b96289ee /tests
parentef7792c106a1f33397c206fcb5124b5ddfe64378 (diff)
parentae075db15638ee8878bebe3d31affb1aa320e90f (diff)
Merge pull request #219 from AeneasVerif/son/infinite
Fix the infinite loop test
Diffstat (limited to 'tests')
-rw-r--r--tests/coq/misc/InfiniteLoop.v27
-rw-r--r--tests/fstar/misc/InfiniteLoop.fst24
-rw-r--r--tests/lean/InfiniteLoop.lean25
-rw-r--r--tests/src/infinite-loop.rs1
4 files changed, 76 insertions, 1 deletions
diff --git a/tests/coq/misc/InfiniteLoop.v b/tests/coq/misc/InfiniteLoop.v
new file mode 100644
index 00000000..1c0ccbe0
--- /dev/null
+++ b/tests/coq/misc/InfiniteLoop.v
@@ -0,0 +1,27 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [infinite_loop] *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Module InfiniteLoop.
+
+(** [infinite_loop::bar]:
+ Source: 'tests/src/infinite-loop.rs', lines 4:0-4:8 *)
+Definition bar : result unit :=
+ Ok tt.
+
+(** [infinite_loop::foo]: loop 0:
+ Source: 'tests/src/infinite-loop.rs', lines 6:0-10:1 *)
+Fixpoint foo_loop (n : nat) : result unit :=
+ match n with | O => Fail_ OutOfFuel | S n1 => _ <- bar; foo_loop n1 end
+.
+
+(** [infinite_loop::foo]:
+ Source: 'tests/src/infinite-loop.rs', lines 6:0-6:8 *)
+Definition foo (n : nat) : result unit :=
+ foo_loop n.
+
+End InfiniteLoop.
diff --git a/tests/fstar/misc/InfiniteLoop.fst b/tests/fstar/misc/InfiniteLoop.fst
new file mode 100644
index 00000000..4e7c8c06
--- /dev/null
+++ b/tests/fstar/misc/InfiniteLoop.fst
@@ -0,0 +1,24 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [infinite_loop] *)
+module InfiniteLoop
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [infinite_loop::bar]:
+ Source: 'tests/src/infinite-loop.rs', lines 4:0-4:8 *)
+let bar : result unit =
+ Ok ()
+
+(** [infinite_loop::foo]: loop 0:
+ Source: 'tests/src/infinite-loop.rs', lines 6:0-10:1 *)
+let rec foo_loop (n : nat) : result unit =
+ if is_zero n
+ then Fail OutOfFuel
+ else let n1 = decrease n in let* _ = bar in foo_loop n1
+
+(** [infinite_loop::foo]:
+ Source: 'tests/src/infinite-loop.rs', lines 6:0-6:8 *)
+let foo (n : nat) : result unit =
+ foo_loop n
+
diff --git a/tests/lean/InfiniteLoop.lean b/tests/lean/InfiniteLoop.lean
new file mode 100644
index 00000000..9eb8e22c
--- /dev/null
+++ b/tests/lean/InfiniteLoop.lean
@@ -0,0 +1,25 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [infinite_loop]
+import Base
+open Primitives
+
+namespace infinite_loop
+
+/- [infinite_loop::bar]:
+ Source: 'tests/src/infinite-loop.rs', lines 4:0-4:8 -/
+def bar : Result Unit :=
+ Result.ok ()
+
+/- [infinite_loop::foo]: loop 0:
+ Source: 'tests/src/infinite-loop.rs', lines 6:0-10:1 -/
+divergent def foo_loop : Result Unit :=
+ do
+ let _ ← bar
+ foo_loop
+
+/- [infinite_loop::foo]:
+ Source: 'tests/src/infinite-loop.rs', lines 6:0-6:8 -/
+def foo : Result Unit :=
+ foo_loop
+
+end infinite_loop
diff --git a/tests/src/infinite-loop.rs b/tests/src/infinite-loop.rs
index 906fc1fa..0e247d20 100644
--- a/tests/src/infinite-loop.rs
+++ b/tests/src/infinite-loop.rs
@@ -1,4 +1,3 @@
-//@ [coq,fstar,lean] skip
//@ [coq,fstar] aeneas-args=-use-fuel
//@ [coq,fstar] subdir=misc
// FIXME: make it work