cprover
weak_memory.cpp File Reference

Weak Memory Instrumentation for Threaded Goto Programs. More...

#include "weak_memory.h"
#include <set>
#include <util/cprover_prefix.h>
#include <util/prefix.h>
#include <util/message.h>
#include <goto-programs/remove_skip.h>
#include "../rw_set.h"
#include "shared_buffers.h"
#include "goto2graph.h"
Include dependency graph for weak_memory.cpp:

Go to the source code of this file.

Functions

void introduce_temporaries (value_setst &value_sets, symbol_tablet &symbol_table, const irep_idt &function, goto_programt &goto_program, messaget &message)
 all access to shared variables is pushed into assignments More...
 
void 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 input_max_var, unsigned input_max_po_trans, bool render_po, bool render_file, bool render_function, bool cav11_option, bool hide_internals, message_handlert &message_handler, bool ignore_arrays)
 

Detailed Description

Weak Memory Instrumentation for Threaded Goto Programs.

Definition in file weak_memory.cpp.

Function Documentation

§ introduce_temporaries()

§ weak_memory()

void 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  input_max_var,
unsigned  input_max_po_trans,
bool  render_po,
bool  render_file,
bool  render_function,
bool  cav11_option,
bool  hide_internals,
message_handlert message_handler,
bool  ignore_arrays 
)