Frama-C:
Plug-ins:
Libraries:

Frama-C API - Logic_subst

Substitution of formals in terms and predicates. These operations are intended for replacing formal parameters by actual ones in terms or predicates occurring in a C function pre-conditions at call site.

  • since Frama-C 33.0-Arsenic
val term : Cil_types.varinfo list -> Cil_types.exp list -> Cil_types.term -> Cil_types.term option

term xs es t substitutes in term t formal parameters xs with actual parameters es and move Pre labels to Here. Returns None if the transposition cannot be performed. This is the case when an actual parameter is missing or when the address of formal is taken.

Same as function term for predicates.

Same as function term for identified predicates.