cprover
fence_assert.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: ILP construction for cycles affecting user-assertions
4
and resolution
5
6
Author: Vincent Nimal
7
8
\*******************************************************************/
9
12
13
#include "
fence_assert.h
"
14
15
bool
fence_assert_insertert::find_assert
(
16
const
event_grapht::critical_cyclet
&cycle)
const
17
{
18
/* TODO */
19
return
true
;
20
}
21
22
void
fence_assert_insertert::process_cycles_selection
()
23
{
24
for
(std::set<event_grapht::critical_cyclet>::const_iterator
25
C_j=
instrumenter
.
set_of_cycles
.begin();
26
C_j!=
instrumenter
.
set_of_cycles
.end();
27
++C_j)
28
{
29
if
(
find_assert
(*C_j) )
30
selected_cycles
.insert(C_j->id);
31
}
32
}
fence_assert_insertert::process_cycles_selection
virtual void process_cycles_selection()
Definition:
fence_assert.cpp:22
fence_assert_insertert::find_assert
bool find_assert(const event_grapht::critical_cyclet &cycle) const
Definition:
fence_assert.cpp:15
fence_assert.h
ILP construction for cycles affecting user-assertions and resolution.
fence_assert_insertert::selected_cycles
std::set< unsigned > selected_cycles
Definition:
fence_assert.h:27
fence_insertert::instrumenter
instrumentert & instrumenter
Definition:
fence_inserter.h:65
instrumentert::set_of_cycles
std::set< event_grapht::critical_cyclet > set_of_cycles
Definition:
goto2graph.h:289
event_grapht::critical_cyclet
Definition:
event_graph.h:38
musketeer
fence_assert.cpp
Generated by
1.8.14