Test Add ops on GhostInt

viperproject · Oct 10, 2020 · 3beeb22 · 3beeb22
1 parent 584c635
commit 3beeb22
Show file tree

Hide file tree

Showing 3 changed files with 17 additions and 9 deletions.
diff --git a/prusti-contracts/src/ghost.rs b/prusti-contracts/src/ghost.rs
@@ -5,6 +5,7 @@ pub unsafe auto trait Ghost {}
 
 macro_rules! implement_ghost_type {
     ($ghost_type: ident) => {
+        #[derive(PartialEq, Eq)]
         pub struct $ghost_type;
         unsafe impl Ghost for $ghost_type{}
     };

diff --git a/prusti-tests/tests/typecheck/pass/ghost_int.rs b/prusti-tests/tests/typecheck/pass/ghost_int.rs
@@ -1,9 +1,15 @@
+use prusti_contracts::GhostInt;
 use prusti_contracts::*;
-use crate::ghost::GhostInt;
 
-fn test4() {
-    let a = GhostInt;
-    let b = GhostInt;
-    let c = a + b;
-}   
+fn test_1() -> GhostInt{
+    let x = GhostInt::new(10);
+    let y = GhostInt::new(20);
+    x + y
+}
+
+#[ensures(result == gh1 + gh2)]
+fn test_2(gh1: GhostInt, gh2: GhostInt) -> GhostInt{
+   gh1 + gh2
+}
+
 fn main() {}
diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs
@@ -1887,16 +1887,17 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                             // Is this viper declaration of an Int type encoded in prepare_assign_target method?
                             // Currently, it's using the destination field from the MIR to accomplish this. I'm not sure how
                             // destination and location are related here.
+                            let value_field = self.encoder.encode_value_field(dest_ty);
                             stmts.extend(
                                 self.prepare_assign_target(
-                                    dst,
-                                    ref_field,
+                                    dst.clone(),
+                                    value_field.clone(),
                                     location,
                                     vir::AssignKind::Move,
                                 )
                             );
                             // N.B. Is encode_value_field the right choice here?
-                            let value_field = self.encoder.encode_value_field(dest_ty);
+                            //let value_field = self.encoder.encode_value_field(dest_ty);
                             // Step2. assign value = `ghost_val` to the above created destination/ location (unsure about the terminology)
                             stmts.extend(self.encode_assign_operand(&dst.clone().field(value_field), &args[0], location));
                         }