sig
exception Empty_automaton
module Aorai_state :
sig
type t = Promelaast.state
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
module Set :
sig
type elt = t
type t
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
val add : elt -> t -> t
val singleton : elt -> t
val remove : elt -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t
val subset : t -> t -> bool
val iter : (elt -> unit) -> t -> unit
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val filter : (elt -> bool) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val cardinal : t -> int
val elements : t -> elt list
val choose : t -> elt
val split : elt -> t -> t * bool * t
val find : elt -> t -> elt
val of_list : elt list -> t
val min_elt : t -> elt
val max_elt : t -> elt
val nearest_elt_le : elt -> t -> elt
val nearest_elt_ge : elt -> t -> elt
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
end
module Map :
sig
type key = t
type +'a t
val empty : 'a t
val is_empty : 'a t -> bool
val mem : key -> 'a t -> bool
val add : key -> 'a -> 'a t -> 'a t
val singleton : key -> 'a -> 'a t
val remove : key -> 'a t -> 'a t
val merge :
(key -> 'a option -> 'b option -> 'c option) ->
'a t -> 'b t -> 'c t
val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val for_all : (key -> 'a -> bool) -> 'a t -> bool
val exists : (key -> 'a -> bool) -> 'a t -> bool
val filter : (key -> 'a -> bool) -> 'a t -> 'a t
val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
val cardinal : 'a t -> int
val bindings : 'a t -> (key * 'a) list
val min_binding : 'a t -> key * 'a
val max_binding : 'a t -> key * 'a
val choose : 'a t -> key * 'a
val split : key -> 'a t -> 'a t * 'a option * 'a t
val find : key -> 'a t -> 'a
val map : ('a -> 'b) -> 'a t -> 'b t
val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
module Key :
sig
type t = key
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
end
module Make :
functor (Data : Datatype.S) ->
sig
type t = Data.t t
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
end
end
module Hashtbl :
sig
type key = t
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
val iter_sorted :
?cmp:(key -> key -> int) -> (key -> 'a -> unit) -> 'a t -> unit
val fold_sorted :
?cmp:(key -> key -> int) ->
(key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val iter_sorted_by_entry :
cmp:(key * 'a -> key * 'a -> int) ->
(key -> 'a -> unit) -> 'a t -> unit
val fold_sorted_by_entry :
cmp:(key * 'a -> key * 'a -> int) ->
(key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val iter_sorted_by_value :
cmp:('a -> 'a -> int) -> (key -> 'a -> unit) -> 'a t -> unit
val fold_sorted_by_value :
cmp:('a -> 'a -> int) ->
(key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val structural_descr : Structural_descr.t -> Structural_descr.t
val make_type : 'a Type.t -> 'a t Type.t
val memo : 'a t -> key -> (key -> 'a) -> 'a
module Key :
sig
type t = key
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
end
module Make :
functor (Data : Datatype.S) ->
sig
type t = Data.t t
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
end
end
end
module Aorai_typed_trans :
sig
type t =
(Promelaast.typed_condition * Promelaast.action) Promelaast.trans
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
module Set :
sig
type elt = t
type t
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
val add : elt -> t -> t
val singleton : elt -> t
val remove : elt -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t
val subset : t -> t -> bool
val iter : (elt -> unit) -> t -> unit
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val filter : (elt -> bool) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val cardinal : t -> int
val elements : t -> elt list
val choose : t -> elt
val split : elt -> t -> t * bool * t
val find : elt -> t -> elt
val of_list : elt list -> t
val min_elt : t -> elt
val max_elt : t -> elt
val nearest_elt_le : elt -> t -> elt
val nearest_elt_ge : elt -> t -> elt
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
end
module Map :
sig
type key = t
type +'a t
val empty : 'a t
val is_empty : 'a t -> bool
val mem : key -> 'a t -> bool
val add : key -> 'a -> 'a t -> 'a t
val singleton : key -> 'a -> 'a t
val remove : key -> 'a t -> 'a t
val merge :
(key -> 'a option -> 'b option -> 'c option) ->
'a t -> 'b t -> 'c t
val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val for_all : (key -> 'a -> bool) -> 'a t -> bool
val exists : (key -> 'a -> bool) -> 'a t -> bool
val filter : (key -> 'a -> bool) -> 'a t -> 'a t
val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
val cardinal : 'a t -> int
val bindings : 'a t -> (key * 'a) list
val min_binding : 'a t -> key * 'a
val max_binding : 'a t -> key * 'a
val choose : 'a t -> key * 'a
val split : key -> 'a t -> 'a t * 'a option * 'a t
val find : key -> 'a t -> 'a
val map : ('a -> 'b) -> 'a t -> 'b t
val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
module Key :
sig
type t = key
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
end
module Make :
functor (Data : Datatype.S) ->
sig
type t = Data.t t
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
end
end
module Hashtbl :
sig
type key = t
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
val iter_sorted :
?cmp:(key -> key -> int) -> (key -> 'a -> unit) -> 'a t -> unit
val fold_sorted :
?cmp:(key -> key -> int) ->
(key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val iter_sorted_by_entry :
cmp:(key * 'a -> key * 'a -> int) ->
(key -> 'a -> unit) -> 'a t -> unit
val fold_sorted_by_entry :
cmp:(key * 'a -> key * 'a -> int) ->
(key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val iter_sorted_by_value :
cmp:('a -> 'a -> int) -> (key -> 'a -> unit) -> 'a t -> unit
val fold_sorted_by_value :
cmp:('a -> 'a -> int) ->
(key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val structural_descr : Structural_descr.t -> Structural_descr.t
val make_type : 'a Type.t -> 'a t Type.t
val memo : 'a t -> key -> (key -> 'a) -> 'a
module Key :
sig
type t = key
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
end
module Make :
functor (Data : Datatype.S) ->
sig
type t = Data.t t
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
end
end
end
val setCData : unit -> unit
val add_logic : string -> Cil_types.logic_info -> unit
val get_logic : string -> Cil_types.logic_info
val add_predicate : string -> Cil_types.logic_info -> unit
val get_predicate : string -> Cil_types.logic_info
val pebble_set_at :
Cil_types.logic_info -> Cil_types.logic_label -> Cil_types.term
val aux_variables : unit -> Cil_types.varinfo list
val abstract_logic_info : unit -> Cil_types.logic_info list
val pand :
Promelaast.condition -> Promelaast.condition -> Promelaast.condition
val por :
Promelaast.condition -> Promelaast.condition -> Promelaast.condition
val pnot : Promelaast.condition -> Promelaast.condition
val cst_one : Promelaast.expression
val cst_zero : Promelaast.expression
val is_cst_one : Promelaast.expression -> bool
val is_cst_zero : Promelaast.expression -> bool
val is_single : Promelaast.seq_elt -> bool
val get_fresh : string -> string
val transStart : string
val transStop : string
val transCond : string
val transCondP : string
val loopInit : string
val curOp : string
val curOpStatus : string
val curState : string
val curStateOld : string
val curTrans : string
val acceptSt : string
val nbOp : string
val nbAcceptSt : string
val nbTrans : string
val macro_ligth : string
val macro_full : string
val macro_pure : string
val get_state_var : Promelaast.state -> Cil_types.varinfo
val get_state_logic_var : Promelaast.state -> Cil_types.logic_var
val listOp : string
val listStatus : string
val callStatus : string
val termStatus : string
val states : string
val buch_sync : string
val new_state : string -> Promelaast.state
val new_trans :
Promelaast.state -> Promelaast.state -> 'a -> 'a Promelaast.trans
val getAutomata : unit -> Promelaast.typed_automaton
val setAutomata : Promelaast.parsed_automaton -> unit
val getNumberOfTransitions : unit -> int
val getNumberOfStates : unit -> int
val getFunctions_from_c : unit -> string list
val getVariables_from_c : unit -> string list
val getIgnoredFunctions : unit -> string list
val addIgnoredFunction : string -> unit
val isIgnoredFunction : string -> bool
val getState : int -> Promelaast.state
val getStateName : int -> string
val is_reject_state : Promelaast.state -> bool
val getTransition :
int -> (Promelaast.typed_condition * Promelaast.action) Promelaast.trans
val set_varinfo : string -> Cil_types.varinfo -> unit
val get_varinfo : string -> Cil_types.varinfo
val get_varinfo_option : string -> Cil_types.varinfo option
val get_logic_var : string -> Cil_types.logic_var
val set_paraminfo : string -> string -> Cil_types.varinfo -> unit
val get_paraminfo : string -> string -> Cil_types.varinfo
val set_returninfo : string -> Cil_types.varinfo -> unit
val get_returninfo : string -> Cil_types.varinfo
val find_max_value : Cil_types.term -> Cil_types.term option
type range =
Fixed of int
| Interval of int * int
| Bounded of int * Cil_types.term
| Unbounded of int
module Range :
sig
type t = range
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
module Set :
sig
type elt = t
type t
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
val add : elt -> t -> t
val singleton : elt -> t
val remove : elt -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t
val subset : t -> t -> bool
val iter : (elt -> unit) -> t -> unit
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val filter : (elt -> bool) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val cardinal : t -> int
val elements : t -> elt list
val choose : t -> elt
val split : elt -> t -> t * bool * t
val find : elt -> t -> elt
val of_list : elt list -> t
val min_elt : t -> elt
val max_elt : t -> elt
val nearest_elt_le : elt -> t -> elt
val nearest_elt_ge : elt -> t -> elt
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
end
module Map :
sig
type key = t
type +'a t
val empty : 'a t
val is_empty : 'a t -> bool
val mem : key -> 'a t -> bool
val add : key -> 'a -> 'a t -> 'a t
val singleton : key -> 'a -> 'a t
val remove : key -> 'a t -> 'a t
val merge :
(key -> 'a option -> 'b option -> 'c option) ->
'a t -> 'b t -> 'c t
val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val for_all : (key -> 'a -> bool) -> 'a t -> bool
val exists : (key -> 'a -> bool) -> 'a t -> bool
val filter : (key -> 'a -> bool) -> 'a t -> 'a t
val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
val cardinal : 'a t -> int
val bindings : 'a t -> (key * 'a) list
val min_binding : 'a t -> key * 'a
val max_binding : 'a t -> key * 'a
val choose : 'a t -> key * 'a
val split : key -> 'a t -> 'a t * 'a option * 'a t
val find : key -> 'a t -> 'a
val map : ('a -> 'b) -> 'a t -> 'b t
val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
module Key :
sig
type t = key
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
end
module Make :
functor (Data : Datatype.S) ->
sig
type t = Data.t t
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
end
end
module Hashtbl :
sig
type key = t
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
val iter_sorted :
?cmp:(key -> key -> int) -> (key -> 'a -> unit) -> 'a t -> unit
val fold_sorted :
?cmp:(key -> key -> int) ->
(key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val iter_sorted_by_entry :
cmp:(key * 'a -> key * 'a -> int) ->
(key -> 'a -> unit) -> 'a t -> unit
val fold_sorted_by_entry :
cmp:(key * 'a -> key * 'a -> int) ->
(key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val iter_sorted_by_value :
cmp:('a -> 'a -> int) -> (key -> 'a -> unit) -> 'a t -> unit
val fold_sorted_by_value :
cmp:('a -> 'a -> int) ->
(key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val structural_descr : Structural_descr.t -> Structural_descr.t
val make_type : 'a Type.t -> 'a t Type.t
val memo : 'a t -> key -> (key -> 'a) -> 'a
module Key :
sig
type t = key
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
end
module Make :
functor (Data : Datatype.S) ->
sig
type t = Data.t t
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
end
end
end
module Intervals :
sig
type t = range Cil_datatype.Term.Map.t
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
end
module Vals :
sig
type t = Intervals.t Cil_datatype.Term.Map.t
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
end
val absolute_range : Cil_types.term -> int -> Data_for_aorai.Range.t
val merge_range :
Cil_types.term ->
Cil_types.term ->
Data_for_aorai.Range.t ->
Data_for_aorai.Range.t -> Data_for_aorai.Range.t
val tlval : Cil_types.term_lval -> Cil_types.term
type end_state =
(Data_for_aorai.Aorai_state.Set.t * Data_for_aorai.Aorai_state.Set.t *
Data_for_aorai.Vals.t)
Data_for_aorai.Aorai_state.Map.t
module Case_state :
sig
type t = end_state Aorai_state.Map.t
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
end
type state = Data_for_aorai.Case_state.t
val pretty_end_state :
Data_for_aorai.Aorai_state.t ->
Format.formatter -> Data_for_aorai.end_state -> unit
val pretty_state : Format.formatter -> Data_for_aorai.state -> unit
val included_state : Data_for_aorai.state -> Data_for_aorai.state -> bool
val merge_bindings :
Data_for_aorai.Vals.t -> Data_for_aorai.Vals.t -> Data_for_aorai.Vals.t
val merge_end_state :
Data_for_aorai.end_state ->
Data_for_aorai.end_state -> Data_for_aorai.end_state
val merge_state :
Data_for_aorai.state -> Data_for_aorai.state -> Data_for_aorai.state
val set_kf_init_state : Kernel_function.t -> Data_for_aorai.state -> unit
val set_kf_return_state : Kernel_function.t -> Data_for_aorai.state -> unit
val set_loop_init_state : Cil_types.stmt -> Data_for_aorai.state -> unit
val set_loop_invariant_state :
Cil_types.stmt -> Data_for_aorai.state -> unit
val replace_kf_init_state :
Kernel_function.t -> Data_for_aorai.state -> unit
val replace_kf_return_state :
Kernel_function.t -> Data_for_aorai.state -> unit
val replace_loop_init_state :
Cil_types.stmt -> Data_for_aorai.state -> unit
val replace_loop_invariant_state :
Cil_types.stmt -> Data_for_aorai.state -> unit
val get_kf_init_state : Kernel_function.t -> Data_for_aorai.state
val get_kf_return_state : Kernel_function.t -> Data_for_aorai.state
val get_loop_init_state : Cil_types.stmt -> Data_for_aorai.state
val get_loop_invariant_state : Cil_types.stmt -> Data_for_aorai.state
val debug_computed_state : ?dkey:Log.category -> unit -> unit
val get_cenum_option : string -> Cil_types.constant option
val func_enum_type : unit -> Cil_types.typ
val status_enum_type : unit -> Cil_types.typ
val func_to_cenum : string -> Cil_types.constant
val op_status_to_cenum : Promelaast.funcStatus -> Cil_types.constant
val func_to_op_func : string -> string
val set_usedinfo : string -> Cil_types.enuminfo -> unit
val get_usedinfo : string -> Cil_types.enuminfo
val removeUnusedTransitionsAndStates : unit -> unit
end