Skip to content

Commit 367d426

Browse files
author
martin
committed
Fix all of the linting errors
1 parent c796ee0 commit 367d426

32 files changed

+125
-113
lines changed

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

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -491,8 +491,6 @@ Function: abstract_environmentt::merge
491491
492492
\*******************************************************************/
493493

494-
#include <iostream>
495-
496494
bool abstract_environmentt::merge(const abstract_environmentt &env)
497495
{
498496
// Use the sharing_map's "iterative over all differences" functionality

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,7 @@ class abstract_environmentt;
4343
class namespacet;
4444

4545
#define CLONE \
46-
virtual internal_abstract_object_pointert mutable_clone() const override \
46+
internal_abstract_object_pointert mutable_clone() const override \
4747
{ \
4848
typedef std::remove_const< \
4949
std::remove_reference<decltype(*this)>::type>::type current_typet; \

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,11 @@
1+
/*******************************************************************\
2+
3+
Module: Variable Sensitivity Domain
4+
5+
Author: Hannes Steffenhagen
6+
7+
\*******************************************************************/
8+
19
#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_OBJECT_STATISTICS_H
210
#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_OBJECT_STATISTICS_H
311

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -24,12 +24,12 @@ class array_abstract_objectt : public abstract_objectt
2424
const abstract_environmentt &environment,
2525
const namespacet &ns);
2626

27-
virtual abstract_object_pointert read(
27+
abstract_object_pointert read(
2828
const abstract_environmentt &env,
2929
const exprt &specifier,
3030
const namespacet &ns) const override;
3131

32-
virtual abstract_object_pointert write(
32+
abstract_object_pointert write(
3333
abstract_environmentt &environment,
3434
const namespacet &ns,
3535
const std::stack<exprt> stack,

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,7 @@ abstract_object_pointert constant_abstract_valuet::expression_transform(
4848
// try finding the rounding mode. If it's not constant, try
4949
// seeing if we can get the same result with all rounding modes
5050
auto rounding_mode_symbol =
51-
symbol_exprt("__CPROVER_rounding_mode", signedbv_typet(32));
51+
symbol_exprt(CPROVER_PREFIX "rounding_mode", signedbv_typet(32));
5252
auto rounding_mode_value = environment.eval(rounding_mode_symbol, ns);
5353
auto rounding_mode_constant = rounding_mode_value->to_constant();
5454
if(rounding_mode_constant.is_nil())
@@ -103,7 +103,7 @@ constant_abstract_valuet::try_transform_expr_with_all_rounding_modes(
103103
const namespacet &ns) const
104104
{
105105
const symbol_exprt rounding_mode_symbol =
106-
symbol_exprt("__CPROVER_rounding_mode", signedbv_typet(32));
106+
symbol_exprt(CPROVER_PREFIX "rounding_mode", signedbv_typet(32));
107107
// NOLINTNEXTLINE (whitespace/braces)
108108
auto rounding_modes = std::array<ieee_floatt::rounding_modet, 4>{
109109
// NOLINTNEXTLINE (whitespace/braces)

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

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -31,15 +31,15 @@ class constant_abstract_valuet : public abstract_valuet
3131
{
3232
}
3333

34-
virtual abstract_object_pointert expression_transform(
34+
abstract_object_pointert expression_transform(
3535
const exprt &expr,
3636
const std::vector<abstract_object_pointert> &operands,
3737
const abstract_environmentt &environment,
3838
const namespacet &ns) const override;
3939

40-
virtual exprt to_constant() const override;
40+
exprt to_constant() const override;
4141

42-
virtual void output(
42+
void output(
4343
std::ostream &out,
4444
const class ai_baset &ai,
4545
const class namespacet &ns) const override;
@@ -64,8 +64,7 @@ class constant_abstract_valuet : public abstract_valuet
6464

6565
protected:
6666
CLONE
67-
virtual abstract_object_pointert
68-
merge(abstract_object_pointert other) const override;
67+
abstract_object_pointert merge(abstract_object_pointert other) const override;
6968

7069
abstract_object_pointert try_transform_expr_with_all_rounding_modes(
7170
const exprt &expr,

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -183,7 +183,7 @@ abstract_object_pointert constant_array_abstract_objectt::constant_array_merge(
183183
mutable_clone());
184184

185185
bool modified =
186-
abstract_objectt::merge_shared_maps<mp_integer, mp_integer_hash>(
186+
abstract_objectt::merge_shared_maps<mp_integer, mp_integer_hasht>(
187187
map, other->map, result->map);
188188

189189
if(!modified)

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

Lines changed: 8 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@ class constant_array_abstract_objectt : public array_abstract_objectt
3737
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns)
3838
const override;
3939

40-
virtual abstract_object_pointert
40+
abstract_object_pointert
4141
visit_sub_elements(const abstract_object_visitort &visitor) const override;
4242

4343
void get_statistics(
@@ -49,24 +49,23 @@ class constant_array_abstract_objectt : public array_abstract_objectt
4949
protected:
5050
CLONE
5151

52-
virtual abstract_object_pointert read_index(
52+
abstract_object_pointert read_index(
5353
const abstract_environmentt &env,
5454
const index_exprt &index,
5555
const namespacet &ns) const override;
5656

57-
virtual sharing_ptrt<array_abstract_objectt> write_index(
57+
sharing_ptrt<array_abstract_objectt> write_index(
5858
abstract_environmentt &environment,
5959
const namespacet &ns,
6060
const std::stack<exprt> stack,
6161
const index_exprt &index_expr,
6262
const abstract_object_pointert value,
6363
bool merging_write) const override;
6464

65-
virtual abstract_object_pointert
66-
merge(abstract_object_pointert other) const override;
65+
abstract_object_pointert merge(abstract_object_pointert other) const override;
6766

68-
virtual bool verify() const override;
69-
virtual void make_top_internal() override;
67+
bool verify() const override;
68+
void make_top_internal() override;
7069

7170
virtual bool eval_index(
7271
const index_exprt &index,
@@ -78,7 +77,7 @@ class constant_array_abstract_objectt : public array_abstract_objectt
7877
// Since we don't store for any index where the value is top
7978
// we don't use a regular array but instead a map of array indices
8079
// to the value at that index
81-
struct mp_integer_hash
80+
struct mp_integer_hasht
8281
{
8382
size_t operator()(const mp_integer &i) const
8483
{
@@ -90,7 +89,7 @@ class constant_array_abstract_objectt : public array_abstract_objectt
9089
mp_integer,
9190
abstract_object_pointert,
9291
false,
93-
mp_integer_hash>
92+
mp_integer_hasht>
9493
shared_array_mapt;
9594

9695
shared_array_mapt map;

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

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -54,8 +54,7 @@ class constant_pointer_abstract_objectt : public pointer_abstract_objectt
5454
const namespacet &ns) const override;
5555

5656
protected:
57-
virtual abstract_object_pointert
58-
merge(abstract_object_pointert op1) const override;
57+
abstract_object_pointert merge(abstract_object_pointert op1) const override;
5958

6059
CLONE
6160

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

Lines changed: 10 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -59,17 +59,17 @@ class context_abstract_objectt : public abstract_objectt
5959
return child_abstract_object->type();
6060
}
6161

62-
virtual bool is_top() const override
62+
bool is_top() const override
6363
{
6464
return child_abstract_object->is_top();
6565
}
6666

67-
virtual bool is_bottom() const override
67+
bool is_bottom() const override
6868
{
6969
return child_abstract_object->is_bottom();
7070
}
7171

72-
virtual exprt to_constant() const override
72+
exprt to_constant() const override
7373
{
7474
return child_abstract_object->to_constant();
7575
}
@@ -80,10 +80,8 @@ class context_abstract_objectt : public abstract_objectt
8080
const abstract_environmentt &environment,
8181
const namespacet &ns) const override;
8282

83-
virtual void output(
84-
std::ostream &out,
85-
const class ai_baset &ai,
86-
const namespacet &ns) const override;
83+
void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns)
84+
const override;
8785

8886
abstract_object_pointert unwrap_context() const override;
8987

@@ -105,24 +103,23 @@ class context_abstract_objectt : public abstract_objectt
105103

106104
// These are internal hooks that allow sub-classes to perform additional
107105
// actions when an abstract_object is set/unset to TOP
108-
virtual void make_top_internal() override;
109-
virtual void clear_top_internal() override;
106+
void make_top_internal() override;
107+
void clear_top_internal() override;
110108

111-
virtual abstract_object_pointert read(
109+
abstract_object_pointert read(
112110
const abstract_environmentt &env,
113111
const exprt &specifier,
114112
const namespacet &ns) const override;
115113

116-
virtual abstract_object_pointert write(
114+
abstract_object_pointert write(
117115
abstract_environmentt &environment,
118116
const namespacet &ns,
119117
const std::stack<exprt> stack,
120118
const exprt &specifier,
121119
const abstract_object_pointert value,
122120
bool merging_write) const override;
123121

124-
virtual bool
125-
has_been_modified(const abstract_object_pointert before) const override;
122+
bool has_been_modified(const abstract_object_pointert before) const override;
126123
};
127124

128125
#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_CONTEXT_ABSTRACT_OBJECT_H

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

Lines changed: 6 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -47,15 +47,15 @@ class data_dependency_contextt : public write_location_contextt
4747
{
4848
}
4949

50-
virtual abstract_object_pointert write(
50+
abstract_object_pointert write(
5151
abstract_environmentt &environment,
5252
const namespacet &ns,
5353
const std::stack<exprt> stack,
5454
const exprt &specifier,
5555
const abstract_object_pointert value,
5656
bool merging_write) const override;
5757

58-
virtual abstract_object_pointert update_location_context(
58+
abstract_object_pointert update_location_context(
5959
const abstract_objectt::locationst &locations,
6060
const bool update_sub_elements) const override;
6161

@@ -64,18 +64,15 @@ class data_dependency_contextt : public write_location_contextt
6464
std::set<goto_programt::const_targett> get_data_dependencies() const;
6565
std::set<goto_programt::const_targett> get_data_dominators() const;
6666

67-
virtual void output(
68-
std::ostream &out,
69-
const class ai_baset &ai,
70-
const namespacet &ns) const override;
67+
void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns)
68+
const override;
7169

7270
protected:
7371
CLONE
7472

75-
virtual abstract_object_pointert
76-
merge(abstract_object_pointert other) const override;
73+
abstract_object_pointert merge(abstract_object_pointert other) const override;
7774

78-
virtual abstract_object_pointert abstract_object_merge_internal(
75+
abstract_object_pointert abstract_object_merge_internal(
7976
const abstract_object_pointert other) const override;
8077

8178
private:

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

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -145,8 +145,7 @@ abstract_object_pointert full_struct_abstract_objectt::read_component(
145145
const namespacet &ns) const
146146
{
147147
#ifdef DEBUG
148-
std::cout << "Reading component " << member_expr.get_component_name()
149-
<< std::endl;
148+
std::cout << "Reading component " << member_expr.get_component_name() << '\n';
150149
#endif
151150

152151
if(is_top())
@@ -203,8 +202,7 @@ full_struct_abstract_objectt::write_component(
203202
bool merging_write) const
204203
{
205204
#ifdef DEBUG
206-
std::cout << "Writing component " << member_expr.get_component_name()
207-
<< std::endl;
205+
std::cout << "Writing component " << member_expr.get_component_name() << '\n';
208206
#endif
209207

210208
if(is_bottom())

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

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -35,12 +35,12 @@ class full_struct_abstract_objectt : public struct_abstract_objectt
3535
const abstract_environmentt &environment,
3636
const namespacet &ns);
3737

38-
virtual void output(
38+
void output(
3939
std::ostream &out,
4040
const class ai_baset &ai,
4141
const class namespacet &ns) const override;
4242

43-
virtual abstract_object_pointert
43+
abstract_object_pointert
4444
visit_sub_elements(const abstract_object_visitort &visitor) const override;
4545

4646
void get_statistics(
@@ -62,24 +62,23 @@ class full_struct_abstract_objectt : public struct_abstract_objectt
6262
CLONE
6363

6464
// struct interface
65-
virtual abstract_object_pointert read_component(
65+
abstract_object_pointert read_component(
6666
const abstract_environmentt &environment,
6767
const member_exprt &member_expr,
6868
const namespacet &ns) const override;
6969

70-
virtual sharing_ptrt<struct_abstract_objectt> write_component(
70+
sharing_ptrt<struct_abstract_objectt> write_component(
7171
abstract_environmentt &environment,
7272
const namespacet &ns,
7373
const std::stack<exprt> &stack,
7474
const member_exprt &member_expr,
7575
const abstract_object_pointert value,
7676
bool merging_write) const override;
7777

78-
virtual bool verify() const override;
78+
bool verify() const override;
7979
// Set the state of this to the merge result of op1 and op2 and
8080
// return if the result is different from op1
81-
virtual abstract_object_pointert
82-
merge(abstract_object_pointert other) const override;
81+
abstract_object_pointert merge(abstract_object_pointert other) const override;
8382
};
8483

8584
#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_STRUCT_ABSTRACT_OBJECT_H

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

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@ class interval_abstract_valuet : public abstract_valuet
3737

3838
~interval_abstract_valuet() override = default;
3939

40-
virtual exprt to_constant() const override;
40+
exprt to_constant() const override;
4141

4242
// Interface for transforms
4343
abstract_object_pointert expression_transform(
@@ -46,7 +46,7 @@ class interval_abstract_valuet : public abstract_valuet
4646
const abstract_environmentt &environment,
4747
const namespacet &ns) const override;
4848

49-
virtual void output(
49+
void output(
5050
std::ostream &out,
5151
const class ai_baset &ai,
5252
const class namespacet &ns) const override;
@@ -61,8 +61,7 @@ class interval_abstract_valuet : public abstract_valuet
6161

6262
protected:
6363
CLONE
64-
virtual abstract_object_pointert
65-
merge(abstract_object_pointert other) const override;
64+
abstract_object_pointert merge(abstract_object_pointert other) const override;
6665
abstract_object_pointert
6766
meet(const abstract_object_pointert &other) const override;
6867

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,8 @@ Author: Diffblue Ltd.
66
77
\*******************************************************************/
88

9-
#ifndef PROJECT_INTERVAL_ARRAY_ABSTRACT_OBJECTT_H
10-
#define PROJECT_INTERVAL_ARRAY_ABSTRACT_OBJECTT_H
9+
#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_INTERVAL_ARRAY_ABSTRACT_OBJECT_H
10+
#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_INTERVAL_ARRAY_ABSTRACT_OBJECT_H
1111

1212
#include "constant_array_abstract_object.h"
1313

@@ -52,4 +52,4 @@ class interval_array_abstract_objectt : public constant_array_abstract_objectt
5252
const namespacet &ns) const override;
5353
};
5454

55-
#endif //PROJECT_INTERVAL_ARRAY_ABSTRACT_OBJECTT_H
55+
#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_INTERVAL_ARRAY_ABSTRACT_OBJECT_H

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -26,12 +26,12 @@ class pointer_abstract_objectt : public abstract_objectt
2626
const abstract_environmentt &environment,
2727
const namespacet &ns);
2828

29-
virtual abstract_object_pointert read(
29+
abstract_object_pointert read(
3030
const abstract_environmentt &env,
3131
const exprt &specifier,
3232
const namespacet &ns) const override;
3333

34-
virtual abstract_object_pointert write(
34+
abstract_object_pointert write(
3535
abstract_environmentt &environment,
3636
const namespacet &ns,
3737
const std::stack<exprt> stack,

0 commit comments

Comments
 (0)