module Aorai_visitors: sig
.. 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. It also takes care of changing the automaton at function's
return.
val dkey : Log.category
val get_acceptance_pred : unit -> Cil_types.predicate
val get_call_name : Cil_types.exp -> string
type
func_auto_mode =
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 Pervasives.ref, Cil_types.stmt Pervasives.ref) 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