package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c.kernel/Frama_c_kernel/Logic_typing/Make/index.html

Module `Logic_typing.Make`

Parameters

module _ : sig ... end

Signature

val type_of_field : 
  Cil_types.location ->
  string ->
  Cil_types.logic_type ->
  Cil_types.term_offset * Cil_types.logic_type

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

val conditional_conversion : 
  Cil_types.location ->
  Logic_ptree.relation option ->
  Cil_types.term ->
  Cil_types.term ->
  Cil_types.logic_type

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

val term : Lenv.t -> Logic_ptree.lexpr -> Cil_types.term

type-checks a term.

val predicate : Lenv.t -> Logic_ptree.lexpr -> Cil_types.predicate

val code_annot : 
  Cil_types.location ->
  string list ->
  Cil_types.logic_type ->
  Logic_ptree.code_annot ->
  Cil_types.code_annotation

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 type_annot : 
  Cil_types.location ->
  Logic_ptree.type_annot ->
  Cil_types.logic_info

val model_annot : 
  Cil_types.location ->
  Logic_ptree.model_annot ->
  Cil_types.model_info

val annot : Logic_ptree.decl -> Cil_types.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

On This Page

Parameters
Signature