Skip to content

Commit 5c4cd32

Browse files
jezhigginsjezhiggins
committed
Renamed wident to widen_modet
Also should_widen to could_widen - it's a request not an instruction
1 parent 4aa65ff commit 5c4cd32

33 files changed

+116
-103
lines changed

‎src/analyses/variable-sensitivity/abstract_aggregate_object.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -126,7 +126,7 @@ class abstract_aggregate_objectt : public abstract_objectt,
126126
const sharing_mapt<keyt, abstract_object_pointert, false, hash> &map1,
127127
const sharing_mapt<keyt, abstract_object_pointert, false, hash> &map2,
128128
sharing_mapt<keyt, abstract_object_pointert, false, hash> &out_map,
129-
const wident &widen_mode)
129+
const widen_modet &widen_mode)
130130
{
131131
bool modified = false;
132132

‎src/analyses/variable-sensitivity/abstract_environment.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -331,7 +331,7 @@ abstract_object_pointert abstract_environmentt::add_object_context(
331331

332332
bool abstract_environmentt::merge(
333333
const abstract_environmentt &env,
334-
wident widen_mode)
334+
widen_modet widen_mode)
335335
{
336336
// for each entry in the incoming environment we need to either add it
337337
// if it is new, or merge with the existing key if it is not present

‎src/analyses/variable-sensitivity/abstract_environment.h

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -32,10 +32,10 @@ class variable_sensitivity_object_factoryt;
3232
using variable_sensitivity_object_factory_ptrt =
3333
std::shared_ptr<variable_sensitivity_object_factoryt>;
3434

35-
enum class wident
35+
enum class widen_modet
3636
{
3737
no,
38-
should_widen
38+
could_widen
3939
};
4040

4141
class abstract_environmentt
@@ -196,7 +196,7 @@ class abstract_environmentt
196196
/// \param widen_mode: indicates if this is a widening merge
197197
///
198198
/// \return A Boolean, true when the merge has changed something
199-
virtual bool merge(const abstract_environmentt &env, wident widen_mode);
199+
virtual bool merge(const abstract_environmentt &env, widen_modet widen_mode);
200200

201201
/// This should be used as a default case / everything else has failed
202202
/// The string is so that I can easily find and diagnose cases where this

‎src/analyses/variable-sensitivity/abstract_object.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -57,7 +57,7 @@ const typet &abstract_objectt::type() const
5757

5858
abstract_object_pointert abstract_objectt::merge(
5959
const abstract_object_pointert &other,
60-
const wident &widen_mode) const
60+
const widen_modet &widen_mode) const
6161
{
6262
return abstract_object_merge(other);
6363
}
@@ -193,7 +193,7 @@ void abstract_objectt::output(
193193
abstract_objectt::merge_result abstract_objectt::merge(
194194
const abstract_object_pointert &op1,
195195
const abstract_object_pointert &op2,
196-
const wident &widen_mode)
196+
const widen_modet &widen_mode)
197197
{
198198
abstract_object_pointert result = op1->should_use_base_merge(op2)
199199
? op1->abstract_object_merge(op2)

‎src/analyses/variable-sensitivity/abstract_object.h

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,7 @@ class typet;
4343
class constant_exprt;
4444
class abstract_environmentt;
4545
class namespacet;
46-
enum class wident;
46+
enum class widen_modet;
4747

4848
#define CLONE \
4949
internal_abstract_object_pointert mutable_clone() const override \
@@ -263,7 +263,7 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
263263
static merge_result merge(
264264
const abstract_object_pointert &op1,
265265
const abstract_object_pointert &op2,
266-
const wident &widen_mode);
266+
const widen_modet &widen_mode);
267267

268268
/// Interface method for the meet operation. Decides whether to use the base
269269
/// implementation or if a more precise abstraction is attainable.
@@ -435,8 +435,9 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
435435
/// \param widen_mode: Indicates if this is a widening merge
436436
///
437437
/// \return Returns the result of the merge.
438-
virtual abstract_object_pointert
439-
merge(const abstract_object_pointert &other, const wident &widen_mode) const;
438+
virtual abstract_object_pointert merge(
439+
const abstract_object_pointert &other,
440+
const widen_modet &widen_mode) const;
440441

441442
/// Helper function for base meet. Two cases: return itself (if trivially
442443
/// contained in other); return BOTTOM otherwise.

‎src/analyses/variable-sensitivity/abstract_value_object.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -190,7 +190,7 @@ abstract_object_pointert abstract_value_objectt::write(
190190

191191
abstract_object_pointert abstract_value_objectt::merge(
192192
const abstract_object_pointert &other,
193-
const wident &widen_mode) const
193+
const widen_modet &widen_mode) const
194194
{
195195
auto cast_other =
196196
std::dynamic_pointer_cast<const abstract_value_objectt>(other);

‎src/analyses/variable-sensitivity/abstract_value_object.h

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -306,14 +306,14 @@ class abstract_value_objectt : public abstract_objectt,
306306
/// \return Returns the result of the merge
307307
abstract_object_pointert merge(
308308
const abstract_object_pointert &other,
309-
const wident &widen_mode) const final;
309+
const widen_modet &widen_mode) const final;
310310

311311
abstract_object_pointert
312312
meet(const abstract_object_pointert &other) const final;
313313

314314
virtual abstract_object_pointert merge_with_value(
315315
const abstract_value_pointert &other,
316-
const wident &widen_mode) const = 0;
316+
const widen_modet &widen_mode) const = 0;
317317

