cprover
pensieve.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Fence insertion following criteria of Pensieve (PPoPP'05)
4 
5 Author: Vincent Nimal
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_MUSKETEER_PENSIEVE_H
13 #define CPROVER_MUSKETEER_PENSIEVE_H
14 
17 
18 class value_setst;
19 class goto_functionst;
20 class symbol_tablet;
21 class message_handlert;
22 
23 void fence_pensieve(
24  value_setst &value_sets,
25  symbol_tablet &symbol_table,
26  goto_functionst &goto_functions,
27  unsigned unwinding_bound,
28  unsigned max_po_trans,
29  bool render_po,
30  bool render_file,
31  bool render_function,
32  bool naive_mode,
33  message_handlert &message_handler);
34 
35 #endif // CPROVER_MUSKETEER_PENSIEVE_H
memory models
Weak Memory Instrumentation for Threaded Goto Programs.
void fence_pensieve(value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions, unsigned unwinding_bound, unsigned max_po_trans, bool render_po, bool render_file, bool render_function, bool naive_mode, message_handlert &message_handler)
Definition: pensieve.cpp:19
The symbol table.
Definition: symbol_table.h:52