dfcc_instrument.cpp File Reference

#include "dfcc_instrument.h"
#include <util/format_expr.h>
#include <util/fresh_symbol.h>
#include <util/namespace.h>
#include <util/pointer_expr.h>
#include <util/pointer_predicates.h>
#include <util/prefix.h>
#include <util/suffix.h>
#include <goto-programs/goto_model.h>
#include <goto-programs/remove_skip.h>
#include <ansi-c/c_expr.h>
#include <ansi-c/c_object_factory_parameters.h>
#include <goto-instrument/contracts/utils.h>
#include <goto-instrument/generate_function_bodies.h>
#include <goto-instrument/unwind.h>
#include <goto-instrument/unwindset.h>
#include <langapi/language_util.h>
#include "dfcc_cfg_info.h"
#include "dfcc_contract_clauses_codegen.h"
#include "dfcc_instrument_loop.h"
#include "dfcc_is_cprover_symbol.h"
#include "dfcc_is_freeable.h"
#include "dfcc_is_fresh.h"
#include "dfcc_library.h"
#include "dfcc_obeys_contract.h"
#include "dfcc_pointer_equals.h"
#include "dfcc_pointer_in_range.h"
#include "dfcc_spec_functions.h"
#include "dfcc_utils.h"
#include <memory>

Include dependency graph for dfcc_instrument.cpp:

Go to the source code of this file.