Skip to content

Commit 93a0994

Browse files
Daniel Kroeningsvorenova
Daniel Kroening
authored and
svorenova
committed
clang-format the moved files
1 parent 39a03aa commit 93a0994

34 files changed

+895
-894
lines changed

‎jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp

Lines changed: 35 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -8,28 +8,36 @@ Author: Jesse Sigal, [email protected]
88

99
#include <testing-utils/catch.hpp>
1010

11-
#include <numeric>
1211
#include <java_bytecode/java_bytecode_language.h>
1312
#include <java_bytecode/java_types.h>
13+
#include <numeric>
1414

15-
#include <langapi/mode.h>
1615
#include <langapi/language_util.h>
16+
#include <langapi/mode.h>
1717

18-
#include <solvers/strings/string_constraint_instantiation.h>
1918
#include <solvers/sat/satcheck.h>
19+
#include <solvers/strings/string_constraint_instantiation.h>
2020

21-
#include <util/simplify_expr.h>
2221
#include <util/config.h>
22+
#include <util/simplify_expr.h>
2323

2424
/// \class Types used throughout the test. Currently it is impossible to
2525
/// statically initialize this value, there is a PR to allow this
2626
/// diffblue/cbmc/pull/1213
2727
class tt
2828
{
2929
public:
30-
tt() {}
31-
typet char_type() const {return java_char_type();}
32-
typet length_type() const {return java_int_type();}
30+
tt()
31+
{
32+
}
33+
typet char_type() const
34+
{
35+
return java_char_type();
36+
}
37+
typet length_type() const
38+
{
39+
return java_int_type();
40+
}
3341
array_typet array_type() const
3442
{
3543
return array_typet(char_type(), infinity_exprt(length_type()));
@@ -60,7 +68,7 @@ constant_exprt from_integer(const mp_integer &i)
6068
/// \return corresponding `string_exprt`
6169
array_string_exprt make_string_exprt(const std::string &str)
6270
{
63-
const constant_exprt length=from_integer(str.length(), t.length_type());
71+
const constant_exprt length = from_integer(str.length(), t.length_type());
6472
array_exprt content({}, array_typet(t.char_type(), length));
6573

6674
for(const char c : str)
@@ -92,7 +100,7 @@ std::set<exprt> full_index_set(const array_string_exprt &s)
92100
{
93101
const mp_integer n = numeric_cast_v<mp_integer>(s.length());
94102
std::set<exprt> ret;
95-
for(mp_integer i=0; i<n; ++i)
103+
for(mp_integer i = 0; i < n; ++i)
96104
ret.insert(from_integer(i));
97105
return ret;
98106
}
@@ -115,7 +123,7 @@ std::set<std::pair<X, Y>> product(const std::set<X> xs, const std::set<Y> ys)
115123
exprt combine_lemmas(const std::vector<exprt> &lemmas, const namespacet &ns)
116124
{
117125
// Conjunction of new lemmas
118-
exprt conj=conjunction(lemmas);
126+
exprt conj = conjunction(lemmas);
119127
// Simplify
120128
simplify(conj, ns);
121129

@@ -137,7 +145,7 @@ std::string create_info(std::vector<exprt> &lemmas, const namespacet &ns)
137145
get_language_from_mode(ID_java)->from_expr(lemma, lemma_string, ns);
138146
new_lemmas += lemma_string + "\n\n";
139147
}
140-
return "Instantiated lemmas:\n"+new_lemmas;
148+
return "Instantiated lemmas:\n" + new_lemmas;
141149
}
142150

143151
/// Checks the satisfiability of the given expression.
@@ -148,16 +156,17 @@ decision_proceduret::resultt check_sat(const exprt &expr, const namespacet &ns)
148156
{
149157
satcheck_no_simplifiert sat_check;
150158
bv_refinementt::infot info;
151-
info.ns=&ns;
152-
info.prop=&sat_check;
159+
info.ns = &ns;
160+
info.prop = &sat_check;
153161
info.output_xml = false;
154162
bv_refinementt solver(info);
155163
solver << expr;
156164
return solver();
157165
}
158166

159167
// The [!mayfail] tag allows tests to fail while reporting the failure
160-
SCENARIO("instantiate_not_contains",
168+
SCENARIO(
169+
"instantiate_not_contains",
161170
"[!mayfail][core][solvers][refinement][string_constraint_instantiation]")
162171
{
163172
// For printing expression
@@ -261,10 +270,10 @@ SCENARIO("instantiate_not_contains",
261270
decision_proceduret::resultt result = check_sat(conj, empty_ns);
262271

263272
// Require SAT
264-
if(result==decision_proceduret::resultt::D_ERROR)
273+
if(result == decision_proceduret::resultt::D_ERROR)
265274
INFO("Got an error");
266275

267-
REQUIRE(result==decision_proceduret::resultt::D_SATISFIABLE);
276+
REQUIRE(result == decision_proceduret::resultt::D_SATISFIABLE);
268277
}
269278
}
270279
}
@@ -311,10 +320,10 @@ SCENARIO("instantiate_not_contains",
311320
decision_proceduret::resultt result = check_sat(conj, empty_ns);
312321

313322
// Require SAT
314-
if(result==decision_proceduret::resultt::D_ERROR)
323+
if(result == decision_proceduret::resultt::D_ERROR)
315324
INFO("Got an error");
316325

317-
REQUIRE(result==decision_proceduret::resultt::D_SATISFIABLE);
326+
REQUIRE(result == decision_proceduret::resultt::D_SATISFIABLE);
318327
}
319328
}
320329
}
@@ -362,10 +371,10 @@ SCENARIO("instantiate_not_contains",
362371
decision_proceduret::resultt result = check_sat(conj, empty_ns);
363372

364373
// Require UNSAT
365-
if(result==decision_proceduret::resultt::D_ERROR)
374+
if(result == decision_proceduret::resultt::D_ERROR)
366375
INFO("Got an error");
367376

368-
REQUIRE(result==decision_proceduret::resultt::D_UNSATISFIABLE);
377+
REQUIRE(result == decision_proceduret::resultt::D_UNSATISFIABLE);
369378
}
370379
}
371380
}
@@ -414,10 +423,10 @@ SCENARIO("instantiate_not_contains",
414423
decision_proceduret::resultt result = check_sat(conj, empty_ns);
415424

416425
// Require UNSAT
417-
if(result==decision_proceduret::resultt::D_ERROR)
426+
if(result == decision_proceduret::resultt::D_ERROR)
418427
INFO("Got an error");
419428

420-
REQUIRE(result==decision_proceduret::resultt::D_UNSATISFIABLE);
429+
REQUIRE(result == decision_proceduret::resultt::D_UNSATISFIABLE);
421430
}
422431
}
423432
}
@@ -465,10 +474,10 @@ SCENARIO("instantiate_not_contains",
465474
decision_proceduret::resultt result = check_sat(conj, empty_ns);
466475

467476
// Require UNSAT
468-
if(result==decision_proceduret::resultt::D_ERROR)
477+
if(result == decision_proceduret::resultt::D_ERROR)
469478
INFO("Got an error");
470479

471-
REQUIRE(result==decision_proceduret::resultt::D_UNSATISFIABLE);
480+
REQUIRE(result == decision_proceduret::resultt::D_UNSATISFIABLE);
472481
}
473482
}
474483
}
@@ -517,10 +526,10 @@ SCENARIO("instantiate_not_contains",
517526
decision_proceduret::resultt result = check_sat(conj, empty_ns);
518527

519528
// Require UNSAT
520-
if(result==decision_proceduret::resultt::D_ERROR)
529+
if(result == decision_proceduret::resultt::D_ERROR)
521530
INFO("Got an error");
522531

523-
REQUIRE(result==decision_proceduret::resultt::D_SATISFIABLE);
532+
REQUIRE(result == decision_proceduret::resultt::D_SATISFIABLE);
524533
}
525534
}
526535
}

