cprover
|
Fence inference. More...
#include <goto-instrument/wmm/wmm.h>
#include <goto-instrument/wmm/weak_memory.h>
#include "infer_mode.h"
Go to the source code of this file.
Functions | |
void | fence_weak_memory (memory_modelt model, value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions, bool SCC, instrumentation_strategyt event_strategy, unsigned unwinding_bound, bool no_cfg_kill, bool no_dependencies, loop_strategyt duplicate_body, unsigned max_var, unsigned max_po_trans, bool render_po, bool render_file, bool render_function, bool cav11_option, bool hide_internals, bool print_graph, infer_modet mode, message_handlert &message_handler, bool ignore_arrays) |
Fence inference.
Definition in file fencer.h.
void fence_weak_memory | ( | memory_modelt | model, |
value_setst & | value_sets, | ||
symbol_tablet & | symbol_table, | ||
goto_functionst & | goto_functions, | ||
bool | SCC, | ||
instrumentation_strategyt | event_strategy, | ||
unsigned | unwinding_bound, | ||
bool | no_cfg_kill, | ||
bool | no_dependencies, | ||
loop_strategyt | duplicate_body, | ||
unsigned | max_var, | ||
unsigned | max_po_trans, | ||
bool | render_po, | ||
bool | render_file, | ||
bool | render_function, | ||
bool | cav11_option, | ||
bool | hide_internals, | ||
bool | print_graph, | ||
infer_modet | mode, | ||
message_handlert & | message_handler, | ||
bool | ignore_arrays | ||
) |
Definition at line 25 of file fencer.cpp.
References instrumentert::cfg_cycles_filter(), instrumentert::collect_cycles(), instrumentert::collect_cycles_by_SCCs(), fence_insertert::compute(), CPROVER_PREFIX, instrumentert::egraph, instrumentert::egraph_SCCs, goto_functions_templatet< goto_programt >::entry_point(), messaget::eom(), Forall_goto_functions, instrumentert::goto2graph_cfg(), INFER, introduce_temporaries(), instrumentert::num_sccs, event_grapht::print_graph(), instrumentert::print_map_function_graph(), instrumentert::print_outputs(), fence_insertert::print_to_file_3(), remove_skip(), instrumentert::set_of_cycles, instrumentert::set_of_cycles_per_SCC, instrumentert::set_parameters_collection(), instrumentert::set_rendering_options(), messaget::status(), goto_functions_templatet< bodyT >::update(), USER_ASSERT, and USER_DEF.
Referenced by goto_fence_inserter_parse_optionst::instrument_goto_program().