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 (10)

Authors

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

Maintainers

  1. M
    Michael Schwarz <michael.schwarz93@gmail.com>
  2. S
    Simmo Saan <simmo.saan@gmail.com>
  3. R
    Ralf Vogler <ralf.vogler@gmail.com>

Sources

goblint-1.1.1.tbz
sha256=999272bfbd3b9b96fcd58987b237ac6e9fa6d92ef935cc89f1ea2b4205185141
sha512=f3bf6ab71cf8c258d3290da4bf9f6fe42d7c671822e0efeb0fc50afdff078ab15e352237e5c1db31c5aa3a9d430691268ed2e5e00da10f2615835f672f91683d

doc/goblint.lib/Cilfacade/index.html

Module Cilfacade

Helpful functions for dealing with Cil.

module E = Errormsg
module GU = Goblintutil
val get_labelLoc : Cil.label -> Cil.location
val get_labelsLoc : Cil.label list -> Cil.location
val get_stmtkindLoc : Cil.stmtkind -> Cil.location
val get_stmtLoc : Cil.stmt -> Cil.location
val init : unit -> unit
val current_statement : Cil.stmt ref
val current_file : Cil.file ref
val showtemps : bool ref
val parse : string -> Cil.file
val print_to_file : string -> Cil.file -> unit
val print : Cil.file -> unit
val printDebug : Cil.file -> unit
val rmTemps : Cil.file -> unit
class allBBVisitor : object ... end
val end_basic_blocks : Cil.file -> unit
val visitors : (string * (Cil.fundec -> Cil.cilVisitor)) list ref
val register_preprocess : string -> (Cil.fundec -> Cil.cilVisitor) -> unit
val do_preprocess : Cil.file -> unit
val createCFG : Cil.file -> unit
val getAST : string -> Cil.file
class addConstructors : Cil.fundec list -> object ... end
val getMergedAST : Cil.file list -> Cil.file
val callConstructors : Cil.file -> Cil.file
val in_section : (string -> bool) -> Cil.attribute list -> bool
val is_init : Cil.attribute list -> bool
val is_initptr : Cil.attribute list -> bool
val is_exit : Cil.attribute list -> bool
val get_varinfo : Cil.exp -> Cil.varinfo
exception MyException of Cil.varinfo
val find_module_init : Cil.fundec list -> Cil.file -> Cil.fundec list * Cil.fundec list
type startfuns = Cil.fundec list * Cil.fundec list * Cil.fundec list
val getFuns : Cil.file -> startfuns
val getFirstStmt : Cil.fundec -> Cil.stmt
val pstmt : Cil.stmt -> unit
val p_expr : Cil.exp -> Pretty.doc
val d_expr : Cil.exp -> Pretty.doc
val get_ikind : Cil.typ -> Cil.ikind
val ptrdiff_ikind : unit -> Cil.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 Cil.exp
    (*

    typeOfLval: Mem on a non-pointer (exp)

    *)
  4. | Index_NonArray
    (*

    typeOffset: Index on a non-array

    *)
  5. | Field_NonCompound
    (*

    typeOffset: Field on a non-compound

    *)
exception TypeOfError of typeOfError
val stringLiteralType : Cil.typ ref
val typeOfRealAndImagComponents : Cil.typ -> Cil.typ
val typeOf : Cil.exp -> Cil.typ
val typeOfInit : Cil.init -> Cil.typ
val typeOfLval : Cil.lval -> Cil.typ
val typeOffset : Cil.typ -> Cil.offset -> Cil.typ
val get_ikind_exp : Cil.exp -> Cil.ikind
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 : Cil.fundec -> int

Count the number of unique locations appearing in fundec fn. Uses Cilfacade.locs hashtable for intermediate computations

val fundec_return_type : Cil.fundec -> Cil.typ
module StmtH : sig ... end
val stmt_fundecs : Cil.fundec StmtH.t Lazy.t
val pseudo_return_to_fun : Cil.fundec StmtH.t
val find_stmt_fundec : StmtH.key -> Cil.fundec

Find fundec which the stmt is in.

module VarinfoH : sig ... end
val varinfo_fundecs : Cil.fundec VarinfoH.t Lazy.t
val find_varinfo_fundec : VarinfoH.key -> Cil.fundec

Find fundec by the function's varinfo (has the function name and type).

module StringH : sig ... end
val name_fundecs : Cil.fundec StringH.t Lazy.t
val find_name_fundec : StringH.key -> Cil.fundec

Find fundec by the function's name.

type varinfo_role =
  1. | Formal of Cil.fundec
  2. | Local of Cil.fundec
  3. | Function
  4. | Global
val varinfo_roles : varinfo_role VarinfoH.t Lazy.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 -> Cil.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 Lazy.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.

val stmt_pretty_short : unit -> Cil.stmt -> Pretty.doc