package goblint

  1. Overview
  2. Docs
package goblint
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Goblint_lib.Cilfacade

GoblintCil utilities.

module E = GoblintCil.Errormsg

Cilfacade functions to avoid dependency cycles.

val get_labelLoc : GoblintCil.label -> GoblintCil.location
val get_labelsLoc : GoblintCil.label list -> GoblintCil.Cil.location

Following functions are similar to Cil versions, but return expression location instead of entire statement location, where possible.

val eloc_fallback : eloc:GoblintCil.location -> loc:GoblintCil.location -> GoblintCil.location
val get_instrLoc : GoblintCil.instr -> GoblintCil.location

Get expression location for Cil.instr.

val get_stmtLoc : GoblintCil.stmt -> GoblintCil.Cil.location

Get expression location for Cil.stmt.

val create_var : GoblintCil.varinfo -> GoblintCil.varinfo

Command for assigning an id to a varinfo. All varinfos directly created by Goblint should be modified by this method

val isCharType : GoblintCil.Cil.typ -> bool

Is character type (N1570 6.2.5.15)?

val isFloatType : GoblintCil.Cil.typ -> bool
val isVLAType : GoblintCil.Cil.typ -> bool
val is_first_field : GoblintCil.fieldinfo -> bool
val init_options : unit -> unit
val init : unit -> unit
val current_file : GoblintCil.file ref
val parse : Fpath.t -> GoblintCil__.Cil.file
  • raises GoblintCil.FrontC.ParseError
  • raises GoblintCil.Errormsg.Error
val print : GoblintCil.file -> unit
val rmTemps : GoblintCil__.Cil.file -> unit
val visitors : (string * (GoblintCil.fundec -> GoblintCil.cilVisitor)) list ref
val register_preprocess : string -> (GoblintCil.fundec -> GoblintCil.cilVisitor) -> unit
val do_preprocess : GoblintCil.file -> unit
val getAST : Fpath.t -> GoblintCil__.Cil.file
  • raises GoblintCil.FrontC.ParseError
  • raises GoblintCil.Errormsg.Error
class addConstructors : GoblintCil.fundec list -> object ... end
val getMergedAST : GoblintCil__.Cil.file list -> GoblintCil__.Cil.file
  • raises GoblintCil.Errormsg.Error
val callConstructors : GoblintCil.file -> GoblintCil.file
val in_section : (string -> bool) -> GoblintCil.attribute list -> bool
val is_init : GoblintCil.attribute list -> bool
val is_exit : GoblintCil.attribute list -> bool
type startfuns = GoblintCil.fundec list * GoblintCil.fundec list * GoblintCil.fundec list
val getFuns : GoblintCil.file -> startfuns
val getFirstStmt : GoblintCil.fundec -> GoblintCil.stmt
val get_ikind : GoblintCil.Cil.typ -> GoblintCil.ikind
val get_fkind : GoblintCil.Cil.typ -> GoblintCil.fkind
val ptrdiff_ikind : unit -> GoblintCil.ikind
val ptr_ikind : unit -> GoblintCil.ikind

Cil.typeOf, etc reimplemented to raise sensible exceptions instead of printing all errors directly...

type typeOfError =
  1. | RealImag_NonNumerical
    (*

    unexpected non-numerical type for argument to __real__/__imag__

    *)
  2. | StartOf_NonArray
    (*

    typeOf: StartOf on a non-array

    *)
  3. | Mem_NonPointer of GoblintCil.exp
    (*

    typeOfLval: Mem on a non-pointer (exp)

    *)
  4. | Index_NonArray of GoblintCil.exp * GoblintCil.typ
    (*

    typeOffset: Index on a non-array

    *)
  5. | Field_NonCompound of GoblintCil.fieldinfo * GoblintCil.typ
    (*

    typeOffset: Field on a non-compound

    *)
