Index of classes

C
change_formals [Aorai_visitors]
change_result [Aorai_visitors]
V
visit_adding_code_for_synchronisation [Aorai_visitors]

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.

visit_adding_pre_post_from_buch [Aorai_visitors]

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