Build_pred_or_term.S
A unified signature for building terms and expressions. Not to be confused with Analyses_types.pred_or_term
, which simply is the sum of both types, while here separate modules are provided for predicates and terms.
val mk_false : Frama_c_kernel.Cil_types.logic_type option -> t
val mk_true : Frama_c_kernel.Cil_types.logic_type option -> t
val mk_logic_body : t -> Frama_c_kernel.Cil_types.logic_body
val mk_let :
?loc:Frama_c_kernel.Cil_types.location ->
Frama_c_kernel.Cil_types.logic_info ->
t ->
t
val mk_if :
?loc:Frama_c_kernel.Cil_types.location ->
Frama_c_kernel.Cil_types.predicate ->
t ->
t ->
t
val mk_at : Frama_c_kernel.Cil_types.logic_label -> t -> t
val visit : Frama_c_kernel.Visitor.frama_c_visitor -> t -> t