Skip to content

Commit 357bbe4

Browse files
thomasspriggsthomasspriggs
committed
Fix formatting in assert replacements.
1 parent f8c2b09 commit 357bbe4

File tree

1 file changed

+39
-39
lines changed

1 file changed

+39
-39
lines changed

‎src/java_bytecode/java_bytecode_convert_method.cpp

Lines changed: 39 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -1510,7 +1510,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
15101510
}
15111511
else if(statement==patternt("?aload"))
15121512
{
1513-
PRECONDITION(op.size()==2 && results.size()==1);
1513+
PRECONDITION(op.size() == 2 && results.size() == 1);
15141514

15151515
char type_char=statement[0];
15161516

@@ -1541,7 +1541,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
15411541
else if(statement=="ldc" || statement=="ldc_w" ||
15421542
statement=="ldc2" || statement=="ldc2_w")
15431543
{
1544-
PRECONDITION(op.empty() && results.size()==1);
1544+
PRECONDITION(op.empty() && results.size() == 1);
15451545

15461546
INVARIANT(
15471547
arg0.id() != ID_java_string_literal && arg0.id() != ID_type,
@@ -1562,7 +1562,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
15621562
else if(statement=="jsr" || statement=="jsr_w")
15631563
{
15641564
// As 'goto', except we must also push the subroutine return address:
1565-
PRECONDITION(op.empty() && results.size()==1);
1565+
PRECONDITION(op.empty() && results.size() == 1);
15661566
mp_integer number;
15671567
bool ret=to_integer(to_constant_expr(arg0), number);
15681568
INVARIANT(!ret, "jsr argument should be an integer");
@@ -1659,7 +1659,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
16591659
}
16601660
else if(statement==patternt("if_?cmp??"))
16611661
{
1662-
PRECONDITION(op.size()==2 && results.empty());
1662+
PRECONDITION(op.size() == 2 && results.empty());
16631663
mp_integer number;
16641664
bool ret=to_integer(to_constant_expr(arg0), number);
16651665
INVARIANT(!ret, "if_?cmp?? argument should be an integer");
@@ -1697,7 +1697,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
16971697

16981698
INVARIANT(!id.empty(), "unexpected bytecode-if");
16991699

1700-
PRECONDITION(op.size()==1 && results.empty());
1700+
PRECONDITION(op.size() == 1 && results.empty());
17011701
mp_integer number;
17021702
bool ret=to_integer(to_constant_expr(arg0), number);
17031703
INVARIANT(!ret, "if?? argument should be an integer");
@@ -1718,7 +1718,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
17181718
}
17191719
else if(statement==patternt("ifnonnull"))
17201720
{
1721-
PRECONDITION(op.size()==1 && results.empty());
1721+
PRECONDITION(op.size() == 1 && results.empty());
17221722
mp_integer number;
17231723
bool ret=to_integer(to_constant_expr(arg0), number);
17241724
INVARIANT(!ret, "ifnonnull argument should be an integer");
@@ -1735,7 +1735,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
17351735
}
17361736
else if(statement==patternt("ifnull"))
17371737
{
1738-
PRECONDITION(op.size()==1 && results.empty());
1738+
PRECONDITION(op.size() == 1 && results.empty());
17391739
mp_integer number;
17401740
bool ret=to_integer(to_constant_expr(arg0), number);
17411741
INVARIANT(!ret, "ifnull argument should be an integer");
@@ -1777,32 +1777,32 @@ codet java_bytecode_convert_methodt::convert_instructions(
17771777
}
17781778
else if(statement==patternt("?xor"))
17791779
{
1780-
PRECONDITION(op.size()==2 && results.size()==1);
1780+
PRECONDITION(op.size() == 2 && results.size() == 1);
17811781
results[0]=bitxor_exprt(op[0], op[1]);
17821782
}
17831783
else if(statement==patternt("?or"))
17841784
{
1785-
PRECONDITION(op.size()==2 && results.size()==1);
1785+
PRECONDITION(op.size() == 2 && results.size() == 1);
17861786
results[0]=bitor_exprt(op[0], op[1]);
17871787
}
17881788
else if(statement==patternt("?and"))
17891789
{
1790-
PRECONDITION(op.size()==2 && results.size()==1);
1790+
PRECONDITION(op.size() == 2 && results.size() == 1);
17911791
results[0]=bitand_exprt(op[0], op[1]);
17921792
}
17931793
else if(statement==patternt("?shl"))
17941794
{
1795-
PRECONDITION(op.size()==2 && results.size()==1);
1795+
PRECONDITION(op.size() == 2 && results.size() == 1);
17961796
results[0]=shl_exprt(op[0], op[1]);
17971797
}
17981798
else if(statement==patternt("?shr"))
17991799
{
1800-
PRECONDITION(op.size()==2 && results.size()==1);
1800+
PRECONDITION(op.size() == 2 && results.size() == 1);
18011801
results[0]=ashr_exprt(op[0], op[1]);
18021802
}
18031803
else if(statement==patternt("?ushr"))
18041804
{
1805-
PRECONDITION(op.size()==2 && results.size()==1);
1805+
PRECONDITION(op.size() == 2 && results.size() == 1);
18061806
const typet type=java_type_from_char(statement[0]);
18071807

18081808
const std::size_t width=type.get_size_t(ID_width);
@@ -1821,40 +1821,40 @@ codet java_bytecode_convert_methodt::convert_instructions(
18211821
}
18221822
else if(statement==patternt("?add"))
18231823
{
1824-
PRECONDITION(op.size()==2 && results.size()==1);
1824+
PRECONDITION(op.size() == 2 && results.size() == 1);
18251825
results[0]=plus_exprt(op[0], op[1]);
18261826
}
18271827
else if(statement==patternt("?sub"))
18281828
{
1829-
PRECONDITION(op.size()==2 && results.size()==1);
1829+
PRECONDITION(op.size() == 2 && results.size() == 1);
18301830
results[0]=minus_exprt(op[0], op[1]);
18311831
}
18321832
else if(statement==patternt("?div"))
18331833
{
1834-
PRECONDITION(op.size()==2 && results.size()==1);
1834+
PRECONDITION(op.size() == 2 && results.size() == 1);
18351835
results[0]=div_exprt(op[0], op[1]);
18361836
}
18371837
else if(statement==patternt("?mul"))
18381838
{
1839-
PRECONDITION(op.size()==2 && results.size()==1);
1839+
PRECONDITION(op.size() == 2 && results.size() == 1);
18401840
results[0]=mult_exprt(op[0], op[1]);
18411841
}
18421842
else if(statement==patternt("?neg"))
18431843
{
1844-
PRECONDITION(op.size()==1 && results.size()==1);
1844+
PRECONDITION(op.size() == 1 && results.size() == 1);
18451845
results[0]=unary_minus_exprt(op[0], op[0].type());
18461846
}
18471847
else if(statement==patternt("?rem"))
18481848
{
1849-
PRECONDITION(op.size()==2 && results.size()==1);
1849+
PRECONDITION(op.size() == 2 && results.size() == 1);
18501850
if(statement=="frem" || statement=="drem")
18511851
results[0]=rem_exprt(op[0], op[1]);
18521852
else
18531853
results[0]=mod_exprt(op[0], op[1]);
18541854
}
18551855
else if(statement==patternt("?cmp"))
18561856
{
1857-
PRECONDITION(op.size()==2 && results.size()==1);
1857+
PRECONDITION(op.size() == 2 && results.size() == 1);
18581858

18591859
// The integer result on the stack is:
18601860
// 0 if op[0] equals op[1]
@@ -1878,7 +1878,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
18781878
}
18791879
else if(statement==patternt("?cmp?"))
18801880
{
1881-
PRECONDITION(op.size()==2 && results.size()==1);
1881+
PRECONDITION(op.size() == 2 && results.size() == 1);
18821882
const int nan_value(statement[4]=='l' ? -1 : 1);
18831883
const typet result_type(java_int_type());
18841884
const exprt nan_result(from_integer(nan_value, result_type));
@@ -1906,24 +1906,24 @@ codet java_bytecode_convert_methodt::convert_instructions(
19061906
}
19071907
else if(statement==patternt("?cmpl"))
19081908
{
1909-
PRECONDITION(op.size()==2 && results.size()==1);
1909+
PRECONDITION(op.size() == 2 && results.size() == 1);
19101910
results[0]=binary_relation_exprt(op[0], ID_lt, op[1]);
19111911
}
19121912
else if(statement=="dup")
19131913
{
1914-
PRECONDITION(op.size()==1 && results.size()==2);
1914+
PRECONDITION(op.size() == 1 && results.size() == 2);
19151915
results[0]=results[1]=op[0];
19161916
}
19171917
else if(statement=="dup_x1")
19181918
{
1919-
PRECONDITION(op.size()==2 && results.size()==3);
1919+
PRECONDITION(op.size() == 2 && results.size() == 3);
19201920
results[0]=op[1];
19211921
results[1]=op[0];
19221922
results[2]=op[1];
19231923
}
19241924
else if(statement=="dup_x2")
19251925
{
1926-
PRECONDITION(op.size()==3 && results.size()==4);
1926+
PRECONDITION(op.size() == 3 && results.size() == 4);
19271927
results[0]=op[2];
19281928
results[1]=op[0];
19291929
results[2]=op[1];
@@ -1978,20 +1978,20 @@ codet java_bytecode_convert_methodt::convert_instructions(
19781978
}
19791979
else if(statement=="dconst")
19801980
{
1981-
PRECONDITION(op.empty() && results.size()==1);
1981+
PRECONDITION(op.empty() && results.size() == 1);
19821982
}
19831983
else if(statement=="fconst")
19841984
{
1985-
PRECONDITION(op.empty() && results.size()==1);
1985+
PRECONDITION(op.empty() && results.size() == 1);
19861986
}
19871987
else if(statement=="getfield")
19881988
{
1989-
PRECONDITION(op.size()==1 && results.size()==1);
1989+
PRECONDITION(op.size() == 1 && results.size() == 1);
19901990
results[0]=java_bytecode_promotion(to_member(op[0], arg0));
19911991
}
19921992
else if(statement=="getstatic")
19931993
{
1994-
PRECONDITION(op.empty() && results.size()==1);
1994+
PRECONDITION(op.empty() && results.size() == 1);
19951995
symbol_exprt symbol_expr(arg0.type());
19961996
const auto &field_name=arg0.get_string(ID_component_name);
19971997
const bool is_assertions_disabled_field=
@@ -2041,7 +2041,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
20412041
}
20422042
else if(statement=="putfield")
20432043
{
2044-
PRECONDITION(op.size()==2 && results.empty());
2044+
PRECONDITION(op.size() == 2 && results.empty());
20452045
code_blockt block;
20462046
save_stack_entries(
20472047
"stack_field",
@@ -2054,7 +2054,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
20542054
}
20552055
else if(statement=="putstatic")
20562056
{
2057-
PRECONDITION(op.size()==1 && results.empty());
2057+
PRECONDITION(op.size() == 1 && results.empty());
20582058
symbol_exprt symbol_expr(arg0.type());
20592059
const auto &field_name=arg0.get_string(ID_component_name);
20602060
symbol_expr.set_identifier(
@@ -2091,7 +2091,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
20912091
}
20922092
else if(statement==patternt("?2?")) // i2c etc.
20932093
{
2094-
PRECONDITION(op.size()==1 && results.size()==1);
2094+
PRECONDITION(op.size() == 1 && results.size() == 1);
20952095
typet type=java_type_from_char(statement[2]);
20962096
results[0]=op[0];
20972097
if(results[0].type()!=type)
@@ -2100,7 +2100,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
21002100
else if(statement=="new")
21012101
{
21022102
// use temporary since the stack symbol might get duplicated
2103-
PRECONDITION(op.empty() && results.size()==1);
2103+
PRECONDITION(op.empty() && results.size() == 1);
21042104
const reference_typet ref_type=java_reference_type(arg0.type());
21052105
exprt java_new_expr=side_effect_exprt(ID_java_new, ref_type);
21062106

@@ -2125,7 +2125,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
21252125
statement=="anewarray")
21262126
{
21272127
// the op is the array size
2128-
PRECONDITION(op.size()==1 && results.size()==1);
2128+
PRECONDITION(op.size() == 1 && results.size() == 1);
21292129

21302130
char element_type;
21312131

@@ -2217,7 +2217,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
22172217
}
22182218
else if(statement=="arraylength")
22192219
{
2220-
PRECONDITION(op.size()==1 && results.size()==1);
2220+
PRECONDITION(op.size() == 1 && results.size() == 1);
22212221

22222222
exprt pointer=
22232223
typecast_exprt(op[0], java_array_type(statement[0]));
@@ -2233,7 +2233,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
22332233
else if(statement=="tableswitch" ||
22342234
statement=="lookupswitch")
22352235
{
2236-
PRECONDITION(op.size()==1 && results.empty());
2236+
PRECONDITION(op.size() == 1 && results.empty());
22372237

22382238
// we turn into switch-case
22392239
code_switcht code_switch;
@@ -2294,7 +2294,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
22942294
}
22952295
else if(statement=="instanceof")
22962296
{
2297-
PRECONDITION(op.size()==1 && results.size()==1);
2297+
PRECONDITION(op.size() == 1 && results.size() == 1);
22982298

22992299
results[0]=
23002300
binary_predicate_exprt(op[0], ID_java_instanceof, arg0);
@@ -2329,7 +2329,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
23292329
}
23302330
else if(statement=="swap")
23312331
{
2332-
PRECONDITION(op.size()==2 && results.size()==2);
2332+
PRECONDITION(op.size() == 2 && results.size() == 2);
23332333
results[1]=op[0];
23342334
results[0]=op[1];
23352335
}
@@ -2465,7 +2465,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
24652465
for(const unsigned address : a_it->second.successors)
24662466
{
24672467
address_mapt::iterator a_it2=address_map.find(address);
2468-
CHECK_RETURN(a_it2!=address_map.end());
2468+
CHECK_RETURN(a_it2 != address_map.end());
24692469

24702470
// clear the stack if this is an exception handler
24712471
for(const auto &exception_row : method.exception_table)

0 commit comments

Comments
 (0)