cprover
weak_memory.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Weak Memory Instrumentation for Threaded Goto Programs
4 
5 Author: Daniel Kroening
6 
7 Date: September 2011
8 
9 \*******************************************************************/
10 
13 
14 #ifndef CPROVER_GOTO_INSTRUMENT_WMM_WEAK_MEMORY_H
15 #define CPROVER_GOTO_INSTRUMENT_WMM_WEAK_MEMORY_H
16 
17 #include "wmm.h"
18 
19 #include <util/irep.h>
20 
21 class symbol_tablet;
22 class value_setst;
23 class goto_modelt;
24 class message_handlert;
25 class goto_programt;
26 class messaget;
27 
28 void weak_memory(
29  memory_modelt model,
30  value_setst &,
31  goto_modelt &,
32  bool SCC,
33  instrumentation_strategyt event_stategy,
34  unsigned unwinding_bound,
35  bool no_cfg_kill,
36  bool no_dependencies,
37  loop_strategyt duplicate_body,
38  unsigned max_var,
39  unsigned max_po_trans,
40  bool render_po,
41  bool render_file,
42  bool render_function,
43  bool cav11_option,
44  bool hide_internals,
46  bool ignore_arrays);
47 
49  value_setst &,
50  symbol_tablet &,
51  const irep_idt &function,
52  goto_programt &,
53 #ifdef LOCAL_MAY
54  const goto_functionst::goto_functiont &goto_function,
55 #endif
56  messaget &message);
57 
58 #endif // CPROVER_GOTO_INSTRUMENT_WMM_WEAK_MEMORY_H
memory models
instrumentation_strategyt
Definition: wmm.h:26
void weak_memory(memory_modelt model, value_setst &, goto_modelt &, bool SCC, instrumentation_strategyt event_stategy, 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, message_handlert &, bool ignore_arrays)
loop_strategyt
Definition: wmm.h:36
memory_modelt
Definition: wmm.h:17
The symbol table.
Definition: symbol_table.h:19
::goto_functiont goto_functiont
void introduce_temporaries(value_setst &, symbol_tablet &, const irep_idt &function, goto_programt &, messaget &message)
all access to shared variables is pushed into assignments
Definition: weak_memory.cpp:36
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70