Skip to content

Commit 95396bc

Browse files
author
Daniel Kroening
authored
Merge pull request diffblue#2438 from tautschnig/vs-partial
Partial-order concurrency: Remove unused parameter
2 parents 551ab81 + 209d459 commit 95396bc

5 files changed

+5
-6
lines changed

src/goto-symex/memory_model_pso.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ void memory_model_psot::operator()(symex_target_equationt &equation)
1616
statistics() << "Adding PSO constraints" << eom;
1717

1818
build_event_lists(equation);
19-
build_clock_type(equation);
19+
build_clock_type();
2020

2121
read_from(equation);
2222
write_serialization_external(equation);

src/goto-symex/memory_model_sc.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ void memory_model_sct::operator()(symex_target_equationt &equation)
1818
statistics() << "Adding SC constraints" << eom;
1919

2020
build_event_lists(equation);
21-
build_clock_type(equation);
21+
build_clock_type();
2222

2323
read_from(equation);
2424
write_serialization_external(equation);

src/goto-symex/memory_model_tso.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ void memory_model_tsot::operator()(symex_target_equationt &equation)
1919
statistics() << "Adding TSO constraints" << eom;
2020

2121
build_event_lists(equation);
22-
build_clock_type(equation);
22+
build_clock_type();
2323

2424
read_from(equation);
2525
write_serialization_external(equation);

src/goto-symex/partial_order_concurrency.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -161,8 +161,7 @@ symbol_exprt partial_order_concurrencyt::clock(
161161
return symbol_exprt(identifier, clock_type);
162162
}
163163

164-
void partial_order_concurrencyt::build_clock_type(
165-
const symex_target_equationt &equation)
164+
void partial_order_concurrencyt::build_clock_type()
166165
{
167166
assert(!numbering.empty());
168167

src/goto-symex/partial_order_concurrency.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -77,7 +77,7 @@ class partial_order_concurrencyt:public messaget
7777
// produce a clock symbol for some event
7878
typet clock_type;
7979
symbol_exprt clock(event_it e, axiomt axiom);
80-
void build_clock_type(const symex_target_equationt &);
80+
void build_clock_type();
8181

8282
// preprocess and add a constraint to equation
8383
void add_constraint(

0 commit comments

Comments
 (0)