Fix imports in tests

viperproject · Sep 29, 2020 · 5db62e1 · 5db62e1
1 parent 079a6d7
commit 5db62e1
Show file tree

Hide file tree

Showing 3 changed files with 18 additions and 10 deletions.
diff --git a/prusti-contracts/src/ghost.rs b/prusti-contracts/src/ghost.rs
@@ -19,6 +19,7 @@ macro_rules! implement_ghost_type_generic {
             /// Constructor for generic ghost types.
             /// #Examples
             ///  ```rust
+            ///  use prusti_contracts::{GhostInt, GhostSeq};
             ///  let seq_inst: GhostSeq<GhostInt> = GhostSeq::new();
             ///  ```
             pub fn new() -> Self {
@@ -48,6 +49,12 @@ impl Sub for GhostInt {
     }
 }
 
+impl GhostInt {
+    pub fn new(val: i32) -> Self {
+        GhostInt
+    }
+}
+
 // Ghost variant of Viper type, Bool
 implement_ghost_type!(GhostBool);
 // wrappers around standard operations on GhostBool
@@ -79,8 +86,9 @@ impl<T: Ghost> GhostSeq<T> {
     /// Push an item of type `T` to the ghost sequence
     /// #Examples
     /// ```rust
-    /// let seq: GhostSeq<i32> = GhostSeq::new();
-    /// seq.push(10);
+    /// use prusti_contracts::{GhostInt, GhostSeq};
+    /// let seq: GhostSeq<GhostInt> = GhostSeq::new();
+    /// seq.push(GhostInt::new(10));
     /// ```
     pub fn push(self, to_add: T) -> Self {
         GhostSeq::new()
@@ -89,9 +97,10 @@ impl<T: Ghost> GhostSeq<T> {
     /// Pop an item from a ghost sequence instance
     /// #Examples
     /// ```rust
-    /// let seq: GhostSeq<i32> = GhostSeq::new();
-    /// seq.push(10);
-    /// seq.pop(10);
+    /// use prusti_contracts::{GhostInt, GhostSeq};
+    /// let seq: GhostSeq<GhostInt> = GhostSeq::new();
+    /// seq.push(GhostInt::new(10));
+    /// seq.pop(GhostInt::new(10));
     /// ```
     pub fn pop(self, to_remove: T) -> Self {
         GhostSeq::new()
@@ -100,7 +109,8 @@ impl<T: Ghost> GhostSeq<T> {
     /// Concatenate two instances of ghost sequence
     /// #Examples
     /// ```rust
-    /// let seq1: GhostSeq<i32> = GhostSeq::new();
+    /// use prusti_contracts::{GhostInt, GhostSeq};
+    /// let seq1: GhostSeq<GhostInt> = GhostSeq::new();
     /// seq1.chain(seq2);
     /// ```
     pub fn chain(self, other: GhostSeq<T>) -> Self {

diff --git a/prusti-tests/tests/typecheck/fail/ghost_regular_types.rs b/prusti-tests/tests/typecheck/fail/ghost_regular_types.rs
@@ -1,5 +1,4 @@
-use prusti_contracts::*;
-use crate::ghost::GhostInt;
+use prusti_contracts::GhostInt;
 
 
 fn test_ghost_regular_sum() -> GhostInt {

diff --git a/prusti-tests/tests/typecheck/pass/ghost_types.rs b/prusti-tests/tests/typecheck/pass/ghost_types.rs
@@ -1,5 +1,4 @@
-use prusti_contracts::*;
-use crate::ghost::GhostInt;
+use prusti_contracts::GhostInt;
 
 fn test_ghost_int_sum() -> GhostInt{
     let a = GhostInt;