package goblint
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=452d8491527aea21f2cbb11defcc14ba0daf9fdb6bdb9fc0af73e56eac57b916
sha512=1993cd45c4c7fe124ca6e157f07d17ec50fab5611b270a434ed1b7fb2910aa85a8e6eaaa77dad770430710aafb2f6d676c774dd33942d921f23e2f9854486551
doc/goblint.common/Cilfacade/index.html
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 current_file : GoblintCil.file Stdlib.ref
val parse : Fpath.t -> GoblintCil.Cil.file
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
class addConstructors : GoblintCil.fundec list -> object ... end
val getMergedAST : GoblintCil.Cil.file list -> GoblintCil.Cil.file
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.
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 =
| 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
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 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
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 pretty_typsig_like_typ : unit -> GoblintCil.typsig -> GoblintCil.Pretty.doc
Pretty-print typsig like typ, because d_typsig
prints with CIL constructors.
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.
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
.
module FunLocH : sig ... end
module LocSet : sig ... end
Contains the locations of the upjumping gotos and the respective functions * they are being called in.
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
.