Skip to content

Commit 2b9c880

Browse files
author
martin
committed
Clang format the domain files.
1 parent 028d8b6 commit 2b9c880

File tree

2 files changed

+31
-45
lines changed

2 files changed

+31
-45
lines changed

src/analyses/ai_domain.cpp

+18-21
Original file line numberDiff line numberDiff line change
@@ -13,24 +13,21 @@ Author: Daniel Kroening, [email protected]
1313

1414
#include <util/simplify_expr.h>
1515

16-
jsont ai_domain_baset::output_json(
17-
const ai_baset &ai,
18-
const namespacet &ns) const
16+
jsont ai_domain_baset::output_json(const ai_baset &ai, const namespacet &ns)
17+
const
1918
{
2019
std::ostringstream out;
2120
output(out, ai, ns);
2221
json_stringt json(out.str());
2322
return json;
2423
}
2524

26-
xmlt ai_domain_baset::output_xml(
27-
const ai_baset &ai,
28-
const namespacet &ns) const
25+
xmlt ai_domain_baset::output_xml(const ai_baset &ai, const namespacet &ns) const
2926
{
3027
std::ostringstream out;
3128
output(out, ai, ns);
3229
xmlt xml("abstract_state");
33-
xml.data=out.str();
30+
xml.data = out.str();
3431
return xml;
3532
}
3633

@@ -42,38 +39,38 @@ xmlt ai_domain_baset::output_xml(
4239
/// \param ns: the namespace
4340
/// \return True if condition did not change. False otherwise. condition will be
4441
/// updated with the simplified condition if it has worked
45-
bool ai_domain_baset::ai_simplify_lhs(
46-
exprt &condition, const namespacet &ns) const
42+
bool ai_domain_baset::ai_simplify_lhs(exprt &condition, const namespacet &ns)
43+
const
4744
{
4845
// Care must be taken here to give something that is still writable
49-
if(condition.id()==ID_index)
46+
if(condition.id() == ID_index)
5047
{
51-
index_exprt ie=to_index_expr(condition);
52-
bool no_simplification=ai_simplify(ie.index(), ns);
48+
index_exprt ie = to_index_expr(condition);
49+
bool no_simplification = ai_simplify(ie.index(), ns);
5350
if(!no_simplification)
54-
condition=simplify_expr(ie, ns);
51+
condition = simplify_expr(ie, ns);
5552

5653
return no_simplification;
5754
}
58-
else if(condition.id()==ID_dereference)
55+
else if(condition.id() == ID_dereference)
5956
{
60-
dereference_exprt de=to_dereference_expr(condition);
61-
bool no_simplification=ai_simplify(de.pointer(), ns);
57+
dereference_exprt de = to_dereference_expr(condition);
58+
bool no_simplification = ai_simplify(de.pointer(), ns);
6259
if(!no_simplification)
63-
condition=simplify_expr(de, ns); // So *(&x) -> x
60+
condition = simplify_expr(de, ns); // So *(&x) -> x
6461

6562
return no_simplification;
6663
}
67-
else if(condition.id()==ID_member)
64+
else if(condition.id() == ID_member)
6865
{
69-
member_exprt me=to_member_expr(condition);
66+
member_exprt me = to_member_expr(condition);
7067
// Since simplify_ai_lhs is required to return an addressable object
7168
// (so remains a valid left hand side), to simplify
7269
// `(something_simplifiable).b` we require that `something_simplifiable`
7370
// must also be addressable
74-
bool no_simplification=ai_simplify_lhs(me.compound(), ns);
71+
bool no_simplification = ai_simplify_lhs(me.compound(), ns);
7572
if(!no_simplification)
76-
condition=simplify_expr(me, ns);
73+
condition = simplify_expr(me, ns);
7774

7875
return no_simplification;
7976
}

src/analyses/ai_domain.h

+13-24
Original file line numberDiff line numberDiff line change
@@ -12,10 +12,10 @@ Author: Daniel Kroening, [email protected]
1212
#ifndef CPROVER_ANALYSES_AI_DOMAIN_H
1313
#define CPROVER_ANALYSES_AI_DOMAIN_H
1414

15-
#include <util/json.h>
16-
#include <util/xml.h>
1715
#include <util/expr.h>
16+
#include <util/json.h>
1817
#include <util/make_unique.h>
18+
#include <util/xml.h>
1919

2020
#include <goto-programs/goto_model.h>
2121

@@ -61,34 +61,28 @@ class ai_domain_baset
6161
ai_baset &ai,
6262
const namespacet &ns) = 0;
6363

64-
virtual void output(
65-
std::ostream &out,
66-
const ai_baset &ai,
67-
const namespacet &ns) const
64+
virtual void
65+
output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const
6866
{
6967
}
7068

71-
virtual jsont output_json(
72-
const ai_baset &ai,
73-
const namespacet &ns) const;
69+
virtual jsont output_json(const ai_baset &ai, const namespacet &ns) const;
7470

75-
virtual xmlt output_xml(
76-
const ai_baset &ai,
77-
const namespacet &ns) const;
71+
virtual xmlt output_xml(const ai_baset &ai, const namespacet &ns) const;
7872

7973
// no states
80-
virtual void make_bottom()=0;
74+
virtual void make_bottom() = 0;
8175

8276
// all states -- the analysis doesn't use this,
8377
// and domains may refuse to implement it.
84-
virtual void make_top()=0;
78+
virtual void make_top() = 0;
8579

8680
// a reasonable entry-point state
87-
virtual void make_entry()=0;
81+
virtual void make_entry() = 0;
8882

89-
virtual bool is_bottom() const=0;
83+
virtual bool is_bottom() const = 0;
9084

91-
virtual bool is_top() const=0;
85+
virtual bool is_top() const = 0;
9286

9387
// also add
9488
//
@@ -102,23 +96,18 @@ class ai_domain_baset
10296
// PRECONDITION(from.is_dereferenceable(), "Must not be _::end()")
10397
// PRECONDITION(to.is_dereferenceable(), "Must not be _::end()")
10498

105-
10699
// This method allows an expression to be simplified / evaluated using the
107100
// current state. It is used to evaluate assertions and in program
108101
// simplification
109102

110103
// return true if unchanged
111-
virtual bool ai_simplify(
112-
exprt &condition,
113-
const namespacet &ns) const
104+
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const
114105
{
115106
return true;
116107
}
117108

118109
// Simplifies the expression but keeps it as an l-value
119-
virtual bool ai_simplify_lhs(
120-
exprt &condition,
121-
const namespacet &ns) const;
110+
virtual bool ai_simplify_lhs(exprt &condition, const namespacet &ns) const;
122111

123112
// Gives a Boolean condition that is true for all values represented by the
124113
// domain. This allows domains to be converted into program invariants.

0 commit comments

Comments
 (0)