Module Db.Value.Logic

module Logic: sig .. end

Evaluation of logic terms and predicates




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