package goblint
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=dba2b664c7c125687e708e871d83fbfb6ba6d9ee98d235b4850d9a238caa84de
sha512=529987cde39691ad9e955000a3603e89c1c8cf14ed5e8b4cd3a7fc26e47d016aff571b472e2329725133c46f8d0cb45a05b88994eeffaa221a4d31b4c543adcd
doc/goblint.lib/Goblint_lib/Cilfacade/index.html
Module Goblint_lib.Cilfacade
Helpful functions for dealing with Cil
.
module GU = Goblintutil
include module type of struct include Cilfacade0 end
Cilfacade functions to avoid dependency cycles.
Following functions are similar to Cil
versions, but return expression location instead of entire statement location, where possible.
val parse : Fpath.t -> GoblintCil__.Cil.file
class allBBVisitor : object ... end
class patchLabelsGotosVisitor : (GoblintCil.stmt -> GoblintCil.stmt option) -> object ... end
module StatementHashTable : sig ... end
class copyandPatchLabelsVisitor : (GoblintCil.stmt Stdlib.ref * GoblintCil.stmt Stdlib.ref Stdlib.ref) -> object ... end
class loopUnrollingVisitor : object ... end
val getAST : Fpath.t -> GoblintCil__.Cil.file
class addConstructors : GoblintCil.fundec list -> object ... end
val getFuns : GoblintCil.file -> startfuns
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
(*typeOffset: Index on a non-array
*)| Field_NonCompound
(*typeOffset: Field on a non-compound
*)
exception TypeOfError of typeOfError
Cil.mkCast
using our typeOf
.
Make Cil.BinOp
with correct implicit casts inserted.
class countFnVisitor : object ... end
Visitor to count locs appearing inside a fundec.
val fnvis : countFnVisitor
Count the number of unique locations appearing in fundec fn
. Uses Cilfacade.locs
hashtable for intermediate computations
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.
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
.