cprover
fence_shared.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: (naive) Fence insertion
4 
5 Purpose: fences all the shared or volatile-declared variables
6 
7 Author: Vincent Nimal
8 
9 \*******************************************************************/
10 
13 
14 #ifndef CPROVER_MUSKETEER_FENCE_SHARED_H
15 #define CPROVER_MUSKETEER_FENCE_SHARED_H
16 
17 class value_setst;
18 class goto_functionst;
19 class symbol_tablet;
20 class message_handlert;
21 
22 /* finds all the shared variables (including static, global and dynamic) */
23 void fence_all_shared(
24  message_handlert &message_handler,
25  value_setst &value_sets,
26  symbol_tablet &symbol_table,
27  goto_functionst &goto_functions);
28 
29 /* finds all the shared variables (including static, global and dynamic) */
31  message_handlert &message_handler,
32  value_setst &value_sets,
33  symbol_tablet &symbol_table,
34  goto_functionst &goto_functions);
35 
36 /* finds all the volatile-declared variables */
37 void fence_volatile(
38  message_handlert &message_handler,
39  value_setst &value_sets,
40  symbol_tablet &symbol_table,
41  goto_functionst &goto_functions);
42 
43 #endif // CPROVER_MUSKETEER_FENCE_SHARED_H
void fence_all_shared_aeg(message_handlert &message_handler, value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions)
The symbol table.
Definition: symbol_table.h:52
void fence_volatile(message_handlert &message_handler, value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions)
void fence_all_shared(message_handlert &message_handler, value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions)