kvirt_alloc_succeeds

ostd::mm::kspace::kvirt_area

Function kvirt_alloc_succeeds 

Source 
pub proof fn kvirt_alloc_succeeds(area_size: usize)
Expand description
requires
0 < area_size <= usize::MAX / 2,
ensures
kvirt_alloc_spec(area_size).is_ok(),