Cilfacade (goblint.Cilfacade)

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.

type Goblint_backtrace.mark +=

| FunVarinfo of GoblintCil.varinfo

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 isBoolType : GoblintCil.Cil.typ -> bool

val isFloatType : GoblintCil.Cil.typ -> bool

val isVLAType : GoblintCil.Cil.typ -> bool

val isStructOrUnionType : 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 =

| RealImag_NonNumerical
(*
unexpected non-numerical type for argument to __real__/__imag__
*)
| StartOf_NonArray
(*
typeOf: StartOf on a non-array
*)
| Mem_NonPointer of GoblintCil.exp
(*
typeOfLval: Mem on a non-pointer (exp)
*)
| Index_NonArray of GoblintCil.exp * GoblintCil.typ
(*
typeOffset: Index on a non-array
*)
| 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 bytesSizeOf : GoblintCil.typ -> int

val bytesOffsetOnly : GoblintCil.typ -> GoblintCil.offset -> int

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 =

| Formal of GoblintCil.fundec
| Local of GoblintCil.fundec
| Function
| Global

val varinfo_roles : varinfo_role VarinfoH.t ResettableLazy.t

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.