CBMC
|
#include "dfcc_library.h"
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/config.h>
#include <util/cprover_prefix.h>
#include <util/message.h>
#include <util/pointer_expr.h>
#include <util/pointer_predicates.h>
#include <util/std_code.h>
#include <util/std_expr.h>
#include <goto-programs/goto_function.h>
#include <goto-programs/goto_model.h>
#include <ansi-c/c_expr.h>
#include <ansi-c/c_object_factory_parameters.h>
#include <ansi-c/cprover_library.h>
#include <ansi-c/goto-conversion/goto_convert_functions.h>
#include <goto-instrument/generate_function_bodies.h>
#include <goto-instrument/unwind.h>
#include <goto-instrument/unwindset.h>
#include <linking/static_lifetime_init.h>
#include "dfcc_utils.h"
Go to the source code of this file.
Macros | |
#define | CONTRACTS_PREFIX CPROVER_PREFIX "contracts_" |
Functions | |
template<typename K , typename V > | |
std::map< V, K > | swap_map (std::map< K, V > const &map) |
Swaps keys and values in a map. More... | |
const std::map< dfcc_typet, irep_idt > | create_dfcc_type_to_name () |
Creates the enum to type name mapping. More... | |
const std::map< dfcc_funt, irep_idt > | create_dfcc_fun_to_name () |
const std::map< irep_idt, dfcc_funt > | create_dfcc_hook () |
const std::map< irep_idt, dfcc_funt > | create_havoc_hook () |
const std::set< irep_idt > | create_assignable_builtin_names () |
static void | add_checked_pragmas (source_locationt &sl) |
Variables | |
static const std::set< dfcc_funt > | to_inline |
set of functions that need to be inlined More... | |
static const std::map< dfcc_funt, int > | to_unwind |
set of functions that need to be unwound to assigns clause size with corresponding loop identifiers. More... | |
static const std::set< dfcc_funt > | fix_malloc_free_set |
Set of functions that contain calls to assignable_malloc or assignable_free. More... | |
#define CONTRACTS_PREFIX CPROVER_PREFIX "contracts_" |
Definition at line 46 of file dfcc_library.cpp.
|
static |
Definition at line 216 of file dfcc_library.cpp.
const std::set<irep_idt> create_assignable_builtin_names | ( | ) |
Definition at line 158 of file dfcc_library.cpp.
Definition at line 61 of file dfcc_library.cpp.
Definition at line 138 of file dfcc_library.cpp.
const std::map<dfcc_typet, irep_idt> create_dfcc_type_to_name | ( | ) |
Creates the enum to type name mapping.
Definition at line 49 of file dfcc_library.cpp.
Definition at line 148 of file dfcc_library.cpp.
std::map<V, K> swap_map | ( | std::map< K, V > const & | map | ) |
Swaps keys and values in a map.
Definition at line 37 of file dfcc_library.cpp.
|
static |
Set of functions that contain calls to assignable_malloc or assignable_free.
Definition at line 457 of file dfcc_library.cpp.
|
static |
set of functions that need to be inlined
Definition at line 386 of file dfcc_library.cpp.
|
static |
set of functions that need to be unwound to assigns clause size with corresponding loop identifiers.
Definition at line 420 of file dfcc_library.cpp.