Skip to content

Adding check-callee-assigns option

The added -meta-check-callee-assigns option allows to enforce the treatment of -meta-check-ext for listed functions (with or without a body). More precisely, for a listed function called from a non-listed function, writing meta-propreties are instantiated at the callsite based on the assigns clauses of the callee, and reading meta-propreties are instantiated based on the \from clauses of the callee.

Merge request reports

Loading