We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
pkvm_host_map_guest
1 parent 2b07504 commit 4396f35Copy full SHA for 4396f35
arch/arm64/kvm/hyp/nvhe/ghost_spec.c
@@ -670,7 +670,12 @@ bool compute_new_abstract_state_handle___pkvm_host_map_guest(struct ghost_state
670
* so it's safe to copy.
671
*/
672
copy_abstraction_host(g1, g0);
673
- copy_abstraction_pkvm(g1, g0);
+ if (call->memcache_donations.len > 0)
674
+ copy_abstraction_pkvm(g1, g0);
675
+ else {
676
+ ghost_assert(!g0->pkvm.present);
677
+ g1->pkvm.present = false;
678
+ }
679
680
for (int d=0; d<call->memcache_donations.len; d++) {
681
u64 pfn = call->memcache_donations.pages[d];
0 commit comments