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
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
weak_memory
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)
Definition: weak_memory.cpp:107
goto_modelt
Definition: goto_model.h:26
loop_strategyt
loop_strategyt
Definition: wmm.h:37
message
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
Definition: static_verifier.cpp:74
introduce_temporaries
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:38
message_handlert
Definition: message.h:28
memory_modelt
memory_modelt
Definition: wmm.h:18
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
value_setst
Definition: value_sets.h:22
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instrumentation_strategyt
instrumentation_strategyt
Definition: wmm.h:27
wmm.h
memory models
irep.h