cprover
|
#include <source_location.h>
Public Member Functions | |
source_locationt () | |
std::string | as_string () const |
std::string | as_string_with_cwd () const |
const irep_idt & | get_file () const |
const irep_idt & | get_working_directory () const |
const irep_idt & | get_line () const |
const irep_idt & | get_column () const |
const irep_idt & | get_function () const |
const irep_idt & | get_property_id () const |
const irep_idt & | get_property_class () const |
const irep_idt & | get_comment () const |
const irep_idt & | get_case_number () const |
const irep_idt & | get_java_bytecode_index () const |
const irep_idt & | get_basic_block_covered_lines () const |
void | set_file (const irep_idt &file) |
void | set_working_directory (const irep_idt &cwd) |
void | set_line (const irep_idt &line) |
void | set_line (unsigned line) |
void | set_column (const irep_idt &column) |
void | set_column (unsigned column) |
void | set_function (const irep_idt &function) |
void | set_property_id (const irep_idt &property_id) |
void | set_property_class (const irep_idt &property_class) |
void | set_comment (const irep_idt &comment) |
void | set_case_number (const irep_idt &number) |
void | set_java_bytecode_index (const irep_idt &index) |
void | set_basic_block_covered_lines (const irep_idt &covered_lines) |
void | set_hide () |
bool | get_hide () const |
bool | is_built_in () const |
void | merge (const source_locationt &from) |
Set all unset source-location fields in this object to their values in 'from'. More... | |
![]() | |
bool | is_nil () const |
bool | is_not_nil () const |
irept (const irep_idt &_id) | |
irept () | |
irept (const irept &irep) | |
irept (irept &&irep) | |
irept & | operator= (const irept &irep) |
irept & | operator= (irept &&irep) |
~irept () | |
const irep_idt & | id () const |
const std::string & | id_string () const |
void | id (const irep_idt &_data) |
const irept & | find (const irep_namet &name) const |
irept & | add (const irep_namet &name) |
irept & | add (const irep_namet &name, const irept &irep) |
const std::string & | get_string (const irep_namet &name) const |
const irep_idt & | get (const irep_namet &name) const |
bool | get_bool (const irep_namet &name) const |
signed int | get_int (const irep_namet &name) const |
unsigned int | get_unsigned_int (const irep_namet &name) const |
std::size_t | get_size_t (const irep_namet &name) const |
long long | get_long_long (const irep_namet &name) const |
void | set (const irep_namet &name, const irep_idt &value) |
void | set (const irep_namet &name, const irept &irep) |
void | set (const irep_namet &name, const long long value) |
void | remove (const irep_namet &name) |
void | move_to_sub (irept &irep) |
void | move_to_named_sub (const irep_namet &name, irept &irep) |
bool | operator== (const irept &other) const |
bool | operator!= (const irept &other) const |
void | swap (irept &irep) |
bool | operator< (const irept &other) const |
defines ordering on the internal representation More... | |
bool | ordering (const irept &other) const |
defines ordering on the internal representation More... | |
int | compare (const irept &i) const |
defines ordering on the internal representation More... | |
void | clear () |
void | make_nil () |
subt & | get_sub () |
const subt & | get_sub () const |
named_subt & | get_named_sub () |
const named_subt & | get_named_sub () const |
named_subt & | get_comments () |
const named_subt & | get_comments () const |
std::size_t | hash () const |
std::size_t | full_hash () const |
bool | full_eq (const irept &other) const |
std::string | pretty (unsigned indent=0, unsigned max_indent=0) const |
const dt & | read () const |
dt & | write () |
Static Public Member Functions | |
static bool | is_built_in (const std::string &s) |
static const source_locationt & | nil () |
Protected Member Functions | |
std::string | as_string (bool print_cwd) const |
![]() | |
void | detach () |
Additional Inherited Members | |
![]() | |
typedef std::vector< irept > | subt |
typedef std::map< irep_namet, irept > | named_subt |
![]() | |
static bool | is_comment (const irep_namet &name) |
static void | remove_ref (dt *old_data) |
static void | nonrecursive_destructor (dt *old_data) |
Does the same as remove_ref, but using an explicit stack instead of recursion. More... | |
![]() | |
dt * | data |
![]() | |
static dt | empty_d |
Definition at line 16 of file source_location.h.
|
inline |
Definition at line 19 of file source_location.h.
|
inline |
Definition at line 23 of file source_location.h.
Referenced by as_string_with_cwd(), mm2cppt::check_acyclic(), java_bytecode_convert_methodt::convert_athrow(), linkingt::detailed_conflict_report_rec(), operator<<(), goto_programt::output_instruction(), event_grapht::critical_cyclet::print_detail(), event_grapht::critical_cyclet::print_output(), goto_symext::return_assignment(), and symex_bmct::symex_step().
|
protected |
Definition at line 16 of file source_location.cpp.
References concat_dir_file(), dstringt::empty(), get_column(), get_file(), get_function(), get_java_bytecode_index(), get_line(), get_working_directory(), and id2string().
|
inline |
Definition at line 28 of file source_location.h.
References as_string().
|
inline |
Definition at line 83 of file source_location.h.
Referenced by convert_properties_json().
|
inline |
Definition at line 73 of file source_location.h.
|
inline |
Definition at line 48 of file source_location.h.
Referenced by as_string(), json(), message_handlert::print(), gcc_message_handlert::print(), and xml().
|
inline |
Definition at line 68 of file source_location.h.
Referenced by as_string(), expr2ct::convert_code(), convert_properties_json(), bmc_all_propertiest::goalt::goalt(), goto_programt::output_instruction(), replace_location(), and show_properties().
|
inline |
Definition at line 33 of file source_location.h.
Referenced by cpp_parsert::add_location(), as_string(), event_grapht::graph_pensieve_explorert::collect_pairs(), convert(), event_grapht::copy_segment(), filter_out(), document_propertiest::get_code(), parsert::get_file(), is_built_in(), system_library_symbolst::is_symbol_internal_symbol(), json(), json_output_function(), ui_message_handlert::json_ui_msg(), list_functions(), graphml_witnesst::operator()(), internal_goals_filtert::operator()(), goto_difft::output_function(), message_handlert::print(), gcc_message_handlert::print(), instrumentert::print_outputs_local(), show_locations(), value_sets_to_xml(), xml(), xml_output_function(), and ui_message_handlert::xml_ui_msg().
|
inline |
Definition at line 53 of file source_location.h.
Referenced by goto_program2codet::add_local_types(), as_string(), goto_program2codet::cleanup_expr(), dump_ct::convert_compound_declaration(), dump_ct::convert_global_variable(), convert_input(), convert_output(), event_grapht::copy_segment(), linkingt::duplicate_code_symbol(), remove_function_pointerst::fix_return_type(), dump_ct::gather_global_typedefs(), expr2ct::get_shorthands(), json(), code_contractst::new_tmp_symbol(), dump_ct::operator()(), message_handlert::print(), gcc_message_handlert::print(), instrumentert::print_outputs_local(), cpp_typecheck_resolvet::resolve(), bmc_covert::satisfying_assignment(), show_locations(), type2name(), c_typecheck_baset::typecheck_expr_symbol(), and xml().
|
inline |
Definition at line 159 of file source_location.h.
References irept::get_bool().
|
inline |
Definition at line 78 of file source_location.h.
Referenced by as_string(), and json().
|
inline |
Definition at line 43 of file source_location.h.
Referenced by as_string(), event_grapht::graph_pensieve_explorert::collect_pairs(), instrumentert::cfg_visitort::contains_shared_array(), java_bytecode_convert_methodt::convert_multianewarray(), java_bytecode_convert_methodt::convert_new(), java_bytecode_convert_methodt::convert_newarray(), filter_out(), document_propertiest::get_code(), java_bytecode_instrumentt::instrument_code(), json(), json_output_function(), list_functions(), graphml_witnesst::operator()(), message_handlert::print(), gcc_message_handlert::print(), show_locations(), xml(), and xml_output_function().
|
inline |
Definition at line 63 of file source_location.h.
Referenced by convert_properties_json(), goto_checkt::goto_check(), replace_location(), and show_properties().
|
inline |
Definition at line 58 of file source_location.h.
Referenced by convert(), convert_assert(), convert_properties_json(), property_checkert::initialize_property_map(), goto_difft::output_function(), replace_location(), and show_properties().
|
inline |
Definition at line 38 of file source_location.h.
Referenced by as_string(), json(), json_output_function(), list_functions(), xml(), and xml_output_function().
|
inlinestatic |
Definition at line 164 of file source_location.h.
References has_prefix().
Referenced by filter_out(), graphml_witnesst::operator()(), and internal_goals_filtert::operator()().
|
inline |
Definition at line 171 of file source_location.h.
References get_file(), and id2string().
Referenced by symex_coveraget::compute_overall_coverage().
void source_locationt::merge | ( | const source_locationt & | from | ) |
Set all unset source-location fields in this object to their values in 'from'.
Leave set fields in this object alone.
Definition at line 65 of file source_location.cpp.
References forall_named_irep, and irept::get_named_sub().
Referenced by merge_source_location_rec().
|
inlinestatic |
Definition at line 180 of file source_location.h.
References get_nil_irep().
Referenced by cover_basic_blockst::cover_basic_blockst().
|
inline |
Definition at line 149 of file source_location.h.
Referenced by cover_basic_blockst::update_covered_lines().
|
inline |
Definition at line 139 of file source_location.h.
Referenced by goto_convertt::convert_switch().
|
inline |
Definition at line 108 of file source_location.h.
Referenced by error_parse_line(), and parsert::parse_error().
|
inline |
Definition at line 113 of file source_location.h.
|
inline |
Definition at line 133 of file source_location.h.
References comment().
Referenced by uninitializedt::add_assertions(), check_apply_invariants(), java_bytecode_instrumentt::check_arithmetic_exception(), java_bytecode_instrumentt::check_array_access(), java_bytecode_instrumentt::check_array_length(), java_bytecode_instrumentt::check_class_cast(), java_bytecode_instrumentt::check_null_dereference(), java_bytecode_convert_methodt::convert_athrow(), java_bytecode_convert_methodt::convert_checkcast(), dump_ct::insert_local_type_decls(), cover_mcdc_instrumentert::instrument(), java_bytecode_instrument_uncaught_exceptions(), linker_script_merget::ls_data2instructions(), race_check(), replace_location(), and undefined_function_abort_path().
|
inline |
Definition at line 88 of file source_location.h.
Referenced by document_propertiest::doit(), error_parse_line(), get_thread_safe_clinit_wrapper_body(), lazy_goto_modelt::initialize(), initialize_goto_model(), linker_script_merget::ls_data2instructions(), language_uit::parse(), parsert::set_file(), Parser::set_location(), and Parser::SyntaxError().
|
inline |
Definition at line 118 of file source_location.h.
Referenced by java_bytecode_convert_methodt::convert(), java_bytecode_convert_methodt::convert_if(), java_bytecode_convert_methodt::convert_invoke(), java_simple_method_stubst::create_method_stub(), cpp_typecheckt::default_assignop(), cpp_typecheckt::default_cpctor(), document_propertiest::doit(), cpp_typecheckt::dtor(), error_parse_line(), get_thread_safe_clinit_wrapper_body(), goto_checkt::goto_check(), java_bytecode_convert_method_lazy(), java_bytecode_convert_methodt::replace_call_to_cprover_assume(), parsert::set_function(), and Parser::set_location().
|
inline |
Definition at line 154 of file source_location.h.
Referenced by goto_inlinet::insert_function_body().
|
inline |
Definition at line 144 of file source_location.h.
Referenced by java_bytecode_parsert::rbytecode().
|
inline |
Definition at line 98 of file source_location.h.
Referenced by document_propertiest::doit(), smt2_tokenizert::error(), error_parse_line(), get_thread_safe_clinit_wrapper_body(), java_bytecode_parsert::rmethod_attribute(), Parser::set_location(), parsert::set_source_location(), and Parser::SyntaxError().
|
inline |
Definition at line 103 of file source_location.h.
|
inline |
Definition at line 128 of file source_location.h.
Referenced by uninitializedt::add_assertions(), java_bytecode_instrumentt::check_arithmetic_exception(), java_bytecode_instrumentt::check_array_access(), java_bytecode_instrumentt::check_array_length(), java_bytecode_instrumentt::check_class_cast(), java_bytecode_instrumentt::check_null_dereference(), java_bytecode_convert_methodt::convert_athrow(), java_bytecode_convert_methodt::convert_checkcast(), goto_program_dereferencet::dereference_failure(), taint_analysist::instrument(), instrument_preconditions(), and replace_location().
|
inline |
Definition at line 123 of file source_location.h.
Referenced by replace_location().
|
inline |
Definition at line 93 of file source_location.h.
Referenced by parsert::set_file().