module Aorai_utils:sig
..end
Given a transition a function name and a function status (call or
return) it returns if the cross condition can be satisfied with
only function status.
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
Given a transition a function name and a function status (call or return)
it returns if the cross condition can be satisfied with only
function status.
val crosscond_to_pred : Promelaast.typed_condition ->
Cil_types.kernel_function -> Promelaast.funcStatus -> Cil_types.predicate
This function rewrites a cross condition into an ACSL expression.
Moreover, by giving current operation name and its status (call or
return) the generation simplifies the generated expression.
val initFile : Cil_types.file -> unit
Copy the file pointer locally in the class in order to ease globals
management and initializes some tables.
val initGlobals : Cil_types.kernel_function -> bool -> unit
This function computes all newly introduced globals (variables, enumeration structure, invariants, etc.
val host_state_term : unit -> Cil_types.term_lval
Returns a lval term associated to the curState generated variable.
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
AbortFatal
in the deterministic case, as such an assignment is
meaningless in this context: we only assign the state variable to be
in the (unique by definition) state currently activeval 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
auto_func_block loc f status st res
generates the body of pre & post functions.
res must be None
for a pre-function and Some v
for a post-func where
v
is the formal corresponding to the value returned by the original
function. If the original function returns Void
, res
must be None
.
It also returns the local variables list declared in the body.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
start
ing from the given pointval 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
Return an integer constant term with the 0 value.
val mk_offseted_array : Cil_types.term_lval -> int -> Cil_types.term
off
.
Given an lval term 'host' and an integer value 'off', it returns a lval term hostoff
.
val mk_offseted_array_states_as_enum : Cil_types.term_lval -> int -> Cil_types.term
off
.val mk_term_from_vi : Cil_types.varinfo -> Cil_types.term
Returns a term representing the variable associated to the given varinfo
val make_enum_states : unit -> unit