I'd like to add, on top of that, some predicates like 'this memory is initialized'. Potentially also, 'this pointer is valid'. If I get to dream I'd add 'this v

I'd like to add, on top of that, some predicates like 'this memory is initialized'. Potentially also, 'this pointer is valid'. If I get to dream I'd add 'this value is never referenced through a pointer' or 'this is the only expression that can change this field struct'.