diff options
| author | Nadrieril | 2024-05-27 17:33:56 +0200 |
|---|---|---|
| committer | Nadrieril | 2024-05-28 11:36:31 +0200 |
| commit | c81c96f20b1dbf428a9ed42e83b910e798e1a225 (patch) | |
| tree | b01e01eb4bcec7112399647943047bed3b58cad1 /tests/src/infinite-loop.rs | |
| parent | 9cc69020773cc77965a6faa6f0d46f179de3d8b8 (diff) | |
Add some tests
Diffstat (limited to 'tests/src/infinite-loop.rs')
| -rw-r--r-- | tests/src/infinite-loop.rs | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/tests/src/infinite-loop.rs b/tests/src/infinite-loop.rs new file mode 100644 index 00000000..906fc1fa --- /dev/null +++ b/tests/src/infinite-loop.rs @@ -0,0 +1,11 @@ +//@ [coq,fstar,lean] skip +//@ [coq,fstar] aeneas-args=-use-fuel +//@ [coq,fstar] subdir=misc +// FIXME: make it work +fn bar() {} + +fn foo() { + loop { + bar() + } +} |