Module Aorai_utils

module Aorai_utils: sig .. end

Given a transition a function and a function status (call or return) it returns if the cross condition can be satisfied with only function status.

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.

Given a transition a function 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

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 isCrossableAtInit : (Promelaast.typed_condition * Promelaast.action) Promelaast.trans ->
       Cil_types.kernel_function -> bool

Given a transition and the main entry point it returns if the cross condition can be satisfied at the beginning of the program.

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.

Globals management

val initFile : Cil_types.file -> unit

Copy the file pointer locally in the class in order to easiest globals management and initializes some tables.

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

Given the name of the main function, this function computes all newly introduced globals (variables, enumeration structure, invariants, etc.)

This function computes all newly introduced globals (variables, enumeration structure, invariants, etc.

Pre/post management

Pre/post management

Pre and post condition of C functions In our point of view, the pre or the post condition of a C function are defined by the set of states authorized just before/after the call, as such as the set of crossable transitions. The following functions generates abstract pre and post-conditions by using only informations deduced from the buchi automata.

val host_state_term : unit -> Cil_types.term_lval

base lhost corresponding to curState.

Returns a lval term associated to the curState generated variable.

val is_state_pred : Promelaast.state -> Cil_types.predicate

Returns the predicate saying that automaton is in corresponding state.

val is_state_stmt : Promelaast.state * Cil_types.varinfo -> Cil_types.location -> Cil_types.stmt

Returns the statement saying the state is affected

val is_state_exp : Promelaast.state -> Cil_types.location -> Cil_types.exp

Returns the boolean expression saying the state is affected

val is_out_of_state_pred : Promelaast.state -> Cil_types.predicate

Returns the predicate saying that automaton is NOT in corresponding state.

val is_out_of_state_stmt : Promelaast.state * Cil_types.varinfo -> Cil_types.location -> Cil_types.stmt

Returns the statement saying the automaton is not in the corresponding state.
Raises 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 active

val is_out_of_state_exp : Promelaast.state -> Cil_types.location -> Cil_types.exp

Returns the expression testing that automaton is NOT in the corresponding state.

val aorai_assigns : Data_for_aorai.state -> Cil_types.location -> Cil_types.assigns

returns assigns clause corresponding to updating automaton's state, and assigning auxiliary variable depending on the possible transitions made in the function.
Since Neon-20140301 adds kf argument

val force_transition : Cil_types.location ->
       Cil_types.kernel_function ->
       Promelaast.funcStatus ->
       Data_for_aorai.state -> Cil_types.identified_predicate list

returns the list of predicates expressing that for each current state the automaton currently is in, there is at least one transition that is crossed.

val auto_func_preconditions : Cil_types.location ->
       Cil_types.kernel_function ->
       Promelaast.funcStatus ->
       Data_for_aorai.state -> Cil_types.identified_predicate list

return list of preconditions for the given auxiliary function (f_pre_func or f_post_func).

val auto_func_behaviors : Cil_types.location ->
       Cil_types.kernel_function ->
       Promelaast.funcStatus -> Data_for_aorai.state -> Cil_types.funbehavior list

auto_func_behaviors f st (st_status, tr_status) generates behaviors corresponding to the transitions authorized by tr_status for function f in status st
Since Nitrogen-20111001

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

Returns a list of predicate giving for each possible start state the disjunction of possible current states

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

Possible values of the given auxiliary variable under the current path, starting from the given point
Since Neon-20140301 add logic_label argument

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

for a given starting and ending state, returns the post-conditions related to the possible values of the auxiliary variables at current point the function, guarded by the fact that we have followed this path, from the given program point
Change in Neon-20130301: add logic_label argument

val all_actions_preds : Cil_types.logic_label -> Data_for_aorai.state -> Cil_types.predicate list

All actions that might have been performed on aux variables from the given program point, guarded by the path followed.
Change in Neon-20140301: add logic_label argument

val zero_term : unit -> Cil_types.term

Deprecated.use directly Cil.lzero
Return an integer constant term with the 0 value.

Return an integer constant term with the 0 value.

val mk_offseted_array : Cil_types.term_lval -> int -> Cil_types.term

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

Given an lval term 'host' and an integer value 'off', it returns a lval term hostoff.

val mk_term_from_vi : Cil_types.varinfo -> Cil_types.term

Returns a term representing the given logic variable (usually a fresh quantified variable).

Returns a term representing the variable associated to the given varinfo

val make_enum_states : unit -> unit