cprover
|
#include "pensieve.h"
#include <util/cprover_prefix.h>
#include <util/namespace.h>
#include <util/message.h>
#include <goto-programs/remove_skip.h>
#include <goto-instrument/rw_set.h>
#include <goto-instrument/wmm/instrumenter_pensieve.h>
Go to the source code of this file.
Functions | |
void | fence_pensieve (value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions, unsigned unwinding_bound, unsigned input_max_po_trans, bool render_po, bool render_file, bool render_function, bool naive_mode, message_handlert &message_handler) |
void fence_pensieve | ( | value_setst & | value_sets, |
symbol_tablet & | symbol_table, | ||
goto_functionst & | goto_functions, | ||
unsigned | unwinding_bound, | ||
unsigned | input_max_po_trans, | ||
bool | render_po, | ||
bool | render_file, | ||
bool | render_function, | ||
bool | naive_mode, | ||
message_handlert & | message_handler | ||
) |
Definition at line 19 of file pensieve.cpp.
References instrumenter_pensievet::collect_pairs(), instrumenter_pensievet::collect_pairs_naive(), CPROVER_PREFIX, goto_functions_templatet< goto_programt >::entry_point(), messaget::eom(), Forall_goto_functions, instrumentert::goto2graph_cfg(), introduce_temporaries(), no_loop, Power, remove_skip(), instrumentert::set_parameters_collection(), messaget::status(), and goto_functions_templatet< bodyT >::update().
Referenced by goto_fence_inserter_parse_optionst::instrument_goto_program().