CBMC
dfcc_swap_and_wrap.h File Reference

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.