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 &, goto_modelt &, bool SCC, instrumentation_strategyt event_stategy, 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 &, bool ignore_arrays)
 
void introduce_temporaries (value_setst &, symbol_tablet &, const irep_idt &function, goto_programt &, 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()

void introduce_temporaries ( value_setst ,
symbol_tablet ,
const irep_idt function,
goto_programt ,
messaget message 
)

all access to shared variables is pushed into assignments

Definition at line 36 of file weak_memory.cpp.

◆ weak_memory()

void weak_memory ( memory_modelt  model,
value_setst ,
goto_modelt ,
bool  SCC,
instrumentation_strategyt  event_stategy,
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 ,
bool  ignore_arrays 
)

Definition at line 104 of file weak_memory.cpp.