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-project

Dependency

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

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-28.0-Nickel.tar.gz

sha256=29612882330ecb6eddd0b4ca3afc0492b70d0feb3379a1b8e893194c6e173983

doc/frama-c.kernel/Frama_c_kernel/Cil_const/index.html

Module `Frama_c_kernel.Cil_const`

Smart constructors for some CIL data types

val voidType : Cil_types.typ

module CurrentLoc : State_builder.Ref with type data = Cil_types.location

forward reference to current location (see Cil.CurrentLoc)

module Vid : sig ... end

module Sid : sig ... end

module Eid : sig ... end

val set_vid : Cil_types.varinfo -> unit

set the vid to a fresh number.

val copy_with_new_vid : Cil_types.varinfo -> Cil_types.varinfo

returns a copy of the varinfo with a fresh vid. If the varinfo has an associated logic var, a copy of the logic var is made as well.

val change_varinfo_name : Cil_types.varinfo -> string -> unit

change_varinfo_name vi name changes the name of vi to name. Takes care of renaming the associated logic_var if any.

since Oxygen-20120901

val new_raw_id : unit -> int

Generate a new ID. This will be different than any variable ID that is generated by Cil.makeLocalVar and friends. Must not be used for setting vid: use set_vid instead.

val mkCompInfo : 
  bool ->
  string ->
  ?norig:string ->
  (Cil_types.compinfo ->
    (string
     * Cil_types.typ
     * int option
     * Cil_types.attributes
     * Cil_types.location)
      list
      option) ->
  Cil_types.attributes ->
  Cil_types.compinfo

Creates a (potentially recursive) composite type. The arguments are: (1) a boolean indicating whether it is a struct or a union, (2) the name (always non-empty), (3) a function that when given a representation of the structure type constructs the type of the fields recursive type (the first argument is only useful when some fields need to refer to the type of the structure itself), and (4) an optional list of attributes to be associated with the composite type, "None" means that the struct is incomplete.

since 23.0-Vanadium the 4th parameter is a function that returns an option.

val copyCompInfo : 
  ?fresh:bool ->
  Cil_types.compinfo ->
  string ->
  Cil_types.compinfo

Makes a shallow copy of a Cil_types.compinfo changing the name. It also copies the fields, and makes sure that the copied field points back to the copied compinfo. If fresh is true (the default), it will also give a fresh id to the copy.

val make_logic_var_kind : 
  string ->
  Cil_types.logic_var_kind ->
  Cil_types.logic_type ->
  Cil_types.logic_var

Create a fresh logical variable giving its name, type and origin.

since Fluorine-20130401

val make_logic_var_global : 
  string ->
  Cil_types.logic_type ->
  Cil_types.logic_var

Create a new global logic variable

since Fluorine-20130401

val make_logic_var_formal : 
  string ->
  Cil_types.logic_type ->
  Cil_types.logic_var

Create a new formal logic variable

since Fluorine-20130401

val make_logic_var_quant : 
  string ->
  Cil_types.logic_type ->
  Cil_types.logic_var

Create a new quantified logic variable

since Fluorine-20130401

val make_logic_var_local : 
  string ->
  Cil_types.logic_type ->
  Cil_types.logic_var

Create a new local logic variable

since Fluorine-20130401

val make_logic_info : string -> Cil_types.logic_info

Create a fresh logical (global) variable giving its name and type.

val make_logic_info_local : string -> Cil_types.logic_info

Create a new local logic variable given its name.

since Fluorine-20130401