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 value_setst;
22 class goto_functionst;
23 class symbol_tablet;
24 class message_handlert;
25 class goto_programt;
26 class messaget;
27 
28 void weak_memory(
29  memory_modelt model,
30  value_setst &value_sets,
31  symbol_tablet &symbol_table,
32  goto_functionst &goto_functions,
33  bool SCC,
34  instrumentation_strategyt event_stategy,
35  unsigned unwinding_bound,
36  bool no_cfg_kill,
37  bool no_dependencies,
38  loop_strategyt duplicate_body,
39  unsigned max_var,
40  unsigned max_po_trans,
41  bool render_po,
42  bool render_file,
43  bool render_function,
44  bool cav11_option,
45  bool hide_internals,
46  message_handlert &message,
47  bool ignore_arrays);
48 
50  value_setst &value_sets,
51  symbol_tablet &symbol_table,
52  const irep_idt &function,
53  goto_programt &goto_program,
54 #ifdef LOCAL_MAY
55  const goto_functionst::goto_functiont &goto_function,
56 #endif
57  messaget &message);
58 
59 #endif // CPROVER_GOTO_INSTRUMENT_WMM_WEAK_MEMORY_H
memory models
instrumentation_strategyt
Definition: wmm.h:26
loop_strategyt
Definition: wmm.h:36
memory_modelt
Definition: wmm.h:17
The symbol table.
Definition: symbol_table.h:52
void introduce_temporaries(value_setst &value_sets, symbol_tablet &symbol_table, const irep_idt &function, goto_programt &goto_program, messaget &message)
all access to shared variables is pushed into assignments
Definition: weak_memory.cpp:38
goto_function_templatet< goto_programt > goto_functiont
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
void weak_memory(memory_modelt model, value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions, 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 &message, bool ignore_arrays)