cprover
fence_shared.cpp File Reference
#include "fence_shared.h"
#include <iostream>
#include <sstream>
#include <fstream>
#include <list>
#include <vector>
#include <set>
#include <util/cprover_prefix.h>
#include <util/prefix.h>
#include <util/message.h>
#include <goto-programs/remove_skip.h>
#include <goto-programs/goto_functions.h>
#include <goto-instrument/wmm/goto2graph.h>
#include <goto-instrument/rw_set.h>
Include dependency graph for fence_shared.cpp:

Go to the source code of this file.

Classes

class  simple_insertiont
 
class  fence_all_sharedt
 
class  fence_all_shared_aegt
 
class  fence_volatilet
 

Macros

#define OUTPUT(s, fence, file, line, id, type)   s<<fence<<"|"<<file<<"|"<<line<<"|"<<id<<"|"<<type<<'\n'
 

Functions

void fence_all_shared (message_handlert &message_handler, value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions)
 
void fence_all_shared_aeg (message_handlert &message_handler, value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions)
 
void fence_volatile (message_handlert &message_handler, value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions)
 

Macro Definition Documentation

◆ OUTPUT

#define OUTPUT (   s,
  fence,
  file,
  line,
  id,
  type 
)    s<<fence<<"|"<<file<<"|"<<line<<"|"<<id<<"|"<<type<<'\n'

Definition at line 32 of file fence_shared.cpp.

Referenced by simple_insertiont::print_to_file().

Function Documentation

◆ fence_all_shared()

void fence_all_shared ( message_handlert message_handler,
value_setst value_sets,
symbol_tablet symbol_table,
goto_functionst goto_functions 
)

◆ fence_all_shared_aeg()

void fence_all_shared_aeg ( message_handlert message_handler,
value_setst value_sets,
symbol_tablet symbol_table,
goto_functionst goto_functions 
)

◆ fence_volatile()

void fence_volatile ( message_handlert message_handler,
value_setst value_sets,
symbol_tablet symbol_table,
goto_functionst goto_functions 
)