CBMC
|
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>
Go to the source code of this file.
Classes | |
class | dfcc_swap_and_wrapt |
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.