Frama-C:
Plug-ins:
Libraries:

Frama-C API - Infer_assigns

Generation of possible assigns from the C prototype of a function.

val from_prototype : Kernel_function.t -> Cil_types.from list
val from_prototype_vi : Cil_types.varinfo -> Cil_types.from list

Same as from_prototype but given a varinfo instead of a kernel function.

  • since Frama-C+dev