Value.Logic
The APIs of this module are not stabilized yet, and are subject to change between Frama-C versions.
val eval_predicate :
( pre:state ->
here:state ->
Cil_types.predicate ->
Property_status.emitted_status )
Stdlib.ref
Evaluate the given predicate in the given states for the Pre and Here ACSL labels.