cprover
pensieve.h File Reference

Fence insertion following criteria of Pensieve (PPoPP'05) More...

Include dependency graph for pensieve.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

void fence_pensieve (value_setst &value_sets, symbol_tablet &symbol_table, goto_functionst &goto_functions, unsigned unwinding_bound, unsigned max_po_trans, bool render_po, bool render_file, bool render_function, bool naive_mode, message_handlert &message_handler)
 

Detailed Description

Fence insertion following criteria of Pensieve (PPoPP'05)

Definition in file pensieve.h.

Function Documentation

§ fence_pensieve()