Merge pull request #219 from AeneasVerif/son/infinite

Fix the infinite loop test

5 files changed, 77 insertions, 5 deletions

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index d6d2e018..cc203040 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -3529,10 +3529,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
       if effect_info.stateful then mk_simpl_tuple_ty [ mk_state_ty; output ]
       else output
     in
-    let output =
-      if effect_info.can_fail && inputs <> [] then mk_result_ty output
-      else output
-    in
+    let output = if effect_info.can_fail then mk_result_ty output else output in
     (back_info, output)
   in
 
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