Missing Source Snippets in some circumstances

[juliand665]

This is probably not actually the most general case, but with #1249 there's a simple way to produce this error. The following client code will do it:

struct Special {
    x: i32,
}

impl Clone for Special {
    fn clone(&self) -> Self {
        Special { x: self.x + 1 }
    }
}

This violates the postcondition applied to Clone implementers by default through this spec, i.e. ensures(result === x). One would expect to see an error like this:

However, the produced error is actually missing the source snippet of the spec:

One way I've found to bring back this info is to explicitly use prusti_contracts::core_spec::clone; (or anything within the clone module). I don't know enough about how Prusti handles this stuff to come up with a good theory of what's going on, but maybe this insight will set off a lightbulb for someone who knows their way around :)

[fpoli]

This happened to me today. It's not a full explanation, but I noticed that here we register the span of the function instead of the span of the postcondition:

prusti-dev/prusti-viper/src/encoder/procedure_encoder.rs

Lines 4858 to 4866 in 3dd957c

	let func_pos = self.register_error(self.mir.span, ErrorCtxt::AssertMethodPostcondition);
	let patched_func_spec = self.replace_old_places_with_ghost_vars(None, func_spec);
	self.cfg_method.add_stmt(
	return_cfg_block,
	vir::Stmt::Assert( vir::Assert {
	expr: patched_func_spec,
	position: func_pos,
	}),
	);

Usually that span should not matter because Viper should report in the verification error the position of the precise sub-expression in the postcondition that failed. However, if that doesn't happen Prusti will fall-back to the position of the assertion, thus the self.mir.span in the snipped above.