Frama-C:
Plug-ins:
Libraries:

Frama-C API - Make

Parameters

module _ : sig ... end

Signature

  • since Nitrogen-20111001
val mk_cast : ?explicit:bool -> Cil_types.term -> Cil_types.logic_type -> Cil_types.term
  • parameter explicit

    true if the cast is present in original source. defaults to false

  • since Nitrogen-20111001

conditional_conversion loc rel t1 t2 tries to find a common type between two terms, either as part of a comparison or a conditional. comparisons can notably introduce logic coercions to Real, potentially with a warning if acsl-float-compare is active.

  • parameter loc

    the location of the comparison. Can be used in error/warning msg

  • parameter rel

    the relation, or None for a conditional

  • parameter t1

    first term

  • parameter t2

    second term

  • since 27.0-Cobalt

type-checks a term.

code_annot loc behaviors rt annot type-checks an in-code annotation.

  • parameter loc

    current location

  • parameter behaviors

    list of existing behaviors

  • parameter rt

    return type of current function

  • parameter annot

    the annotation

Some logic declaration might not introduce new global annotations (eg. already imported external modules).

  • before 30.0-Zinc

    always return a global annotation

val funspec : string list -> Cil_types.varinfo -> Cil_types.varinfo list option -> Cil_types.typ -> Logic_ptree.spec -> Cil_types.funspec

funspec behaviors f prms typ spec type-checks a function contract.

  • parameter behaviors

    list of existing behaviors (outside of the current spec, e.g. in the spec of the corresponding declaration when type-checking the spec of a definition)

  • parameter f

    the function

  • parameter prms

    its parameters

  • parameter its

    type

  • parameter spec

    the spec to typecheck