Add tests

creusot/tests/should_fail/terminates/default_function_non_logic.rs

@@ -0,0 +1,16 @@
+extern crate creusot_contracts;
+use creusot_contracts::*;
+
+trait Foo {
+    #[terminates]
+    fn f() {}
+    #[terminates]
+    fn g();
+}
+
+impl Foo for i32 {
+    #[terminates]
+    fn g() {
+        Self::f(); // this assumes f could call g
+    }
+}

creusot/tests/should_fail/terminates/default_function_non_logic.stderr

@@ -0,0 +1,14 @@
+error: Mutually recursive functions: when calling `<i32 as Foo>::g`...
+  --> default_function_non_logic.rs:13:5
+   |
+13 |     fn g() {
+   |     ^^^^^^
+   |
+note: then `<i32 as Foo>::g` might call `<i32 as Foo>::g` via the call to `Foo::f`.
+  --> default_function_non_logic.rs:14:9
+   |
+14 |         Self::f(); // this assumes f could call g
+   |         ^^^^^^^^^
+
+error: aborting due to 1 previous error
+

creusot/tests/should_fail/terminates/default_function_non_open.rs

@@ -0,0 +1,21 @@
+extern crate creusot_contracts;
+use creusot_contracts::*;
+
+mod inner {
+    use super::*;
+    pub(super) trait Foo {
+        #[open(self)]
+        #[logic]
+        fn f() {}
+        #[logic]
+        fn g();
+    }
+}
+
+impl inner::Foo for i32 {
+    #[open(self)]
+    #[logic]
+    fn g() {
+        Self::f(); // this assumes f could call g
+    }
+}

creusot/tests/should_fail/terminates/default_function_non_open.stderr

@@ -0,0 +1,14 @@
+error: Mutually recursive functions: when calling `<impl inner::Foo for i32>::g`...
+  --> default_function_non_open.rs:18:5
+   |
+18 |     fn g() {
+   |     ^^^^^^
+   |
+note: then `<impl inner::Foo for i32>::g` might call `<impl inner::Foo for i32>::g` via the call to `inner::Foo::f`.
+  --> default_function_non_open.rs:19:9
+   |
+19 |         Self::f(); // this assumes f could call g
+   |         ^^^^^^^^^
+
+error: aborting due to 1 previous error
+

creusot/tests/should_fail/terminates/loop_through_default_impl.rs

@@ -0,0 +1,35 @@
+#![allow(incomplete_features)]
+#![feature(specialization)]
+
+extern crate creusot_contracts;
+use creusot_contracts::*;
+
+pub trait Foo {
+    #[logic]
+    fn f();
+    #[logic]
+    fn g();
+}
+default impl<T> Foo for T {
+    #[logic]
+    #[open]
+    fn f() {
+        h();
+    }
+    #[logic]
+    #[open]
+    fn g() {}
+}
+impl Foo for i32 {
+    #[logic]
+    #[open]
+    fn g() {
+        Self::f();
+    }
+}
+
+#[logic]
+#[open]
+pub fn h() {
+    <i32 as Foo>::g();
+}

creusot/tests/should_fail/terminates/loop_through_default_impl.stderr

@@ -0,0 +1,24 @@
+error: Mutually recursive functions: when calling `<T as Foo>::f`...
+  --> loop_through_default_impl.rs:16:5
+   |
+16 |     fn f() {
+   |     ^^^^^^
+   |
+note: then `<T as Foo>::f` calls `h`...
+  --> loop_through_default_impl.rs:17:9
+   |
+17 |         h();
+   |         ^^^
+note: then `h` calls `<i32 as Foo>::g`...
+  --> loop_through_default_impl.rs:34:5
+   |
+34 |     <i32 as Foo>::g();
+   |     ^^^^^^^^^^^^^^^^^
+note: finally `<i32 as Foo>::g` calls `<T as Foo>::f`.
+  --> loop_through_default_impl.rs:27:9
+   |
+27 |         Self::f();
+   |         ^^^^^^^^^
+
+error: aborting due to 1 previous error
+

creusot/tests/should_succeed/termination/call_in_contract.rs

@@ -0,0 +1,17 @@
+extern crate creusot_contracts;
+use creusot_contracts::*;
+
+pub trait Foo {
+    #[logic]
+    #[open(self)]
+    fn f() {}
+    #[logic]
+    fn g();
+}
+
+impl Foo for () {
+    #[logic]
+    #[ensures(Self::f() == ())]
+    #[open(self)]
+    fn g() {}
+}

creusot/tests/should_succeed/termination/default_impl.rs

@@ -0,0 +1,28 @@
+#![allow(incomplete_features)]
+#![feature(specialization)]
+
+extern crate creusot_contracts;
+use creusot_contracts::*;
+
+pub trait Foo {
+    #[logic]
+    fn f();
+    #[logic]
+    fn g();
+}
+default impl<T> Foo for T {
+    #[logic]
+    #[open]
+    fn f() {}
+    #[logic]
+    #[open]
+    fn g() {}
+}
+
+impl Foo for () {
+    #[logic]
+    #[open]
+    fn g() {
+        Self::f();
+    }
+}

creusot/tests/should_succeed/termination/default_impl_in_trait.rs

@@ -0,0 +1,45 @@
+extern crate creusot_contracts;
+use creusot_contracts::*;
+
+pub trait Foo {
+    #[logic]
+    #[open(self)]
+    fn f() {}
+    #[logic]
+    fn g();
+}
+
+pub mod inner {
+    use super::*;
+    pub trait Bar {
+        #[logic]
+        #[open(super)]
+        fn f() {}
+        #[logic]
+        fn g();
+    }
+}
+
+impl Foo for () {
+    #[logic]
+    #[open(self)]
+    fn g() {
+        <Self as Foo>::f();
+    }
+}
+
+impl<T> Foo for Box<T> {
+    #[logic]
+    #[open(self)]
+    fn g() {
+        <Self as Foo>::f();
+    }
+}
+
+impl inner::Bar for () {
+    #[logic]
+    #[open(self)]
+    fn g() {
+        <Self as inner::Bar>::f();
+    }
+}