diff options
author | Son HO | 2024-05-28 18:50:52 +0200 |
---|---|---|
committer | GitHub | 2024-05-28 18:50:52 +0200 |
commit | 95cb0eee7f9af0a0fd0d24a2531b5395b98b861f (patch) | |
tree | 4f8cea8688c85603ca250afa0b581aa4b96289ee /tests/coq | |
parent | ef7792c106a1f33397c206fcb5124b5ddfe64378 (diff) | |
parent | ae075db15638ee8878bebe3d31affb1aa320e90f (diff) |
Merge pull request #219 from AeneasVerif/son/infinite
Fix the infinite loop test
Diffstat (limited to 'tests/coq')
-rw-r--r-- | tests/coq/misc/InfiniteLoop.v | 27 |
1 files changed, 27 insertions, 0 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. |