318318
virtual abstract_object_pointert
319319
meet_with_value(const abstract_value_pointert &other) const = 0;

‎src/analyses/variable-sensitivity/constant_abstract_value.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -113,7 +113,7 @@ void constant_abstract_valuet::output(
113113

114114
abstract_object_pointert constant_abstract_valuet::merge_with_value(
115115
const abstract_value_pointert &other,
116-
const wident &widen_mode) const
116+
const widen_modet &widen_mode) const
117117
{
118118
auto other_expr = other->to_constant();
119119
if(is_bottom() && other_expr.is_constant())

‎src/analyses/variable-sensitivity/constant_abstract_value.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -74,7 +74,7 @@ class constant_abstract_valuet : public abstract_value_objectt
7474
/// case it returns this.
7575
abstract_object_pointert merge_with_value(
7676
const abstract_value_pointert &other,
77-
const wident &widen_mode) const override;
77+
const widen_modet &widen_mode) const override;
7878

7979
abstract_object_pointert
8080
meet_with_value(const abstract_value_pointert &other) const override;

‎src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -58,7 +58,7 @@ constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(
5858

5959
abstract_object_pointert constant_pointer_abstract_objectt::merge(
6060
const abstract_object_pointert &other,
61-
const wident &widen_mode) const
61+
const widen_modet &widen_mode) const
6262
{
6363
auto cast_other =
6464
std::dynamic_pointer_cast<const constant_pointer_abstract_objectt>(other);
@@ -71,7 +71,7 @@ abstract_object_pointert constant_pointer_abstract_objectt::merge(
7171
abstract_object_pointert
7272
constant_pointer_abstract_objectt::merge_constant_pointers(
7373
const constant_pointer_abstract_pointert &other,
74-
const wident &widen_mode) const
74+
const widen_modet &widen_mode) const
7575
{
7676
if(is_bottom())
7777
return std::make_shared<constant_pointer_abstract_objectt>(*other);
@@ -185,7 +185,8 @@ abstract_object_pointert constant_pointer_abstract_objectt::write_dereference(
185185
{
186186
abstract_object_pointert pointed_value = environment.eval(value, ns);
187187
abstract_object_pointert merged_value =
188-
abstract_objectt::merge(pointed_value, new_value, wident::no).object;
188+
abstract_objectt::merge(pointed_value, new_value, widen_modet::no)
189+
.object;
189190
environment.assign(value, merged_value, ns);
190191
}
191192
else

‎src/analyses/variable-sensitivity/constant_pointer_abstract_object.h

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -124,7 +124,7 @@ class constant_pointer_abstract_objectt : public abstract_pointer_objectt
124124
/// \return Returns the result of the merge.
125125
abstract_object_pointert merge(
126126
const abstract_object_pointert &op1,
127-
const wident &widen_mode) const override;
127+
const widen_modet &widen_mode) const override;
128128

129129
CLONE
130130

@@ -140,7 +140,7 @@ class constant_pointer_abstract_objectt : public abstract_pointer_objectt
140140
/// case it returns this.
141141
abstract_object_pointert merge_constant_pointers(
142142
const constant_pointer_abstract_pointert &other,
143-
const wident &widen_mode) const;
143+
const widen_modet &widen_mode) const;
144144

145145
write_stackt value_stack;
146146
};

