From 584c6355477d357186b1b0ecce47a03842add11b Mon Sep 17 00:00:00 2001 From: Karuna Grewal Date: Sat, 3 Oct 2020 15:23:10 +0530 Subject: [PATCH] Encoding ghost::new() method for GhostInt --- prusti-viper/src/encoder/procedure_encoder.rs | 25 +++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index 3cb89f076ca..8110971aec3 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -1876,6 +1876,31 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { stmts.extend(self.encode_assign_operand(&box_content, &args[0], location)); } + "prusti_contracts::ghost::GhostInt::new" => { + // let sample_ghost_int = GhostInt::new(ghost_val); + //args[0] will have the integer value `ghost_val` + + // N.B. Do we need to encode the destination for ghost variables as well? + let &(ref target_place, _) = destination.as_ref().unwrap(); + let (dst, dest_ty, _) = self.mir_encoder.encode_place(target_place).unwrap(); + // Step 1. get a destination location for `var sample_ghost_int: Int;` + // 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. + stmts.extend( + self.prepare_assign_target( + dst, + ref_field, + location, + vir::AssignKind::Move, + ) + ); + // N.B. Is encode_value_field the right choice here? + 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)); + } + "std::cmp::PartialEq::eq" | "core::cmp::PartialEq::eq" if args.len() == 2 &&