exception TypeOfError of typeOfError
val stringLiteralType : GoblintCil.typ ref
val typeOfRealAndImagComponents : GoblintCil.typ -> GoblintCil.typ
val isComplexFKind : GoblintCil.fkind -> bool
val typeOf : GoblintCil.exp -> GoblintCil.typ
val typeOfInit : GoblintCil.init -> GoblintCil.typ
val typeOfLval : GoblintCil.lval -> GoblintCil.typ
val typeOffset : GoblintCil.typ -> GoblintCil.offset -> GoblintCil.typ
val mkCast : e:GoblintCil.exp -> newt:GoblintCil.typ -> GoblintCil.Cil.exp

Cil.mkCast using our typeOf.

val get_ikind_exp : GoblintCil.exp -> GoblintCil.ikind
val get_fkind_exp : GoblintCil.exp -> GoblintCil.fkind
val makeBinOp : GoblintCil__.Cil.binop -> GoblintCil.exp -> GoblintCil.exp -> GoblintCil__.Cil.exp

Make Cil.BinOp with correct implicit casts inserted.

val anoncomp_name_regexp : Str.regexp
val split_anoncomp_name : string -> bool * string * int
val pretty_typsig_like_typ : unit -> GoblintCil.typsig -> GoblintCil__.Pretty.doc

Pretty-print typsig like typ, because d_typsig prints with CIL constructors.

val locs : (int, unit) Hashtbl.t

HashSet of line numbers

class countFnVisitor : object ... end

Visitor to count locs appearing inside a fundec.

val fnvis : countFnVisitor
val countLoc : GoblintCil.fundec -> int

Count the number of unique locations appearing in fundec fn. Uses Cilfacade.locs hashtable for intermediate computations

val fundec_return_type : GoblintCil.fundec -> GoblintCil.typ
module StmtH : sig ... end
val stmt_fundecs : GoblintCil.fundec StmtH.t ResettableLazy.t
val pseudo_return_to_fun : GoblintCil.fundec StmtH.t
val find_stmt_fundec : StmtH.key -> GoblintCil.fundec

Find fundec which the stmt is in.

module VarinfoH : sig ... end
val varinfo_fundecs : GoblintCil.fundec VarinfoH.t ResettableLazy.t
val find_varinfo_fundec : VarinfoH.key -> GoblintCil.fundec

Find fundec by the function's varinfo (has the function name and type).

module StringH : sig ... end
val name_fundecs : GoblintCil.fundec StringH.t ResettableLazy.t
val find_name_fundec : StringH.key -> GoblintCil.fundec

Find fundec by the function's name.

type varinfo_role =
  1. | Formal of GoblintCil.fundec
  2. | Local of GoblintCil.fundec
  3. | Function
  4. | Global
val find_varinfo_role : VarinfoH.key -> varinfo_role

Find the role of the varinfo.

val is_varinfo_formal : VarinfoH.key -> bool
val find_scope_fundec : VarinfoH.key -> GoblintCil.fundec option

Find the scope of the varinfo. If varinfo is a local or a formal argument of fundec, then returns Some fundec. If varinfo is a global or a function itself, then returns None.

val original_names : string VarinfoH.t ResettableLazy.t
val find_original_name : VarinfoH.key -> string option

Find the original name (in input source code) of the varinfo. If it was renamed by CIL, then returns the original name before renaming. If it wasn't renamed by CIL, then returns the same name. If it was inserted by CIL (or Goblint), then returns None.

module IntH : sig ... end
class stmtSidVisitor : GoblintCil.stmt IntH.t -> object ... end
val stmt_sids : GoblintCil.stmt IntH.t ResettableLazy.t
val pseudo_return_stmt_sids : GoblintCil.stmt IntH.t
val find_stmt_sid : IntH.key -> GoblintCil.stmt

Find stmt by its sid.

val reset_lazy : unit -> unit
val stmt_pretty_short : unit -> GoblintCil.stmt -> GoblintCil__.Pretty.doc
val add_function_declarations : GoblintCil.Cil.file -> unit

Given a Cil.file, reorders its globals, inserts function declarations before function definitions. This function may be used after a code transformation to ensure that the order of globals yields a compilable program.