CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
source_location.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "source_location.h"
10
11#include "prefix.h"
12
13#include <filesystem>
14#include <ostream>
15
16bool source_locationt::is_built_in(const std::string &s)
17{
18 std::string built_in1 = "<built-in-"; // "<built-in-additions>";
19 std::string built_in2 = "<builtin-"; // "<builtin-architecture-strings>";
20 return has_prefix(s, built_in1) || has_prefix(s, built_in2);
21}
22
25{
26 std::string dest;
27
28 const irep_idt &file=get_file();
29 const irep_idt &line=get_line();
30 const irep_idt &column=get_column();
31 const irep_idt &function=get_function();
32 const irep_idt &bytecode=get_java_bytecode_index();
33
34 if(!file.empty())
35 {
36 if(!dest.empty())
37 dest+=' ';
38 dest+="file ";
39 if(print_cwd)
40 {
41 dest += std::filesystem::path(id2string(get_working_directory()))
42 .append(id2string(file))
43 .string();
44 }
45 else
46 dest+=id2string(file);
47 }
48 if(!line.empty())
49 {
50 if(!dest.empty())
51 dest+=' ';
52 dest+="line "+id2string(line);
53 }
54 if(!column.empty())
55 {
56 if(!dest.empty())
57 dest+=' ';
58 dest+="column "+id2string(column);
59 }
60 if(!function.empty())
61 {
62 if(!dest.empty())
63 dest+=' ';
64 dest+="function "+id2string(function);
65 }
66 if(!bytecode.empty())
67 {
68 if(!dest.empty())
69 dest+=' ';
70 dest+="bytecode-index "+id2string(bytecode);
71 }
72
73 return dest;
74}
75
77{
78 for(const auto &irep_entry : from.get_named_sub())
79 {
80 if(get(irep_entry.first).empty())
81 set(irep_entry.first, irep_entry.second);
82 }
83}
84
88std::optional<std::string> source_locationt::full_path() const
89{
90 const auto file = id2string(get_file());
91
92 if(file.empty() || is_built_in(file))
93 return {};
94
95 return std::filesystem::path(id2string(get_working_directory()))
96 .append(file)
97 .string();
98}
99
100std::ostream &operator << (
101 std::ostream &out,
102 const source_locationt &source_location)
103{
104 if(source_location.is_nil())
105 return out;
106 out << source_location.as_string();
107 return out;
108}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
bool empty() const
Definition dstring.h:89
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:412
bool is_nil() const
Definition irep.h:368
void merge(const source_locationt &from)
Set all unset source-location fields in this object to their values in 'from'.
bool is_built_in() const
const irep_idt & get_java_bytecode_index() const
const irep_idt & get_column() const
const irep_idt & get_function() const
const irep_idt & get_working_directory() const
const irep_idt & get_file() const
const irep_idt & get_line() const
std::string as_string() const
std::optional< std::string > full_path() const
Get a path to the file, including working directory.
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
std::ostream & operator<<(std::ostream &out, const source_locationt &source_location)