Consistency of uses of \from clauses
This issue describes a certain inconsistency in usages of the \from
clauses in different plugins.
WP relies on \from
clauses to facilitate pointer analysis for correct memory model assumptions.
This feature is very helpful.
MetAcsl relies on (assigns
and in particular) \from
clauses to instantiate metaproperties
for callees based on their contracts. This can be used for undefined functions or in some cases
for defined functions for better performances of the global proof. This feature is also very helpful.
There is a certain inconsistency of both usages on the same code: only a base address is necessary for the first usage, while a complete list of dependencies is expected in the second case.
It would be desirable to avoid the usage of the same clause in two different ways.
One suggestion can be to use another clause like \from_ptr
or \from_base
for the first case.