PV4 ⊧ MetAcslchecks high-level ACSL requirements by propagating them across the codebase

a Frama-C plugin for specification and verification of high-level properties. Quoting their website:

MetAcsl is a plug-in dedicated to specifying and verifying high-level ACSL requirements (HILARE), that is, properties that are supposed to be checked at many points of the code base under analysis, so that writing the corresponding ACSL annotations manually would be extremely tedious and error-prone.

Expected input

• a target: the set of functions where the HILARE should hold;
• a context: the kind of program points that are concerned by the HILARE;
• the property itself: an ACSL predicate, possibly enriched with meta-variables