cprover
fencer.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Fence inference
4 
5 Author: Vincent Nimal
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_MUSKETEER_FENCER_H
13 #define CPROVER_MUSKETEER_FENCER_H
14 
17 
18 #include "infer_mode.h"
19 
20 class message_handlert;
21 class value_setst;
22 class goto_functionst;
23 class symbol_tablet;
24 
26  memory_modelt model,
27  value_setst &value_sets,
28  symbol_tablet &symbol_table,
29  goto_functionst &goto_functions,
30  bool SCC,
31  instrumentation_strategyt event_strategy,
32  unsigned unwinding_bound,
33  bool no_cfg_kill,
34  bool no_dependencies,
35  loop_strategyt duplicate_body,
36  unsigned max_var,
37  unsigned max_po_trans,
38  bool render_po,
39  bool render_file,
40  bool render_function,
41  bool cav11_option,
42  bool hide_internals,
43  bool print_graph,
44  infer_modet mode,
45  message_handlert &message_handler,
46  bool ignore_arrays);
47 
48 #endif // CPROVER_MUSKETEER_FENCER_H
memory models
instrumentation_strategyt
Definition: wmm.h:26
Weak Memory Instrumentation for Threaded Goto Programs.
loop_strategyt
Definition: wmm.h:36
memory_modelt
Definition: wmm.h:17
The symbol table.
Definition: symbol_table.h:52
void fence_weak_memory(memory_modelt model, value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions, bool SCC, instrumentation_strategyt event_strategy, 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, bool print_graph, infer_modet mode, message_handlert &message_handler, bool ignore_arrays)
Definition: fencer.cpp:25
infer_modet
Definition: infer_mode.h:13