10 #ifndef CPROVER_UTIL_SOURCE_LOCATION_H 11 #define CPROVER_UTIL_SOURCE_LOCATION_H 44 return get(ID_working_directory);
54 return get(ID_column);
59 return get(ID_function);
64 return get(ID_property_id);
69 return get(ID_property_class);
74 return get(ID_comment);
79 return get(ID_switch_case_number);
84 return get(ID_java_bytecode_index);
89 return get(ID_basic_block_covered_lines);
99 set(ID_working_directory, cwd);
114 set(ID_column, column);
119 set(ID_column, column);
124 set(ID_function,
function);
129 set(ID_property_id, property_id);
134 set(ID_property_class, property_class);
145 set(ID_switch_case_number, number);
150 set(ID_java_bytecode_index, index);
155 return set(ID_basic_block_covered_lines, covered_lines);
170 std::string built_in1=
"<built-in-";
171 std::string built_in2=
"<builtin-";
186 return static_cast<const source_locationt &>(
get_nil_irep());
192 std::string
as_string(
bool print_cwd)
const;
203 return "source location: " + source_location.
as_string();
207 #endif // CPROVER_UTIL_SOURCE_LOCATION_H const irept & get_nil_irep()
const irep_idt & get_working_directory() const
void set_function(const irep_idt &function)
void set_case_number(const irep_idt &number)
const std::string & id2string(const irep_idt &d)
void set_java_bytecode_index(const irep_idt &index)
void set_property_class(const irep_idt &property_class)
static bool is_built_in(const std::string &s)
static const source_locationt & nil()
std::string comment(const rw_set_baset::entryt &entry, bool write)
void set_comment(const irep_idt &comment)
const irep_idt & get_function() const
std::string as_string() const
bool get_bool(const irep_namet &name) const
void set_line(unsigned line)
const irep_idt & get_column() const
void set_property_id(const irep_idt &property_id)
void set_working_directory(const irep_idt &cwd)
const irep_idt & get_case_number() const
void merge(const source_locationt &from)
Set all unset source-location fields in this object to their values in 'from'.
const irep_idt & get_line() const
Helper to give us some diagnostic in a usable form on assertion failure.
void set_file(const irep_idt &file)
nonstd::optional< T > optionalt
const irep_idt & get(const irep_namet &name) const
void set_line(const irep_idt &line)
const irep_idt & get_basic_block_covered_lines() const
void set_column(const irep_idt &column)
bool has_prefix(const std::string &s, const std::string &prefix)
Base class for tree-like data structures with sharing.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
static std::string diagnostics_as_string(const source_locationt &source_location)
const irep_idt & get_file() const
std::string as_string_with_cwd() const
void set_column(unsigned column)
optionalt< std::string > full_path() const
Get a path to the file, including working directory.
const irep_idt & get_java_bytecode_index() const
const irep_idt & get_comment() const
const irep_idt & get_property_id() const
const irep_idt & get_property_class() const
std::ostream & operator<<(std::ostream &, const source_locationt &)
void set(const irep_namet &name, const irep_idt &value)
void set_basic_block_covered_lines(const irep_idt &covered_lines)