package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Evaluation of logic terms and predicates

Module `Value.Logic`

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:state ->
    here:state ->
    Cil_types.predicate ->
    Property_status.emitted_status)
    ref

Evaluate the given predicate in the given states for the Pre and Here ACSL labels.

since Neon-20140301