in checker/src/body_visitor.rs [1460:1519]
fn update_zeroed_flag_for_heap_block_from_environment(
&mut self,
layout_path: &Rc<Path>,
new_layout_expression: &Expression,
) {
if let PathEnum::QualifiedPath { qualifier, .. } = &layout_path.value {
if self.check_for_errors {
let old_layout = self.lookup_path_and_refine_result(
layout_path.clone(),
ExpressionType::NonPrimitive.as_rustc_type(self.tcx),
);
self.check_for_layout_consistency(&old_layout.expression, new_layout_expression);
}
if let PathEnum::HeapBlock { value } = &qualifier.value {
if let Expression::HeapBlock {
abstract_address,
is_zeroed,
} = &value.expression
{
if *is_zeroed {
let new_block = AbstractValue::make_from(
Expression::HeapBlock {
abstract_address: *abstract_address,
is_zeroed: false,
},
1,
);
let new_block_path = Path::get_as_path(new_block);
let mut updated_value_map = self.current_environment.value_map.clone();
for (path, value) in self.current_environment.value_map.iter() {
match &value.expression {
Expression::Reference(p) => {
if *p == *qualifier || p.is_rooted_by(qualifier) {
let new_block_path =
p.replace_root(qualifier, new_block_path.clone());
let new_reference =
AbstractValue::make_reference(new_block_path);
updated_value_map.insert_mut(path.clone(), new_reference);
}
}
Expression::Variable { path: p, var_type } => {
if *p == *qualifier || p.is_rooted_by(qualifier) {
let new_block_path =
p.replace_root(qualifier, new_block_path.clone());
let new_variable = AbstractValue::make_typed_unknown(
*var_type,
new_block_path,
);
updated_value_map.insert_mut(path.clone(), new_variable);
}
}
_ => (),
}
}
self.current_environment.value_map = updated_value_map;
}
}
}
}
}