Skip to content

Commit 8bf4031

Browse files
NlightNFotismartin
authored andcommitted
Implement changes to review comments in diffblue#167
1 parent c211f0f commit 8bf4031

File tree

9 files changed

+21
-22
lines changed

9 files changed

+21
-22
lines changed

regression/goto-instrument/store_goto_locations/test.desc

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,4 +6,3 @@ main.c
66
Original GOTO location
77
--
88
--
9-
This is tracked by the JIRA issue TYT-4: https://diffblue.atlassian.net/projects/TYT/issues/TYT-4

src/analyses/ai.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -235,9 +235,11 @@ xmlt ai_baset::output_xml(
235235
i_it->source_location.as_string());
236236
auto original_location = i_it->source_location.get_goto_location();
237237
if(original_location!="")
238+
{
238239
location.set_attribute(
239-
"originalGOTOLocation",
240+
"original_GOTO_Location",
240241
id2string(original_location));
242+
}
241243

242244
location.new_element(find_state(i_it).output_xml(*this, ns));
243245

src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -427,10 +427,9 @@ int goto_instrument_parse_optionst::doit()
427427

428428
if(cmdline.isset("store-goto-locations"))
429429
{
430-
Forall_goto_functions(it, goto_functions)
430+
for(auto &function : goto_model.goto_functions.function_map)
431431
{
432-
auto &function_body = it->second.body;
433-
store_goto_locations(function_body);
432+
store_goto_locations(function.second.body);
434433
}
435434
}
436435

src/goto-instrument/store_goto_location.cpp

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -5,13 +5,13 @@
55

66
void store_goto_locations(goto_programt &goto_program)
77
{
8-
for (auto it=goto_program.instructions.begin();
9-
it!=goto_program.instructions.end();
10-
it++)
8+
for(auto it=goto_program.instructions.begin();
9+
it!=goto_program.instructions.end();
10+
it++)
1111
{
12-
auto &source_location = it->source_location;
13-
auto location_number = it->location_number;
12+
auto &source_location=it->source_location;
13+
auto location_number=it->location_number;
1414

15-
source_location.set_goto_location(location_number);
15+
source_location.set_goto_location(location_number);
1616
}
1717
}

src/goto-instrument/store_goto_location.h

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -8,12 +8,12 @@ Date: August 2017
88
99
\*******************************************************************/
1010

11-
#ifndef STORE_GOTO_LOCATION_H
12-
#define STORE_GOTO_LOCATION_H
11+
#ifndef CPROVER_GOTO_INSTRUMENT_STORE_GOTO_LOCATION_H
12+
#define CPROVER_GOTO_INSTRUMENT_STORE_GOTO_LOCATION_H
1313

1414

1515
#include <goto-programs/goto_program.h>
1616

1717
void store_goto_locations(goto_programt &goto_program);
1818

19-
#endif // STORE_GOTO_LOCATION_H
19+
#endif // CPROVER_GOTO_INSTRUMENT_STORE_GOTO_LOCATION_H

src/goto-programs/goto_program.cpp

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -37,15 +37,11 @@ std::ostream &goto_programt::output_instruction(
3737
std::ostream &out,
3838
const instructiont &instruction) const
3939
{
40+
out << " // " << instruction.location_number << " ";
4041
auto original_location=instruction.source_location.get_goto_location();
4142
if(original_location!="")
4243
{
43-
out << " // " << instruction.location_number << " "
44-
<< "(Original GOTO location: " << original_location << ") ";
45-
}
46-
else
47-
{
48-
out << " // " << instruction.location_number << " ";
44+
out << "(Original GOTO location: " << original_location << ") ";
4945
}
5046

5147
if(!instruction.source_location.is_nil())

src/goto-programs/show_goto_functions_json.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -79,8 +79,10 @@ json_objectt show_goto_functions_jsont::convert(
7979
json(instruction.code.source_location());
8080

8181
if(instruction.code.source_location().get_goto_location()!="")
82+
{
8283
instruction_entry["originalGOTOLocation"]=
8384
json_stringt(id2string(instruction.code.source_location().get_goto_location()));
85+
}
8486
}
8587

8688
std::ostringstream instruction_builder;

src/util/irep_ids.def

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -839,6 +839,7 @@ IREP_ID_TWO(type_variables, #type_variables)
839839
IREP_ID_ONE(havoc_object)
840840
IREP_ID_TWO(overflow_shl, overflow-shl)
841841
IREP_ID_TWO(C_no_initialization_required, #no_initialization_required)
842+
IREP_ID_ONE(original_GOTO_location)
842843

843844
#undef IREP_ID_ONE
844845
#undef IREP_ID_TWO

src/util/source_location.h

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -163,12 +163,12 @@ class source_locationt:public irept
163163

164164
void set_goto_location(unsigned location)
165165
{
166-
set("GOTO_location", location);
166+
set(ID_original_GOTO_location, location);
167167
}
168168

169169
const irep_idt get_goto_location() const
170170
{
171-
return get("GOTO_location");
171+
return get(ID_original_GOTO_location);
172172
}
173173

174174
static bool is_built_in(const std::string &s)

0 commit comments

Comments
 (0)