Skip to content

Commit ac7867c

Browse files
authored
Merge pull request #4034 from tautschnig/get_code
get_code: return std::string by value
2 parents d56feb6 + 3a0e2ab commit ac7867c

File tree

1 file changed

+11
-13
lines changed

1 file changed

+11
-13
lines changed

src/goto-instrument/document_properties.cpp

Lines changed: 11 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -57,9 +57,7 @@ class document_propertiest
5757

5858
static void strip_space(std::list<linet> &lines);
5959

60-
void get_code(
61-
const source_locationt &source_location,
62-
std::string &dest);
60+
std::string get_code(const source_locationt &source_location);
6361

6462
struct doc_claimt
6563
{
@@ -148,26 +146,25 @@ bool is_empty(const std::string &s)
148146
return true;
149147
}
150148

151-
void document_propertiest::get_code(
152-
const source_locationt &source_location,
153-
std::string &dest)
149+
std::string
150+
document_propertiest::get_code(const source_locationt &source_location)
154151
{
155-
dest="";
156-
157152
const irep_idt &file=source_location.get_file();
158153
const irep_idt &source_line = source_location.get_line();
159154

160-
if(file == "" || source_line == "")
161-
return;
155+
if(file.empty() || source_line.empty())
156+
return "";
162157

163158
std::ifstream in(id2string(file));
164159

160+
std::string dest;
161+
165162
if(!in)
166163
{
167164
dest+="ERROR: unable to open ";
168165
dest+=id2string(file);
169166
dest+="\n";
170-
return;
167+
return dest;
171168
}
172169

173170
int line_int = unsafe_string2int(id2string(source_line));
@@ -268,6 +265,8 @@ void document_propertiest::get_code(
268265

269266
dest+=tmp+"\n";
270267
}
268+
269+
return dest;
271270
}
272271

273272
void document_propertiest::doit()
@@ -298,10 +297,9 @@ void document_propertiest::doit()
298297
for(claim_sett::const_iterator it=claim_set.begin();
299298
it!=claim_set.end(); it++)
300299
{
301-
std::string code;
302300
const source_locationt &source_location=it->first;
303301

304-
get_code(source_location, code);
302+
std::string code = get_code(source_location);
305303

306304
switch(format)
307305
{

0 commit comments

Comments
 (0)