dfcc.cpp File Reference

#include "dfcc.h"
#include <util/config.h>
#include <util/prefix.h>
#include <util/string_utils.h>
#include <goto-programs/remove_skip.h>
#include <goto-programs/remove_unused_functions.h>
#include <ansi-c/ansi_c_entry_point.h>
#include <ansi-c/c_object_factory_parameters.h>
#include <ansi-c/cprover_library.h>
#include <ansi-c/goto-conversion/link_to_library.h>
#include <goto-instrument/generate_function_bodies.h>
#include <goto-instrument/nondet_static.h>
#include <linking/static_lifetime_init.h>
#include "dfcc_lift_memory_predicates.h"
#include "dfcc_utils.h"

Include dependency graph for dfcc.cpp:

Go to the source code of this file.

Functions
static std::pair< irep_idt, irep_idt >	parse_function_contract_pair (const irep_idt &cli_flag)
void	dfcc (const optionst &options, goto_modelt &goto_model, const irep_idt &harness_id, const std::optional< irep_idt > &to_check, const bool allow_recursive_calls, const std::set< irep_idt > &to_replace, const loop_contract_configt loop_contract_config, const std::set< std::string > &to_exclude_from_nondet_static, message_handlert &message_handler)
	Applies function contracts transformation to GOTO model, using the dynamic frame condition checking approach.

Function Documentation

parse_function_contract_pair()

static std::pair< irep_idt, irep_idt > parse_function_contract_pair ( const irep_idt &  cli_flag )

static

Definition at line 54 of file dfcc.cpp.