cprover
weak_memory.h File Reference

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

#include "wmm.h"
#include "util/irep.h"
Include dependency graph for weak_memory.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

void weak_memory (memory_modelt model, value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions, bool SCC, instrumentation_strategyt event_stategy, 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, message_handlert &message, bool ignore_arrays)
 
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...
 

Detailed Description

Weak Memory Instrumentation for Threaded Goto Programs.

Definition in file weak_memory.h.

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_stategy,
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,
message_handlert message,
bool  ignore_arrays 
)