Skip to content

Commit f340f08

Browse files
author
Daniel Kroening
committed
symex_targett::sourcet now knows the function identifier
1 parent 4d2905f commit f340f08

9 files changed

+29
-30
lines changed

‎src/goto-symex/build_goto_trace.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -156,7 +156,7 @@ void update_internal_field(
156156
}
157157

158158
// set internal field to _start function-return step
159-
if(SSA_step.source.pc->function==goto_functionst::entry_point())
159+
if(SSA_step.source.function == goto_functionst::entry_point())
160160
{
161161
// "__CPROVER_*" function calls in __CPROVER_start are already marked as
162162
// internal. Don't mark any other function calls (i.e. "main"), function

‎src/goto-symex/show_program.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ void show_program(const namespacet &ns, const symex_target_equationt &equation)
2929
{
3030
std::cout << "// " << step.source.pc->location_number << " ";
3131
std::cout << step.source.pc->source_location.as_string() << "\n";
32-
const irep_idt &function = step.source.pc->function;
32+
const irep_idt &function = step.source.function;
3333

3434
if(step.is_assignment())
3535
{

‎src/goto-symex/show_vcc.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -64,7 +64,7 @@ void show_vcc_plain(
6464
if(!p_it->ignore)
6565
{
6666
std::string string_value =
67-
from_expr(ns, p_it->source.pc->function, p_it->cond_expr);
67+
from_expr(ns, p_it->source.function, p_it->cond_expr);
6868
out << "{-" << count << "} " << string_value << "\n";
6969

7070
#if 0
@@ -84,7 +84,7 @@ void show_vcc_plain(
8484
out << '\n';
8585

8686
std::string string_value =
87-
from_expr(ns, s_it->source.pc->function, s_it->cond_expr);
87+
from_expr(ns, s_it->source.function, s_it->cond_expr);
8888
out << "{" << 1 << "} " << string_value << "\n";
8989
}
9090
}
@@ -135,13 +135,13 @@ void show_vcc_json(
135135
!p_it->ignore)
136136
{
137137
std::string string_value =
138-
from_expr(ns, p_it->source.pc->function, p_it->cond_expr);
138+
from_expr(ns, p_it->source.function, p_it->cond_expr);
139139
json_constraints.push_back(json_stringt(string_value));
140140
}
141141
}
142142

143143
std::string string_value =
144-
from_expr(ns, s_it->source.pc->function, s_it->cond_expr);
144+
from_expr(ns, s_it->source.function, s_it->cond_expr);
145145
object["expression"] = json_stringt(string_value);
146146
}
147147

‎src/goto-symex/symex_builtin_functions.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -55,8 +55,8 @@ void goto_symext::symex_allocate(
5555

5656
exprt size=code.op0();
5757
typet object_type=nil_typet();
58-
auto function_symbol = outer_symbol_table.lookup(state.source.pc->function);
59-
INVARIANT(function_symbol, "function associated with instruction not found");
58+
auto function_symbol = outer_symbol_table.lookup(state.source.function);
59+
INVARIANT(function_symbol, "function associated with allocation not found");
6060
const irep_idt &mode = function_symbol->mode;
6161

6262
// is the type given?

‎src/goto-symex/symex_dereference.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -258,7 +258,7 @@ void goto_symext::dereference_rec(
258258

259259
if(state.threads.size() == 1)
260260
{
261-
const irep_idt &expr_function = state.source.pc->function;
261+
const irep_idt &expr_function = state.source.function;
262262
if(!expr_function.empty())
263263
{
264264
state.get_original_name(to_check);

‎src/goto-symex/symex_function_call.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -358,7 +358,7 @@ void goto_symext::symex_end_of_function(statet &state)
358358
{
359359
// first record the return
360360
target.function_return(
361-
state.guard.as_expr(), state.source.pc->function, state.source);
361+
state.guard.as_expr(), state.source.function, state.source);
362362

363363
// then get rid of the frame
364364
pop_frame(state);

‎src/goto-symex/symex_main.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -260,7 +260,7 @@ void goto_symext::symex_instruction_range(
260260
{
261261
initialize_entry_point(state, get_goto_function, first, limit);
262262
ns = namespacet(outer_symbol_table, state.symbol_table);
263-
while(state.source.pc->function!=limit->function || state.source.pc!=limit)
263+
while(state.source.function != limit->function || state.source.pc != limit)
264264
symex_threaded_step(state, get_goto_function);
265265
}
266266

‎src/goto-symex/symex_target.h

Lines changed: 11 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -29,27 +29,26 @@ class symex_targett
2929
struct sourcet
3030
{
3131
unsigned thread_nr;
32+
irep_idt function;
3233
goto_programt::const_targett pc;
3334
bool is_set;
3435

35-
sourcet():
36-
thread_nr(0),
37-
is_set(false)
36+
sourcet() : thread_nr(0), function(irep_idt()), is_set(false)
3837
{
3938
}
4039

41-
explicit sourcet(
42-
goto_programt::const_targett _pc):
43-
thread_nr(0),
44-
pc(_pc),
45-
is_set(true)
40+
sourcet(const irep_idt &_function, goto_programt::const_targett _pc)
41+
: thread_nr(0), function(_function), pc(_pc), is_set(true)
4642
{
4743
}
4844

49-
explicit sourcet(const goto_programt &_goto_program):
50-
thread_nr(0),
51-
pc(_goto_program.instructions.begin()),
52-
is_set(true)
45+
explicit sourcet(
46+
const irep_idt &_function,
47+
const goto_programt &_goto_program)
48+
: thread_nr(0),
49+
function(_function),
50+
pc(_goto_program.instructions.begin()),
51+
is_set(true)
5352
{
5453
}
5554
};

‎src/goto-symex/symex_target_equation.cpp

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -776,10 +776,10 @@ void symex_target_equationt::SSA_stept::output(
776776
switch(type)
777777
{
778778
case goto_trace_stept::typet::ASSERT:
779-
out << "ASSERT " << from_expr(ns, source.pc->function, cond_expr) << '\n';
779+
out << "ASSERT " << from_expr(ns, source.function, cond_expr) << '\n';
780780
break;
781781
case goto_trace_stept::typet::ASSUME:
782-
out << "ASSUME " << from_expr(ns, source.pc->function, cond_expr) << '\n';
782+
out << "ASSUME " << from_expr(ns, source.function, cond_expr) << '\n';
783783
break;
784784
case goto_trace_stept::typet::LOCATION:
785785
out << "LOCATION" << '\n'; break;
@@ -790,7 +790,7 @@ void symex_target_equationt::SSA_stept::output(
790790

791791
case goto_trace_stept::typet::DECL:
792792
out << "DECL" << '\n';
793-
out << from_expr(ns, source.pc->function, ssa_lhs) << '\n';
793+
out << from_expr(ns, source.function, ssa_lhs) << '\n';
794794
break;
795795

796796
case goto_trace_stept::typet::ASSIGNMENT:
@@ -844,22 +844,22 @@ void symex_target_equationt::SSA_stept::output(
844844
case goto_trace_stept::typet::MEMORY_BARRIER:
845845
out << "MEMORY_BARRIER\n"; break;
846846
case goto_trace_stept::typet::GOTO:
847-
out << "IF " << from_expr(ns, source.pc->function, cond_expr) << " GOTO\n";
847+
out << "IF " << from_expr(ns, source.function, cond_expr) << " GOTO\n";
848848
break;
849849

850850
default: UNREACHABLE;
851851
}
852852

853853
if(is_assert() || is_assume() || is_assignment() || is_constraint())
854-
out << from_expr(ns, source.pc->function, cond_expr) << '\n';
854+
out << from_expr(ns, source.function, cond_expr) << '\n';
855855

856856
if(is_assert() || is_constraint())
857857
out << comment << '\n';
858858

859859
if(is_shared_read() || is_shared_write())
860-
out << from_expr(ns, source.pc->function, ssa_lhs) << '\n';
860+
out << from_expr(ns, source.function, ssa_lhs) << '\n';
861861

862-
out << "Guard: " << from_expr(ns, source.pc->function, guard) << '\n';
862+
out << "Guard: " << from_expr(ns, source.function, guard) << '\n';
863863
}
864864

865865
void symex_target_equationt::SSA_stept::output(std::ostream &out) const

0 commit comments

Comments
 (0)