sig
val isCrossable :
(Promelaast.typed_condition * Promelaast.action) Promelaast.trans ->
Cil_types.kernel_function -> Promelaast.funcStatus -> bool
val isCrossableAtInit :
(Promelaast.typed_condition * Promelaast.action) Promelaast.trans ->
Cil_types.kernel_function -> bool
val crosscond_to_pred :
Promelaast.typed_condition ->
Cil_types.kernel_function -> Promelaast.funcStatus -> Cil_types.predicate
val initFile : Cil_types.file -> unit
val initGlobals : Cil_types.kernel_function -> bool -> unit
val host_state_term : unit -> Cil_types.term_lval
val is_state_pred : Promelaast.state -> Cil_types.predicate
val is_state_stmt :
Promelaast.state * Cil_types.varinfo ->
Cil_types.location -> Cil_types.stmt
val is_state_exp : Promelaast.state -> Cil_types.location -> Cil_types.exp
val is_out_of_state_pred : Promelaast.state -> Cil_types.predicate
val is_out_of_state_stmt :
Promelaast.state * Cil_types.varinfo ->
Cil_types.location -> Cil_types.stmt
val is_out_of_state_exp :
Promelaast.state -> Cil_types.location -> Cil_types.exp
val aorai_assigns :
Data_for_aorai.state ->
Cil_types.location -> Cil_types.identified_term Cil_types.assigns
val force_transition :
Cil_types.location ->
Cil_types.kernel_function ->
Promelaast.funcStatus ->
Data_for_aorai.state -> Cil_types.identified_predicate list
val auto_func_preconditions :
Cil_types.location ->
Cil_types.kernel_function ->
Promelaast.funcStatus ->
Data_for_aorai.state -> Cil_types.identified_predicate list
val auto_func_behaviors :
Cil_types.location ->
Cil_types.kernel_function ->
Promelaast.funcStatus ->
Data_for_aorai.state -> Cil_types.funbehavior list
val auto_func_block :
Cil_types.location ->
Cil_types.kernel_function ->
Promelaast.funcStatus ->
Data_for_aorai.state ->
Cil_types.varinfo option -> Cil_types.block * Cil_types.varinfo list
val get_preds_pre_wrt_params :
Cil_types.kernel_function -> Cil_types.predicate
val get_preds_post_bc_wrt_params :
Cil_types.kernel_function -> Cil_types.predicate
val possible_states_preds :
Data_for_aorai.state -> Cil_types.predicate list
val update_to_pred :
start:Cil_types.logic_label ->
pre_state:Promelaast.state ->
post_state:Promelaast.state ->
Cil_types.term -> Data_for_aorai.Intervals.t -> Cil_types.predicate
val action_to_pred :
start:Cil_types.logic_label ->
pre_state:Promelaast.state ->
post_state:Promelaast.state ->
Data_for_aorai.Vals.t -> Cil_types.predicate list
val all_actions_preds :
Cil_types.logic_label -> Data_for_aorai.state -> Cil_types.predicate list
val zero_term : unit -> Cil_types.term
val mk_offseted_array : Cil_types.term_lval -> int -> Cil_types.term
val mk_offseted_array_states_as_enum :
Cil_types.term_lval -> int -> Cil_types.term
val mk_term_from_vi : Cil_types.varinfo -> Cil_types.term
val make_enum_states : unit -> unit
end