cprover
cprover_prefix.h File Reference
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Macros

#define CPROVER_PREFIX   "__CPROVER_"
 
#define CPROVER_FKT_PREFIX   "__CPROVER_fkt_"
 
#define CPROVER_MACRO_PREFIX   "__CPROVER_macro_"
 

Macro Definition Documentation

◆ CPROVER_FKT_PREFIX

#define CPROVER_FKT_PREFIX   "__CPROVER_fkt_"

Definition at line 14 of file cprover_prefix.h.

Referenced by goto_symext::symex_function_call_symbol().

◆ CPROVER_MACRO_PREFIX

#define CPROVER_MACRO_PREFIX   "__CPROVER_macro_"

◆ CPROVER_PREFIX

#define CPROVER_PREFIX   "__CPROVER_"

Definition at line 13 of file cprover_prefix.h.

Referenced by adjust_float_expressions(), ansi_c_entry_point(), branch(), value_set_dereferencet::build_reference_to(), goto_checkt::collect_allocations(), fence_all_sharedt::compute(), fence_volatilet::compute(), symex_coveraget::compute_overall_coverage(), show_goto_functions_jsont::convert(), show_goto_functions_xmlt::convert(), create_initialize(), dead_object(), deallocated(), goto_convertt::do_function_call_symbol(), c_typecheck_baset::do_initializer(), goto_convertt::do_printf(), goto_convertt::do_scanf(), c_typecheck_baset::do_special_functions(), dynamic_size(), goto_functions_templatet< goto_programt >::entry_point(), fence_all_shared_aegt::fence_all_shared_aeg_explore(), fence_pensieve(), fence_weak_memory(), function_enter(), function_exit(), goto_checkt::goto_check(), dump_ct::ignore(), implicit(), interrupt(), shared_bufferst::is_buffered(), refined_string_typet::is_c_string_type(), is_shared(), java_internal_additions(), jsil_entry_point(), jsil_internal_additions(), instrumentert::local(), malloc_object(), mm_io(), mmio(), model_argc_argv(), nondet_static(), code_contractst::operator()(), race_check(), remove_internal_symbols(), bmct::run(), configt::set_from_symbol_table(), string_refinementt::set_mode(), slice_global_inits(), stack_depth(), static_lifetime_init(), string_from_ns(), shared_bufferst::track(), c_typecheck_baset::typecheck_expr_symbol(), unsigned_from_ns(), instrumentert::cfg_visitort::visit_cfg_function(), weak_memory(), and shared_bufferst::cfg_visitort::weak_memory().