Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Implement Enums #17

Closed
wants to merge 19 commits into from
Prev Previous commit
Next Next commit
Fix unfolds for enums
tillarnold committed Nov 6, 2023
commit 85890874ca8d4b561ae8a241914d6749a47e3b8f
14 changes: 10 additions & 4 deletions prusti-encoder/src/encoders/mir_impure.rs
Original file line number Diff line number Diff line change
@@ -352,27 +352,33 @@ impl<'vir, 'enc> EncoderVisitor<'vir, 'enc> {
return;
}
let place_ty = place.ty(self.local_decls, self.vcx.tcx);
//assert!(place_ty.variant_index.is_none());

let place_ty_out = self
let place_ty_encoded = self
.deps
.require_ref::<crate::encoders::TypeEncoder>(place_ty.ty)
.unwrap();

let pred_name = match place_ty.variant_index {
None => place_ty_encoded.predicate_name,
Some(idx) => {
place_ty_encoded.expect_enum().variants[idx.as_usize()].predicate_name
}
};

let ref_p = self.encode_place(place);
if matches!(
repack_op,
mir_state_analysis::free_pcs::RepackOp::Expand(..)
) {
self.stmt(vir::StmtData::Unfold(self.vcx.alloc(
vir::PredicateAppData {
target: place_ty_out.predicate_name,
target: pred_name,
args: self.vcx.alloc_slice(&[ref_p]),
},
)));
} else {
self.stmt(vir::StmtData::Fold(self.vcx.alloc(vir::PredicateAppData {
target: place_ty_out.predicate_name,
target: pred_name,
args: self.vcx.alloc_slice(&[ref_p]),
})));
}