File tree Expand file tree Collapse file tree 9 files changed +21
-22
lines changed
regression/goto-instrument/store_goto_locations Expand file tree Collapse file tree 9 files changed +21
-22
lines changed Original file line number Diff line number Diff line change 6
6
Original GOTO location
7
7
--
8
8
--
9
- This is tracked by the JIRA issue TYT-4: https://diffblue.atlassian.net/projects/TYT/issues/TYT-4
Original file line number Diff line number Diff line change @@ -233,9 +233,11 @@ xmlt ai_baset::output_xml(
233
233
i_it->source_location .as_string ());
234
234
auto original_location = i_it->source_location .get_goto_location ();
235
235
if (original_location!=" " )
236
+ {
236
237
location.set_attribute (
237
- " originalGOTOLocation " ,
238
+ " original_GOTO_Location " ,
238
239
id2string (original_location));
240
+ }
239
241
240
242
location.new_element (find_state (i_it).output_xml (*this , ns));
241
243
Original file line number Diff line number Diff line change @@ -436,10 +436,9 @@ int goto_instrument_parse_optionst::doit()
436
436
437
437
if (cmdline.isset (" store-goto-locations" ))
438
438
{
439
- Forall_goto_functions (it, goto_functions)
439
+ for ( auto &function : goto_functions. function_map )
440
440
{
441
- auto &function_body = it->second .body ;
442
- store_goto_locations (function_body);
441
+ store_goto_locations (function.second .body );
443
442
}
444
443
}
445
444
Original file line number Diff line number Diff line change 5
5
6
6
void store_goto_locations (goto_programt &goto_program)
7
7
{
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++)
11
11
{
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 ;
14
14
15
- source_location.set_goto_location (location_number);
15
+ source_location.set_goto_location (location_number);
16
16
}
17
17
}
Original file line number Diff line number Diff line change @@ -8,12 +8,12 @@ Date: August 2017
8
8
9
9
\*******************************************************************/
10
10
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
13
13
14
14
15
15
#include <goto-programs/goto_program.h>
16
16
17
17
void store_goto_locations (goto_programt & goto_program );
18
18
19
- #endif // STORE_GOTO_LOCATION_H
19
+ #endif // CPROVER_GOTO_INSTRUMENT_STORE_GOTO_LOCATION_H
Original file line number Diff line number Diff line change @@ -48,15 +48,11 @@ std::ostream &goto_programt::output_instruction(
48
48
std::ostream &out,
49
49
const goto_program_templatet::instructiont &instruction) const
50
50
{
51
+ out << " // " << instruction.location_number << " " ;
51
52
auto original_location=instruction.source_location .get_goto_location ();
52
53
if (original_location!=" " )
53
54
{
54
- out << " // " << instruction.location_number << " "
55
- << " (Original GOTO location: " << original_location << " ) " ;
56
- }
57
- else
58
- {
59
- out << " // " << instruction.location_number << " " ;
55
+ out << " (Original GOTO location: " << original_location << " ) " ;
60
56
}
61
57
62
58
if (!instruction.source_location .is_nil ())
Original file line number Diff line number Diff line change @@ -69,8 +69,10 @@ json_objectt show_goto_functions_jsont::convert(
69
69
json (instruction.code .source_location ());
70
70
71
71
if (instruction.code .source_location ().get_goto_location ()!=" " )
72
+ {
72
73
instruction_entry[" originalGOTOLocation" ]=
73
74
json_stringt (id2string (instruction.code .source_location ().get_goto_location ()));
75
+ }
74
76
}
75
77
76
78
std::ostringstream instruction_builder;
Original file line number Diff line number Diff line change @@ -810,6 +810,7 @@ IREP_ID_ONE(cprover_string_to_upper_case_func)
810
810
IREP_ID_ONE(cprover_string_trim_func)
811
811
IREP_ID_ONE(cprover_string_value_of_func)
812
812
IREP_ID_ONE(array_replace)
813
+ IREP_ID_ONE(original_GOTO_location)
813
814
814
815
#undef IREP_ID_ONE
815
816
#undef IREP_ID_TWO
Original file line number Diff line number Diff line change @@ -142,12 +142,12 @@ class source_locationt:public irept
142
142
143
143
void set_goto_location (unsigned location)
144
144
{
145
- set (" GOTO_location " , location);
145
+ set (ID_original_GOTO_location , location);
146
146
}
147
147
148
148
const irep_idt get_goto_location () const
149
149
{
150
- return get (" GOTO_location " );
150
+ return get (ID_original_GOTO_location );
151
151
}
152
152
153
153
static bool is_built_in (const std::string &s)
You can’t perform that action at this time.
0 commit comments