Module Aorai_visitors

module Aorai_visitors: sig .. end

val dkey : Aorai_option.category
val get_acceptance_pred : unit -> Cil_types.predicate
val get_call_name : Cil_types.exp -> string
type func_auto_mode = 
| Not_auto_func
| Pre_func of Cil_types.kernel_function
| Post_func of Cil_types.kernel_function
val func_orig_table : func_auto_mode Cil_datatype.Varinfo.Hashtbl.t
val kind_of_func : Cil_datatype.Varinfo.Hashtbl.key -> func_auto_mode
val mk_auto_fct_block : Kernel_function.t ->
Promelaast.funcStatus ->
Data_for_aorai.state ->
Cil_types.varinfo option -> Cil_types.block * Cil_types.varinfo list
val mk_pre_fct_block : Kernel_function.t -> Cil_types.block * Cil_types.varinfo list
val mk_post_fct_block : Kernel_function.t ->
Cil_types.varinfo option -> Cil_types.block * Cil_types.varinfo list
class visit_adding_code_for_synchronisation : object .. end

This visitor adds an auxiliary function for each C function which takes care of setting the automaton in a correct state before calling the original one, and replaces each occurrence of the original function by the auxiliary one.

class change_formals : Kernel_function.t -> Kernel_function.t -> object .. end
class change_result : Kernel_function.t -> object .. end
val post_treatment_loops : (Cil_datatype.Stmt.t Stdlib.ref, Cil_types.stmt Stdlib.ref) Stdlib.Hashtbl.t
val update_loop_assigns : Cil_types.kernel_function ->
Cil_datatype.Stmt.t ->
Data_for_aorai.state ->
Cil_types.logic_var -> Cil_types.code_annotation -> unit
val get_action_post_cond : Kernel_function.t ->
?init_trans:Data_for_aorai.Aorai_state.Set.t Data_for_aorai.Aorai_state.Map.t ->
(Data_for_aorai.Aorai_state.Set.t * 'a * Data_for_aorai.Vals.t)
Data_for_aorai.Aorai_state.Map.t Data_for_aorai.Aorai_state.Map.t ->
(Cil_types.termination_kind * Cil_types.identified_predicate) list
val make_zero_one_choice : 'a Data_for_aorai.Aorai_state.Map.t -> Cil_types.predicate list
val needs_zero_one_choice : 'a Data_for_aorai.Aorai_state.Map.t -> Cil_types.identified_predicate list
val pred_reachable : 'a Data_for_aorai.Aorai_state.Map.t ->
bool * Cil_types.predicate * Cil_types.predicate
val possible_start : Cil_types.kernel_function ->
Promelaast.state * Promelaast.state -> Cil_types.predicate
val neg_trans : Cil_types.kernel_function ->
(Data_for_aorai.Aorai_state.t * Promelaast.state) list -> Cil_types.predicate
val get_unchanged_aux_var : Cil_types.location ->
('a * 'b * 'c Cil_datatype.Term.Map.t) Data_for_aorai.Aorai_state.Map.t
Data_for_aorai.Aorai_state.Map.t ->
(Cil_types.termination_kind * Cil_types.identified_predicate) list
class visit_adding_pre_post_from_buch : bool -> object .. end

This visitor adds a specification to each function and to each loop, according to specifications stored into Data_for_aorai.

val add_pre_post_from_buch : Cil_types.file -> bool -> unit
val add_sync_with_buch : Cil_types.file -> unit