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/ArincUtil/index.html

Module ArincUtil

val debug_each : string -> unit
type resource =
  1. | Process
  2. | Function
  3. | Semaphore
  4. | Event
  5. | Logbook
  6. | SamplingPort
  7. | QueuingPort
  8. | Buffer
  9. | Blackboard
val show_resource : resource -> Ppx_deriving_runtime.string
type id = resource * string
val infinity : int64
type time = int64
type partition_mode =
  1. | Idle
  2. | Cold_Start
  3. | Warm_Start
  4. | Normal
val show_partition_mode : partition_mode -> Ppx_deriving_runtime.string
val min_partition_mode : int
val max_partition_mode : int
val partition_mode_to_enum : partition_mode -> int
val partition_mode_of_enum : int -> partition_mode option
val show_partition_mode_opt : partition_mode option -> string
val mode_is : (partition_mode -> bool) -> ArincDomain.Pmo.t -> bool
val mode_is_init : ArincDomain.Pmo.t -> bool
val mode_is_multi : ArincDomain.Pmo.t -> bool
type queuing_discipline =
  1. | Fifo
  2. | Prio
val show_queuing_discipline : queuing_discipline -> Ppx_deriving_runtime.string
val min_queuing_discipline : int
val max_queuing_discipline : int
val queuing_discipline_to_enum : queuing_discipline -> int
val queuing_discipline_of_enum : int -> queuing_discipline option
val string_of_queuing_discipline : int64 -> string
type return_code =
  1. | NO_ERROR
  2. | NO_ACTION
  3. | NOT_AVAILABLE
  4. | INVALID_PARAM
  5. | INVALID_CONFIG
  6. | INVALID_MODE
  7. | TIMED_OUT
val show_return_code : return_code -> Ppx_deriving_runtime.string
val min_return_code : int
val max_return_code : int
val return_code_to_enum : return_code -> int
val return_code_of_enum : int -> return_code option
val pname_ErrorHandler : string
module Action : sig ... end
type action =
  1. | Nop
  2. | Cond of string * string
  3. | Assign of string * string
  4. | Call of string
  5. | LockPreemption
  6. | UnlockPreemption
  7. | SetPartitionMode of partition_mode option
  8. | CreateProcess of Action.process
  9. | CreateErrorHandler of id * CilType.Varinfo.t
  10. | Start of id
  11. | Stop of id
  12. | Suspend of id
  13. | SuspendSelf of id * time
  14. | Resume of id
  15. | CreateBlackboard of id
  16. | DisplayBlackboard of id
  17. | ReadBlackboard of id * time
  18. | ClearBlackboard of id
  19. | CreateSemaphore of Action.semaphore
  20. | WaitSemaphore of id * time
  21. | SignalSemaphore of id
  22. | CreateEvent of id
  23. | WaitEvent of id * time
  24. | SetEvent of id
  25. | ResetEvent of id
  26. | TimedWait of time
  27. | PeriodicWait
val show_action : action -> Ppx_deriving_runtime.string
val string_of_node : Basetype.ExtractLocation.t -> string
type edge = node * action * string option * node
val action_of_edge : ('a * 'b * 'c * 'd) -> 'b
val edges : edges Prelude.ref
val get_a : ('a * 'b * 'c * 'd) -> 'a
val get_b : ('a * 'b * 'c * 'd) -> 'd
val marshal : 'a BatInnerIO.output -> unit
val unmarshal : BatInnerIO.input -> unit
val get_edges : id -> edge Prelude.Set.t
val add_edge : id -> edge -> unit
val filter_map_actions : (action -> 'a option) -> 'a list
val filter_actions : (action -> bool) -> action list
val funs_for_process : id -> Cil.varinfo list
module type GenSig = sig ... end
module type SymTblSig = sig ... end
module SymTbl (Gen : GenSig) : SymTblSig with type k = Gen.k and type v = Gen.v
val return_vars : (id * [ `Read | `Write ], string Prelude.Set.t) Prelude.Hashtbl.t
val add_return_var : id -> [ `Read | `Write ] -> string -> unit
val get_return_vars : id -> [ `Read | `Write ] -> string Prelude.Set.t
val decl_return_vars : string Prelude.Set.t -> string list
val is_global : string -> bool
val get_locals : id -> string list
val flatten_set : 'a Prelude.Set.t Prelude.Set.t -> 'a Prelude.Set.t
val get_globals : unit -> string list
val str_resource : id -> string
val str_resources : id list -> string
val str_action : 'a -> action -> Ppx_deriving_runtime.string
val str_return_code : string option -> string
val pml_resources : (resource * string, int64) Prelude.Hashtbl.t
val id_pml : (resource * string) -> int64
val str_id_pml : (resource * string) -> string
val str_pid_pml : (resource * string) -> string
val str_ids_pml : (resource * string) list -> (string -> string) -> string
val unset_ret_vars : string Prelude.Set.t Prelude.ref
val undef_funs : string Prelude.Set.t Prelude.ref
val action_may_fail : action -> bool
val str_action_pml : id -> string option -> action -> string
val find_option : ('a -> bool) -> 'a list -> 'a option
val simplify : unit -> unit
val validate : unit -> unit
val print_actions : unit -> unit
val save_result : string -> string -> string -> unit
val save_dot_graph : unit -> unit
module FunTbl : sig ... end
val save_promela_model : unit -> unit