Module `ArincUtil`

val debug_each : string -> unit

type resource =

| Process
| Function
| Semaphore
| Event
| Logbook
| SamplingPort
| QueuingPort
| Buffer
| Blackboard

val pp_resource : 
  Ppx_deriving_runtime.Format.formatter ->
  resource ->
  Ppx_deriving_runtime.unit

val show_resource : resource -> Ppx_deriving_runtime.string

type id = resource * string

val pp_id : 
  Ppx_deriving_runtime.Format.formatter ->
  id ->
  Ppx_deriving_runtime.unit

val show_id : id -> Ppx_deriving_runtime.string

val infinity : int64

type time = int64

val pp_time : 
  Ppx_deriving_runtime.Format.formatter ->
  time ->
  Ppx_deriving_runtime.unit

val show_time : time -> Ppx_deriving_runtime.string

type partition_mode =

| Idle
| Cold_Start
| Warm_Start
| Normal

val pp_partition_mode : 
  Ppx_deriving_runtime.Format.formatter ->
  partition_mode ->
  Ppx_deriving_runtime.unit

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 =

| Fifo
| Prio

val pp_queuing_discipline : 
  Ppx_deriving_runtime.Format.formatter ->
  queuing_discipline ->
  Ppx_deriving_runtime.unit

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 =

| NO_ERROR
| NO_ACTION
| NOT_AVAILABLE
| INVALID_PARAM
| INVALID_CONFIG
| INVALID_MODE
| TIMED_OUT

val pp_return_code : 
  Ppx_deriving_runtime.Format.formatter ->
  return_code ->
  Ppx_deriving_runtime.unit

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 =

| Nop
| Cond of string * string
| Assign of string * string
| Call of string
| LockPreemption
| UnlockPreemption
| SetPartitionMode of partition_mode option
| CreateProcess of Action.process
| CreateErrorHandler of id * CilType.Varinfo.t
| Start of id
| Stop of id
| Suspend of id
| SuspendSelf of id * time
| Resume of id
| CreateBlackboard of id
| DisplayBlackboard of id
| ReadBlackboard of id * time
| ClearBlackboard of id
| CreateSemaphore of Action.semaphore
| WaitSemaphore of id * time
| SignalSemaphore of id
| CreateEvent of id
| WaitEvent of id * time
| SetEvent of id
| ResetEvent of id
| TimedWait of time
| PeriodicWait

val pp_action : 
  Ppx_deriving_runtime.Format.formatter ->
  action ->
  Ppx_deriving_runtime.unit

val show_action : action -> Ppx_deriving_runtime.string

type node = ArincDomain.Pred.Base.t

val string_of_node : Basetype.ExtractLocation.t -> string

type edge = node * action * string option * node

val action_of_edge : ('a * 'b * 'c * 'd) -> 'b

type edges = (id, edge Prelude.Set.t) Prelude.Hashtbl.t

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

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/goblint.lib/ArincUtil/index.html

Module `ArincUtil`

package goblint

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/goblint.lib/ArincUtil/index.html

Module ArincUtil

dune-project
Dependency

Module `ArincUtil`