Given a function_id and contract_id, swaps its body to a function with a fresh mangled name, instruments it for dynamic frame condition checking, and replaces the original function's body with instructions encoding contract checking against the mangled function, or contract replacement. More...

#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/message.h>
#include <util/std_expr.h>
#include <util/std_types.h>
#include <ansi-c/goto-conversion/goto_convert_functions.h>
#include "dfcc_contract_handler.h"
#include "dfcc_instrument.h"
#include "dfcc_library.h"
#include "dfcc_spec_functions.h"
#include <map>
#include <set>

Include dependency graph for dfcc_swap_and_wrap.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	dfcc_swap_and_wrapt

Detailed Description

Given a function_id and contract_id, swaps its body to a function with a fresh mangled name, instruments it for dynamic frame condition checking, and replaces the original function's body with instructions encoding contract checking against the mangled function, or contract replacement.

Definition in file dfcc_swap_and_wrap.h.

Classes

Detailed Description