Module Cilfacade

GoblintCil utilities.

module E = GoblintCil.Errormsg
include module type of struct include Cilfacade0 end

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 Stdlib.ref
val parse : Fpath.t -> GoblintCil__.Cil.file
  • raises GoblintCil.FrontC.ParseError
  • raises GoblintCil.Errormsg.Error
class cleanCilPrinterClass : object ... end

Version of defaultCilPrinterClass which excludes line directives and builtin signatures (in comments). Used for dbg.justcil-printer.

val cleanCilPrinter : cleanCilPrinterClass
val cleanDumpFile : GoblintCil.cilPrinter -> Stdlib.out_channel -> string -> GoblintCil.file -> unit
val print : GoblintCil.file -> unit
val rmTemps : GoblintCil__.Cil.file -> unit
val visitors : (string * (GoblintCil.fundec -> GoblintCil.cilVisitor)) list Stdlib.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

Returns the ikind of a TInt(_) and TEnum(_). Unrolls typedefs.

  • raises Invalid_argument

    if not integral type.

val get_fkind : GoblintCil.Cil.typ -> GoblintCil.fkind
  • raises Invalid_argument

    if not floating-point type.

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 Stdlib.ref
val typeOfRealAndImagComponents : GoblintCil.typ -> GoblintCil.typ
  • raises TypeOfError
val isComplexFKind : GoblintCil.fkind -> bool
val typeOf : GoblintCil.exp -> GoblintCil.typ
  • raises TypeOfError
val typeOfInit : GoblintCil.init -> GoblintCil.typ
  • raises TypeOfError
val typeOfLval : GoblintCil.lval -> GoblintCil.typ
  • raises TypeOfError
val typeOffset : GoblintCil.typ -> GoblintCil.offset -> GoblintCil.typ
  • raises TypeOfError
val typeBlendAttributes : GoblintCil.attributes -> GoblintCil.typ -> GoblintCil.typ
val typeSigBlendAttributes : GoblintCil.attributes -> GoblintCil.typsig -> GoblintCil.typsig
val mkCast : e:GoblintCil.exp -> newt:GoblintCil.typ -> GoblintCil.Cil.exp

Cil.mkCast using our typeOf.

val get_ikind_exp : GoblintCil.exp -> GoblintCil.ikind
  • raises TypeOfError
  • raises Invalid_argument

    if not integral type.

val get_fkind_exp : GoblintCil.exp -> GoblintCil.fkind
  • raises TypeOfError
  • raises Invalid_argument

    if not floating-point type.

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 option * 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) Stdlib.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 get_pseudo_return_id : GoblintCil.fundec -> int
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.

  • raises Not_found
module FunLocH : sig ... end
module LocSet : sig ... end
val funs_with_upjumping_gotos : unit LocSet.t FunLocH.t

Contains the locations of the upjumping gotos and the respective functions * they are being called in.

val reset_lazy : ?keepupjumpinggotos:bool -> 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.

val any_index_exp : GoblintCil.exp lazy_t

Special index expression for some unknown index. Weakly updates array in assignment. Used for exp.fast_global_inits.