sig
  val eval_predicate :
    (pre:Db.Value.state ->
     here:Db.Value.state ->
     Cil_types.predicate Cil_types.named -> Property_status.emitted_status)
    Pervasives.ref
end