cprover
|
#include <fence_assert.h>
Public Member Functions | |
fence_assert_insertert (instrumentert &instr) | |
fence_assert_insertert (instrumentert &instr, memory_modelt _model) | |
![]() | |
unsigned | add_edge (const edget &e) |
unsigned | add_invisible_edge (const edget &e) |
fence_insertert (instrumentert &instr) | |
fence_insertert (instrumentert &instr, memory_modelt _model) | |
void | compute () |
void | print_to_file () |
void | print_to_file_2 () |
void | print_to_file_3 () |
void | print_to_file_4 () |
typet | get_type (const irep_idt &id) |
typet | type_component (std::list< std::string >::const_iterator it, std::list< std::string >::const_iterator end, const typet &type) |
Protected Member Functions | |
bool | find_assert (const event_grapht::critical_cyclet &cycle) const |
virtual void | process_cycles_selection () |
virtual bool | filter_cycles (unsigned cycles_id) const |
![]() | |
void | mip_set_var (ilpt &ilp, unsigned &i) |
void | mip_set_cst (ilpt &ilp, unsigned &i) |
void | mip_fill_matrix (ilpt &ilp, unsigned &i, unsigned const_constraints_number, unsigned const_unique) |
void | preprocess () |
void | solve () |
virtual unsigned | fence_cost (fence_typet e) const |
std::string | to_string (fence_typet f) const |
unsigned | col_to_var (unsigned u) const |
fence_typet | col_to_fence (unsigned u) const |
unsigned | var_fence_to_col (fence_typet f, unsigned var) const |
void | import_freq () |
void | compute_fence_options () |
void | print_vars () const |
Protected Attributes | |
std::set< unsigned > | selected_cycles |
![]() | |
unsigned & | unique |
unsigned | fence_options |
mip_vart | var |
mip_vart | invisible_var |
std::set< event_idt > | po |
std::list< std::set< event_idt > > | powr_constraints |
std::list< std::set< event_idt > > | poww_constraints |
std::list< std::set< event_idt > > | porw_constraints |
std::list< std::set< event_idt > > | porr_constraints |
std::list< std::set< event_idt > > | com_constraints |
cycles_visitort | cycles_visitor |
const float | epsilon |
const bool | with_freq |
std::map< unsigned, float > | freq_table |
std::map< edget, fence_typet > | fenced_edges |
Additional Inherited Members | |
![]() | |
typedef event_grapht::critical_cyclet::delayt | edget |
![]() | |
static std::string | remove_extra (const irep_idt &id) |
static std::string | remove_extra (std::string copy) |
![]() | |
instrumentert & | instrumenter |
std::map< unsigned, edget > & | map_to_e |
normal variables used almost every time More... | |
std::map< edget, unsigned > & | map_from_e |
std::size_t | constraints_number |
number of constraints More... | |
const memory_modelt | model |
const_graph_visitort | const_graph_visitor |
to retrieve the concrete graph edges involved in the (abstract) cycles More... | |
![]() | |
enum | fence_typet { Fence =0, Dp =1, Lwfence =2, Branching =3, Ctlfence =4 } |
Definition at line 24 of file fence_assert.h.
|
inlineexplicit |
Definition at line 41 of file fence_assert.h.
|
inline |
Definition at line 46 of file fence_assert.h.
|
inlineprotectedvirtual |
Reimplemented from fence_insertert.
Definition at line 35 of file fence_assert.h.
|
protected |
Definition at line 15 of file fence_assert.cpp.
Referenced by process_cycles_selection().
|
protectedvirtual |
Reimplemented from fence_insertert.
Definition at line 22 of file fence_assert.cpp.
References find_assert(), fence_insertert::instrumenter, selected_cycles, and instrumentert::set_of_cycles.
|
protected |
Definition at line 27 of file fence_assert.h.
Referenced by process_cycles_selection().