Skip to content

Commit fe4ea78

Browse files
committed
invariant set to_string: remove unused second parameter
The identifier is not required, and sometimes was an empty string.
1 parent d7bb1d4 commit fe4ea78

File tree

3 files changed

+13
-31
lines changed

3 files changed

+13
-31
lines changed

src/analyses/invariant_set.cpp

Lines changed: 9 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ Author: Daniel Kroening, [email protected]
2929
void inv_object_storet::output(std::ostream &out) const
3030
{
3131
for(std::size_t i=0; i<entries.size(); i++)
32-
out << "STORE " << i << ": " << to_string(i, "") << '\n';
32+
out << "STORE " << i << ": " << map[i] << '\n';
3333
}
3434

3535
bool inv_object_storet::get(const exprt &expr, unsigned &n)
@@ -313,9 +313,7 @@ tvt invariant_sett::is_le(std::pair<unsigned, unsigned> p) const
313313
return tvt::unknown();
314314
}
315315

316-
void invariant_sett::output(
317-
const irep_idt &identifier,
318-
std::ostream &out) const
316+
void invariant_sett::output(std::ostream &out) const
319317
{
320318
if(is_false)
321319
{
@@ -339,31 +337,25 @@ void invariant_sett::output(
339337
else
340338
out << " = ";
341339

342-
out << to_string(j, identifier);
340+
out << to_string(j);
343341
}
344342

345343
out << '\n';
346344
}
347345

348346
for(const auto &bounds : bounds_map)
349347
{
350-
out << to_string(bounds.first, identifier)
351-
<< " in " << bounds.second
352-
<< '\n';
348+
out << to_string(bounds.first) << " in " << bounds.second << '\n';
353349
}
354350

355351
for(const auto &le : le_set)
356352
{
357-
out << to_string(le.first, identifier)
358-
<< " <= " << to_string(le.second, identifier)
359-
<< '\n';
353+
out << to_string(le.first) << " <= " << to_string(le.second) << '\n';
360354
}
361355

362356
for(const auto &ne : ne_set)
363357
{
364-
out << to_string(ne.first, identifier)
365-
<< " != " << to_string(ne.second, identifier)
366-
<< '\n';
358+
out << to_string(ne.first) << " != " << to_string(ne.second) << '\n';
367359
}
368360
}
369361

@@ -881,19 +873,15 @@ exprt invariant_sett::get_constant(const exprt &expr) const
881873
return static_cast<const exprt &>(get_nil_irep());
882874
}
883875

884-
std::string inv_object_storet::to_string(
885-
unsigned a,
886-
const irep_idt &) const
876+
std::string inv_object_storet::to_string(unsigned a) const
887877
{
888878
return id2string(map[a]);
889879
}
890880

891-
std::string invariant_sett::to_string(
892-
unsigned a,
893-
const irep_idt &identifier) const
881+
std::string invariant_sett::to_string(unsigned a) const
894882
{
895883
PRECONDITION(object_store!=nullptr);
896-
return object_store->to_string(a, identifier);
884+
return object_store->to_string(a);
897885
}
898886

899887
bool invariant_sett::make_union(const invariant_sett &other)

src/analyses/invariant_set.h

Lines changed: 3 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -51,9 +51,7 @@ class inv_object_storet
5151

5252
void output(std::ostream &out) const;
5353

54-
std::string to_string(
55-
unsigned n,
56-
const irep_idt &identifier) const;
54+
std::string to_string(unsigned n) const;
5755

5856
protected:
5957
const namespacet &ns;
@@ -104,9 +102,7 @@ class invariant_sett
104102
{
105103
}
106104

107-
void output(
108-
const irep_idt &identifier,
109-
std::ostream &out) const;
105+
void output(std::ostream &out) const;
110106

111107
// true = added something
112108
bool make_union(const invariant_sett &other_invariants);
@@ -219,9 +215,7 @@ class invariant_sett
219215

220216
void modifies(unsigned a);
221217

222-
std::string to_string(
223-
unsigned a,
224-
const irep_idt &identifier) const;
218+
std::string to_string(unsigned a) const;
225219

226220
bool get_object(
227221
const exprt &expr,

src/analyses/invariant_set_domain.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -49,7 +49,7 @@ class invariant_set_domaint:public ai_domain_baset
4949
if(has_values.is_known())
5050
out << has_values.to_string() << '\n';
5151
else
52-
invariant_set.output("", out);
52+
invariant_set.output(out);
5353
}
5454

5555
virtual void transform(

0 commit comments

Comments
 (0)