Module `Goblintutil`

Globally accessible flags and utility functions.

Outputs information about what the goblin is doing

val jsonFiles : string list ref

Json files that are given as arguments

val should_warn : bool ref

If this is true we output messages and collect accesses. This is set to true in control.ml before we verify the result (or already before solving if warn = 'early')

val svcomp_may_overflow : bool ref

Whether signed overflow or underflow happened

val inthack : int64

hack to use a special integer to denote synchronized array-based locking

val globals_changed : int ref

number of times that globals change !CAUTION: This is only set in contain.ml and is not what one would think it is!

val out : out_channel ref

The file where everything is output

val tempDirName : string ref

Temp directory, set in maingoblint.ml, but used by the OSEK analysis.

val create_var : Cil.varinfo -> Cil.varinfo

Command for assigning an id to a varinfo. All varinfos directly created by Goblint should be modified by this method

val type_inv_tbl : (int, Cil.varinfo) Hashtbl.t

val type_inv : Cil.compinfo -> Cil.varinfo

val is_blessed : Cil.typ -> Cil.varinfo option

val global_initialization : bool ref

A hack to see if we are currently doing global inits

val earlyglobs : bool ref

Another hack to see if earlyglobs is enabled

val postsolving : bool ref

Whether currently in postsolver evaluations (e.g. verify, warn)

val verified : bool option ref

val escape : string -> string

val create_dir : string -> string

Creates a directory and returns the absolute path *

val rm_rf : string -> unit

Remove directory and its content, as "rm -rf" would do.

type name =

| Cons
| Dest
| Name of string
| Unknown of string
| Template of name
| Nested of name * name
| PtrTo of name
| TypeFun of string * name

val name_to_string_hlp : name -> string

val name_to_string : name -> string

val special : Str.regexp

val dem_prefix : Str.regexp

val num_prefix : Str.regexp

val ti_prefix : Str.regexp

val tv_prefix : Str.regexp

val ts_prefix : Str.regexp

val tt_prefix : Str.regexp

val nested : Str.regexp

val nested_std_t : Str.regexp

val nested_std_a : Str.regexp

val nested_std_s : Str.regexp

val strlift : Str.regexp

val templ : Str.regexp

val const : Str.regexp

val ptr_to : Str.regexp

val constructor : Str.regexp

val destructor : Str.regexp

val varlift : Str.regexp

val take : int -> string -> string

val drop : int -> string -> string

val appp : ('a -> 'b) -> ('a * 'c) -> 'b * 'c

val op_name : string -> string

val num_p : string -> name list * string

val conv : string -> name * string

val to_name : string -> name

val get_class : string -> string option

val get_class_and_name : string -> (string * string) option

val demangle : string -> string

exception Timeout

val timeout : ('a -> 'b) -> 'a -> float -> (unit -> unit) -> 'b

val seconds_of_duration_string : string -> int

val vars : int ref

val evals : int ref

val print_gc_quick_stat : out_channel -> Gc.stat

val scrambled : bool

val arinc_name : string

val arinc_entry_point : string

val arinc_base_priority : string

val arinc_period : string

val arinc_time_capacity : string

val exe_dir : string

val command : string

val opt_predicate : ('a -> bool) -> 'a option -> bool

val signal_of_string : string -> int

val self_signal : int -> unit

val zip : 'a list -> 'b list -> ('a * 'b) list

val for_all_in_range : 
  (IntOps.BigIntOpsBase.t * IntOps.BigIntOpsBase.t) ->
  (IntOps.BigIntOpsBase.t -> bool) ->
  bool

val assoc_eq : 'a -> ('a * 'b) list -> ('a -> 'a -> bool) -> 'b option

val dummy_obj : Obj.t

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/goblint.lib/Goblintutil/index.html

Module `Goblintutil`

package goblint

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/goblint.lib/Goblintutil/index.html

Module Goblintutil

dune-project
Dependency

Module `Goblintutil`