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  bool no_cfg_kill,
35  bool no_dependencies,
36  loop_strategyt duplicate_body,
37  unsigned max_var,
38  unsigned max_po_trans,
39  bool render_po,
40  bool render_file,
41  bool render_function,
42  bool cav11_option,
43  bool hide_internals,
45  bool ignore_arrays);
46 
48  value_setst &,
49  symbol_tablet &,
50  const irep_idt &function,
51  goto_programt &,
52 #ifdef LOCAL_MAY
53  const goto_functionst::goto_functiont &goto_function,
54 #endif
55  messaget &message);
56 
57 #endif // CPROVER_GOTO_INSTRUMENT_WMM_WEAK_MEMORY_H
void weak_memory(memory_modelt model, value_setst &, goto_modelt &, bool SCC, instrumentation_strategyt event_stategy, 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)
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:19
::goto_functiont goto_functiont
Class that provides messages with a built-in verbosity &#39;level&#39;.
Definition: message.h:144
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
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:72