14 #ifndef CPROVER_GOTO_INSTRUMENT_WMM_WEAK_MEMORY_H
15 #define CPROVER_GOTO_INSTRUMENT_WMM_WEAK_MEMORY_H
38 unsigned max_po_trans,
58 #define OPT_WMM_MEMORY_MODEL "(mm):"
60 #define OPT_WMM_INSTRUMENTATION_STRATEGIES \
61 "(one-event-per-cycle)" \
62 "(minimum-interference)" \
67 #define OPT_WMM_LIMITS \
71 #define OPT_WMM_LOOPS \
72 "(force-loop-duplication)" \
73 "(no-loop-duplication)" \
75 #define OPT_WMM_MISC \
80 "(render-cluster-file)" \
81 "(render-cluster-function)" \
87 OPT_WMM_MEMORY_MODEL \
88 OPT_WMM_INSTRUMENTATION_STRATEGIES \
94 #define HELP_WMM_FULL \
95 " --mm <tso,pso,rmo,power> instruments a weak memory model\n" \
96 " --scc detects critical cycles per SCC (one thread per SCC)\n"
\
97 " --one-event-per-cycle only instruments one event per cycle\n" \
98 " --minimum-interference instruments an optimal number of events\n" \
99 " --my-events only instruments events whose ids appear in inst.evt\n"
\
100 " --cfg-kill enables symbolic execution used to reduce spurious cycles\n" \
101 " --no-dependencies no dependency analysis\n" \
102 " --no-po-rendering no representation of the threads in the dot\n"\
103 " --render-cluster-file clusterises the dot by files\n" \
104 " --render-cluster-function clusterises the dot by functions\n"
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
::goto_functiont goto_functiont
A generic container class for the GOTO intermediate representation of one function.
Class that provides messages with a built-in verbosity 'level'.
void introduce_temporaries(value_setst &, symbol_tablet &, const irep_idt &function, goto_programt &, messaget &message)
all access to shared variables is pushed into assignments
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)
instrumentation_strategyt