‎jbmc/unit/solvers/strings/string_refinement/dependency_graph.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,11 +9,11 @@ Author: Diffblue Ltd.
99

1010
#include <testing-utils/catch.hpp>
1111

12-
#include <util/arith_tools.h>
13-
#include <util/std_types.h>
14-
#include <util/std_expr.h>
1512
#include <java_bytecode/java_types.h>
1613
#include <solvers/strings/string_refinement_util.h>
14+
#include <util/arith_tools.h>
15+
#include <util/std_expr.h>
16+
#include <util/std_types.h>
1717

1818
#ifdef DEBUG
1919
#include <iostream>

‎jbmc/unit/solvers/strings/string_refinement/string_symbol_resolution.cpp

Lines changed: 8 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -11,16 +11,17 @@ Author: Diffblue Ltd.
1111

1212
#include <solvers/strings/string_refinement.h>
1313

14+
#include <iostream>
15+
#include <java_bytecode/java_bytecode_language.h>
16+
#include <langapi/mode.h>
1417
#include <util/arith_tools.h>
1518
#include <util/c_types.h>
1619
#include <util/std_expr.h>
1720
#include <util/symbol_table.h>
18-
#include <langapi/mode.h>
19-
#include <java_bytecode/java_bytecode_language.h>
20-
#include <iostream>
2121