‎src/analyses/variable-sensitivity/data_dependency_context.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -237,7 +237,7 @@ abstract_object_pointert data_dependency_contextt::update_location_context(
237237
*/
238238
abstract_object_pointert data_dependency_contextt::merge(
239239
const abstract_object_pointert &other,
240-
const wident &widen_mode) const
240+
const widen_modet &widen_mode) const
241241
{
242242
auto cast_other =
243243
std::dynamic_pointer_cast<const data_dependency_contextt>(other);

‎src/analyses/variable-sensitivity/data_dependency_context.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -72,7 +72,7 @@ class data_dependency_contextt : public write_location_contextt
7272

7373
abstract_object_pointert merge(
7474
const abstract_object_pointert &other,
75-
const wident &widen_mode) const override;
75+
const widen_modet &widen_mode) const override;
7676

7777
abstract_object_pointert abstract_object_merge_internal(
7878
const abstract_object_pointert &other) const override;

‎src/analyses/variable-sensitivity/full_array_abstract_object.cpp

Lines changed: 9 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -38,9 +38,10 @@ abstract_object_pointert apply_to_index_range(
3838
{
3939
auto at_index = fn(index_exprt(index_expr.array(), index));
4040

41-
result = (result == nullptr)
42-
? at_index
43-
: abstract_objectt::merge(result, at_index, wident::no).object;
41+
result =
42+
(result == nullptr)
43+
? at_index
44+
: abstract_objectt::merge(result, at_index, widen_modet::no).object;
4445

4546
if(result->is_top()) // no point in continuing once we've gone top
4647
break;
@@ -99,7 +100,7 @@ void full_array_abstract_objectt::set_top_internal()
99100

100101
abstract_object_pointert full_array_abstract_objectt::merge(
101102
const abstract_object_pointert &other,
102-
const wident &widen_mode) const
103+
const widen_modet &widen_mode) const
103104
{
104105
auto cast_other =
105106
std::dynamic_pointer_cast<const full_array_abstract_objectt>(other);
@@ -111,7 +112,7 @@ abstract_object_pointert full_array_abstract_objectt::merge(
111112

112113
abstract_object_pointert full_array_abstract_objectt::full_array_merge(
113114
const full_array_pointert &other,
114-
const wident &widen_mode) const
115+
const widen_modet &widen_mode) const
115116
{
116117
if(is_bottom())
117118
return std::make_shared<full_array_abstract_objectt>(*other);
@@ -223,7 +224,7 @@ abstract_object_pointert full_array_abstract_objectt::read_element(
223224
// Merge each known element into the TOP value
224225
for(const auto &element : map.get_view())
225226
result =
226-
abstract_objectt::merge(result, element.second, wident::no).object;
227+
abstract_objectt::merge(result, element.second, widen_modet::no).object;
227228

228229
return result;
229230
}
@@ -337,7 +338,8 @@ abstract_object_pointert full_array_abstract_objectt::write_leaf_element(
337338
{
338339
result->map.replace(
339340
index_value,
340-
abstract_objectt::merge(old_value.value(), value, wident::no).object);
341+
abstract_objectt::merge(old_value.value(), value, widen_modet::no)
342+
.object);
341343
}
342344

343345
DATA_INVARIANT(result->verify(), "Structural invariants maintained");

‎src/analyses/variable-sensitivity/full_array_abstract_object.h

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -129,7 +129,7 @@ class full_array_abstract_objectt : public abstract_aggregate_objectt<
129129
/// \return Returns the result of the merge.
130130
abstract_object_pointert merge(
131131
const abstract_object_pointert &other,
132-
const wident &widen_mode) const override;
132+
const widen_modet &widen_mode) const override;
133133

134134
/// To validate that the struct object is in a valid state.
135135
/// This means either it is top or bottom, or if neither of those
@@ -213,7 +213,7 @@ class full_array_abstract_objectt : public abstract_aggregate_objectt<
213213
/// case it returns this..
214214
abstract_object_pointert full_array_merge(
215215
const full_array_pointert &other,
216-
const wident &widen_mode) const;
216+
const widen_modet &widen_mode) const;
217217
};
218218

