package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

Parameters

module C : 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

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

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