From 5db62e1c026df275dd4a2fe3c2e0fec8d08a09fa Mon Sep 17 00:00:00 2001
From: Karuna Grewal <karunagrewal98@gmail.com>
Date: Tue, 29 Sep 2020 17:27:43 +0530
Subject: [PATCH] Fix imports in tests

---
 prusti-contracts/src/ghost.rs                 | 22 ++++++++++++++-----
 .../typecheck/fail/ghost_regular_types.rs     |  3 +--
 .../tests/typecheck/pass/ghost_types.rs       |  3 +--
 3 files changed, 18 insertions(+), 10 deletions(-)

diff --git a/prusti-contracts/src/ghost.rs b/prusti-contracts/src/ghost.rs
index 5b65c0de3dd..6a1a920dab8 100644
--- 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
index 0986f9b9e19..01b9615255c 100644
--- 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
index 08cd506d3fc..a173b92f050 100644
--- 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;