219219
#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_ARRAY_ABSTRACT_OBJECT_H

‎src/analyses/variable-sensitivity/full_struct_abstract_object.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -178,7 +178,8 @@ abstract_object_pointert full_struct_abstract_objectt::write_component(
178178

179179
result->map.replace(
180180
c,
181-
abstract_objectt::merge(old_value.value(), value, wident::no).object);
181+
abstract_objectt::merge(old_value.value(), value, widen_modet::no)
182+
.object);
182183
}
183184
else
184185
{
@@ -240,7 +241,7 @@ bool full_struct_abstract_objectt::verify() const
240241

241242
abstract_object_pointert full_struct_abstract_objectt::merge(
242243
const abstract_object_pointert &other,
243-
const wident &widen_mode) const
244+
const widen_modet &widen_mode) const
244245
{
245246
constant_struct_pointert cast_other =
246247
std::dynamic_pointer_cast<const full_struct_abstract_objectt>(other);
@@ -252,7 +253,7 @@ abstract_object_pointert full_struct_abstract_objectt::merge(
252253

253254
abstract_object_pointert full_struct_abstract_objectt::merge_constant_structs(
254255
constant_struct_pointert other,
255-
const wident &widen_mode) const
256+
const widen_modet &widen_mode) const
256257
{
257258
if(is_bottom())
258259
return std::make_shared<full_struct_abstract_objectt>(*other);

‎src/analyses/variable-sensitivity/full_struct_abstract_object.h

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -102,7 +102,7 @@ class full_struct_abstract_objectt : public abstract_aggregate_objectt<
102102
/// case it returns this.
103103
abstract_object_pointert merge_constant_structs(
104104
constant_struct_pointert other,
105-
const wident &widen_mode) const;
105+
const widen_modet &widen_mode) const;
106106

107107
protected:
108108
CLONE
@@ -168,7 +168,7 @@ class full_struct_abstract_objectt : public abstract_aggregate_objectt<
168168
/// \return Returns the result of the merge.
169169
abstract_object_pointert merge(
170170
const abstract_object_pointert &other,
171-
const wident &widen_mode) const override;
171+
const widen_modet &widen_mode) const override;
172172
};
173173

174174
#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_STRUCT_ABSTRACT_OBJECT_H

