Go to the documentation of this file.
10 #ifndef CPROVER_UTIL_SOURCE_LOCATION_H
11 #define CPROVER_UTIL_SOURCE_LOCATION_H
43 return get(ID_working_directory);
53 return get(ID_column);
58 return get(ID_function);
63 return get(ID_property_id);
68 return get(ID_property_class);
73 return get(ID_comment);
78 return get(ID_switch_case_number);
83 return get(ID_java_bytecode_index);
88 return get(ID_basic_block_covered_lines);
93 return get(ID_basic_block_source_lines);
103 set(ID_working_directory, cwd);
118 set(ID_column, column);
123 set(ID_column, column);
128 set(ID_function,
function);
133 set(ID_property_id, property_id);
138 set(ID_property_class, property_class);
149 set(ID_switch_case_number, number);
154 set(ID_java_bytecode_index, index);
159 return set(ID_basic_block_covered_lines, covered_lines);
164 return set(ID_basic_block_source_lines, source_lines);
197 add(ID_pragma).
add(pragma);
206 std::string
as_string(
bool print_cwd)
const;
217 return "source location: " + source_location.
as_string();
221 #endif // CPROVER_UTIL_SOURCE_LOCATION_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const irep_idt & get_function() const
const irep_idt & get_comment() const
const irep_idt & get_property_id() const
const irep_idt & get_property_class() const
std::string as_string() const
void set_comment(const irep_idt &comment)
void set_function(const irep_idt &function)
const irept::named_subt & get_pragmas() const
void set_case_number(const irep_idt &number)
void set_line(unsigned line)
irept & add(const irep_namet &name)
static std::string diagnostics_as_string(const source_locationt &source_location)
static const source_locationt & nil()
const irept & find(const irep_namet &name) const
void add_pragma(const irep_idt &pragma)
void set_java_bytecode_index(const irep_idt &index)
const irep_idt & get_column() const
void set_property_id(const irep_idt &property_id)
void set_basic_block_source_lines(const irep_idt &source_lines)
typename dt::named_subt named_subt
void set_working_directory(const irep_idt &cwd)
const irep_idt & get_basic_block_source_lines() const
const irep_idt & get_line() const
void set_column(const irep_idt &column)
void set_line(const irep_idt &line)
bool get_bool(const irep_namet &name) const
const irep_idt & get_case_number() const
const std::string & id2string(const irep_idt &d)
named_subt & get_named_sub()
void merge(const source_locationt &from)
Set all unset source-location fields in this object to their values in 'from'.
void set_file(const irep_idt &file)
const irep_idt & get_basic_block_covered_lines() const
optionalt< std::string > full_path() const
Get a path to the file, including working directory.
nonstd::optional< T > optionalt
Helper to give us some diagnostic in a usable form on assertion failure.
std::ostream & operator<<(std::ostream &, const source_locationt &)
const irep_idt & get_java_bytecode_index() const
const irep_idt & get(const irep_namet &name) const
void set(const irep_namet &name, const irep_idt &value)
std::string as_string_with_cwd() const
const irep_idt & get_file() const
void set_column(unsigned column)
There are a large number of kinds of tree structured or tree-like data in CPROVER.
const irept & get_nil_irep()
void set_basic_block_covered_lines(const irep_idt &covered_lines)
const irep_idt & get_working_directory() const
static std::string comment(const rw_set_baset::entryt &entry, bool write)
void set_property_class(const irep_idt &property_class)