22-
SCENARIO("string_identifiers_resolution_from_equations",
23-
"[core][solvers][refinement][string_refinement]")
22+
SCENARIO(
23+
"string_identifiers_resolution_from_equations",
24+
"[core][solvers][refinement][string_refinement]")
2425
{
2526
// For printing expression
2627
register_language(new_java_bytecode_language);
@@ -51,8 +52,7 @@ SCENARIO("string_identifiers_resolution_from_equations",
5152
WHEN("There is no function call")
5253
{
5354
union_find_replacet symbol_resolve =
54-
string_identifiers_resolution_from_equations(
55-
equations, ns, stream);
55+
string_identifiers_resolution_from_equations(equations, ns, stream);
5656

5757
THEN("The symbol resolution structure is empty")
5858
{
@@ -70,8 +70,7 @@ SCENARIO("string_identifiers_resolution_from_equations",
7070
symbol_exprt bool_sym("bool_b", bool_typet());
7171
equations.emplace_back(bool_sym, fun);
7272
union_find_replacet symbol_resolve =
73-
string_identifiers_resolution_from_equations(
74-
equations, ns, stream);
73+
string_identifiers_resolution_from_equations(equations, ns, stream);
7574

7675
THEN("Equations that depend on it should be added")
7776
{

‎src/goto-checker/solver_factory.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,9 +28,9 @@ Author: Daniel Kroening, Peter Schrammel
2828
#include <solvers/prop/prop.h>
2929
#include <solvers/prop/prop_conv.h>
3030
#include <solvers/refinement/bv_refinement.h>
31-
#include <solvers/strings/string_refinement.h>
3231
#include <solvers/sat/dimacs_cnf.h>
3332
#include <solvers/sat/satcheck.h>
33+
#include <solvers/strings/string_refinement.h>
3434

3535
solver_factoryt::solver_factoryt(
3636
const optionst &_options,

‎src/solvers/strings/string_builtin_function.cpp

Lines changed: 18 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -247,13 +247,11 @@ string_constraintst string_set_char_builtin_functiont::constraints(
247247
{
248248
string_constraintst constraints;
249249
constraints.existential.push_back(length_constraint());
250-
constraints.existential.push_back(
251-
implies_exprt(
252-
and_exprt(
253-
binary_relation_exprt(
254-
from_integer(0, position.type()), ID_le, position),
255-
binary_relation_exprt(position, ID_lt, result.length())),
256-
equal_exprt(result[position], character)));
250+
constraints.existential.push_back(implies_exprt(
251+
and_exprt(
252+
binary_relation_exprt(from_integer(0, position.type()), ID_le, position),
253+
binary_relation_exprt(position, ID_lt, result.length())),
254+
equal_exprt(result[position], character)));
257255
constraints.universal.push_back([&] {
258256
const symbol_exprt q =
259257
generator.fresh_symbol("QA_char_set", position.type());
@@ -323,28 +321,25 @@ static exprt is_upper_case(const exprt &character)
323321
const exprt char_Z = from_integer('Z', character.type());
324322
exprt::operandst upper_case;
325323
// Characters between 'A' and 'Z' are upper-case
326-
upper_case.push_back(
327-
and_exprt(
328-
binary_relation_exprt(char_A, ID_le, character),
329-
binary_relation_exprt(character, ID_le, char_Z)));
324+
upper_case.push_back(and_exprt(
325+
binary_relation_exprt(char_A, ID_le, character),
326+
binary_relation_exprt(character, ID_le, char_Z)));
330327

331328
// Characters between 0xc0 (latin capital A with grave)
332329
// and 0xd6 (latin capital O with diaeresis) are upper-case
333-
upper_case.push_back(
334-
and_exprt(
335-
binary_relation_exprt(
336-
from_integer(0xc0, character.type()), ID_le, character),
337-
binary_relation_exprt(
338-
character, ID_le, from_integer(0xd6, character.type()))));
330+
upper_case.push_back(and_exprt(
331+
binary_relation_exprt(
332+
from_integer(0xc0, character.type()), ID_le, character),
333+
binary_relation_exprt(
334+
character, ID_le, from_integer(0xd6, character.type()))));
339335

340336
// Characters between 0xd8 (latin capital O with stroke)
341337
// and 0xde (latin capital thorn) are upper-case
342-
upper_case.push_back(
343-
and_exprt(
344-
binary_relation_exprt(
345-
from_integer(0xd8, character.type()), ID_le, character),
346-
binary_relation_exprt(
347-
character, ID_le, from_integer(0xde, character.type()))));
338+
upper_case.push_back(and_exprt(
339+
binary_relation_exprt(
340+
from_integer(0xd8, character.type()), ID_le, character),
341+
binary_relation_exprt(
342+
character, ID_le, from_integer(0xde, character.type()))));
348343
return disjunction(upper_case);
349344
}
350345

‎src/solvers/strings/string_builtin_function.h

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,10 +4,10 @@
44
#ifndef CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H
55
#define CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H
66

7-
#include <vector>
7+
#include "string_constraint_generator.h"
88
#include <util/optional.h>
99
#include <util/string_expr.h>
10-
#include "string_constraint_generator.h"
10+
#include <vector>
1111

1212
class array_poolt;
1313
struct string_constraintst;

‎src/solvers/strings/string_constraint.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -161,6 +161,6 @@ struct hash<string_not_contains_constraintt>
161161
irep_hash()(constraint.s1);
162162
}
163163
};
164-
}
164+
} // namespace std
165165

166166
#endif

0 commit comments

Comments
 (0)