‎src/analyses/variable-sensitivity/interval_abstract_value.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -354,7 +354,7 @@ void interval_abstract_valuet::output(
354354
/// this and other
355355
abstract_object_pointert interval_abstract_valuet::merge_with_value(
356356
const abstract_value_pointert &other,
357-
const wident &widen_mode) const
357+
const widen_modet &widen_mode) const
358358
{
359359
if(other->is_bottom())
360360
return shared_from_this();

‎src/analyses/variable-sensitivity/interval_abstract_value.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -65,7 +65,7 @@ class interval_abstract_valuet : public abstract_value_objectt
6565

6666
abstract_object_pointert merge_with_value(
6767
const abstract_value_pointert &other,
68-
const wident &widen_mode) const override;
68+
const widen_modet &widen_mode) const override;
6969

7070
abstract_object_pointert
7171
meet_with_value(const abstract_value_pointert &other) const override;

‎src/analyses/variable-sensitivity/value_set_abstract_object.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -193,7 +193,7 @@ constant_interval_exprt value_set_abstract_objectt::to_interval() const
193193

194194
abstract_object_pointert value_set_abstract_objectt::merge_with_value(
195195
const abstract_value_pointert &other,
196-
const wident &widen_mode) const
196+
const widen_modet &widen_mode) const
197197
{
198198
auto union_values = !is_bottom() ? values : abstract_object_sett{};
199199

‎src/analyses/variable-sensitivity/value_set_abstract_object.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -66,7 +66,7 @@ class value_set_abstract_objectt : public abstract_value_objectt,
6666

6767
abstract_object_pointert merge_with_value(
6868
const abstract_value_pointert &other,
69-
const wident &widen_mode) const override;
69+
const widen_modet &widen_mode) const override;
7070

7171
abstract_object_pointert
7272
meet_with_value(const abstract_value_pointert &other) const override;

‎src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -158,7 +158,7 @@ abstract_object_pointert value_set_pointer_abstract_objectt::resolve_values(
158158

159159
abstract_object_pointert value_set_pointer_abstract_objectt::merge(
160160
const abstract_object_pointert &other,
161-
const wident &widen_mode) const
161+
const widen_modet &widen_mode) const
162162
{
163163
auto cast_other = std::dynamic_pointer_cast<const value_set_tag>(other);
164164
if(cast_other)

‎src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -73,7 +73,7 @@ class value_set_pointer_abstract_objectt : public abstract_pointer_objectt,
7373
/// \copydoc abstract_object::merge
7474
abstract_object_pointert merge(
7575
const abstract_object_pointert &other,
76-
const wident &widen_mode) const override;
76+
const widen_modet &widen_mode) const override;
7777

7878
private:
7979
/// Update the set of stored values to \p new_values. Build a new abstract

‎src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -204,7 +204,8 @@ bool variable_sensitivity_domaint::merge(
204204
std::cout << "Merging from/to:\n " << from->location_number << " --> "
205205
<< to->location_number << '\n';
206206
#endif
207-
auto widen_mode = from->should_widen(*to) ? wident::should_widen : wident::no;
207+
auto widen_mode =
208+
from->should_widen(*to) ? widen_modet::could_widen : widen_modet::no;
208209
// Use the abstract_environment merge
209210
bool any_changes = abstract_state.merge(b.abstract_state, widen_mode);
210211

‎src/analyses/variable-sensitivity/write_location_context.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -112,7 +112,7 @@ abstract_object_pointert write_location_contextt::write(
112112
*/
113113
abstract_object_pointert write_location_contextt::merge(
114114
const abstract_object_pointert &other,
115-
const wident &widen_mode) const
115+
const widen_modet &widen_mode) const
116116
{
117117
auto cast_other =
118118
std::dynamic_pointer_cast<const write_location_contextt>(other);

‎src/analyses/variable-sensitivity/write_location_context.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -101,7 +101,7 @@ class write_location_contextt : public context_abstract_objectt
101101

102102
abstract_object_pointert merge(
103103
const abstract_object_pointert &other,
104-
const wident &widen_mode) const override;
104+
const widen_modet &widen_mode) const override;
105105
abstract_object_pointert
106106
meet(const abstract_object_pointert &other) const override;
107107

0 commit comments

Comments
 (0)