package goblint

  1. Overview
  2. Docs
Static analysis framework for C

Install 

dune-project
 Dependency

goblint.in.tum.de Readme Changelog Edit opam file Versions (9)

Authors

  1. S
    Simmo Saan
  2. M
    Michael Schwarz
  3. J
    Julian Erhard
  4. S
    Sarah Tilscher
  5. R
    Ralf Vogler
  6. K
    Kalmer Apinis
  7. V
    Vesal Vojdani

Maintainers

  1. S
    Simmo Saan <simmo.saan@gmail.com>
  2. M
    Michael Schwarz <michael.schwarz93@gmail.com>

Sources

goblint-2.3.0.tbz
sha256=b729c94adb383a39aea32eb005c988dfd44b92af22ee6a4eedf4239542ac6c26
sha512=643b98770e5fe5644324c95c9ae3a9f698f25c8b11b298f0751d524e0b20af368b2a465fc8200b75a73d48fc9a053fd90f5e8920d4db070927f93188bb8687e0

doc/goblint.common/Cilfacade/index.html

Module Cilfacade

GoblintCil utilities.

include module type of struct include Cilfacade0 end

Cilfacade functions to avoid dependency cycles.

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.

Get expression location for Cil.instr.

Get expression location for Cil.stmt.

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
  • raises GoblintCil.FrontC.ParseError
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
  • raises GoblintCil.FrontC.ParseError
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 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 typeOfInit : GoblintCil.init -> GoblintCil.typ
val typeOfLval : GoblintCil.lval -> GoblintCil.typ
val typeBlendAttributes : GoblintCil.attributes -> GoblintCil.typ -> GoblintCil.typ
val typeSigBlendAttributes : GoblintCil.attributes -> GoblintCil.typsig -> GoblintCil.typsig

Cil.mkCast using our typeOf.

val get_ikind_exp : GoblintCil.exp -> GoblintCil.ikind
val get_fkind_exp : GoblintCil.exp -> GoblintCil.fkind

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) 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 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 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 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 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
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.