Skip to content

Commit 52a669f

Browse files
thomasspriggsthomasspriggs
committed
Remove java_bytecode::swap and return using optionalt instead.
This removes the `swap` method as suggested in #2011 Avoiding having a `swap`method, makes updates less error prone.
1 parent e5e0897 commit 52a669f

File tree

6 files changed

+37
-76
lines changed

6 files changed

+37
-76
lines changed

‎jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp‎

Lines changed: 0 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -18,28 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com
1818

1919
#include "expr2java.h"
2020

21-
void java_bytecode_parse_treet::classt::swap(
22-
classt &other)
23-
{
24-
other.name.swap(name);
25-
other.extends.swap(extends);
26-
std::swap(other.is_enum, is_enum);
27-
std::swap(other.enum_elements, enum_elements);
28-
std::swap(other.is_abstract, is_abstract);
29-
std::swap(other.is_public, is_public);
30-
std::swap(other.is_protected, is_protected);
31-
std::swap(other.is_private, is_private);
32-
std::swap(other.is_final, is_final);
33-
std::swap(other.signature, signature);
34-
other.implements.swap(implements);
35-
other.fields.swap(fields);
36-
other.methods.swap(methods);
37-
other.annotations.swap(annotations);
38-
std::swap(
39-
other.attribute_bootstrapmethods_read, attribute_bootstrapmethods_read);
40-
std::swap(other.lambda_method_handle_map, lambda_method_handle_map);
41-
}
42-
4321
void java_bytecode_parse_treet::output(std::ostream &out) const
4422
{
4523
parsed_class.output(out);

‎jbmc/src/java_bytecode/java_bytecode_parse_tree.h‎

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -261,17 +261,10 @@ class java_bytecode_parse_treet
261261

262262
void output(std::ostream &out) const;
263263

264-
void swap(classt &other);
265264
};
266265

267266
classt parsed_class;
268267

269-
void swap(java_bytecode_parse_treet &other)
270-
{
271-
other.parsed_class.swap(parsed_class);
272-
other.class_refs.swap(class_refs);
273-
std::swap(loading_successful, other.loading_successful);
274-
}
275268

276269
void output(std::ostream &out) const;
277270

‎jbmc/src/java_bytecode/java_bytecode_parser.cpp‎

Lines changed: 11 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1688,26 +1688,25 @@ void java_bytecode_parsert::rmethod(classt &parsed_class)
16881688
rmethod_attribute(method);
16891689
}
16901690

1691-
bool java_bytecode_parse(
1692-
std::istream &istream,
1693-
java_bytecode_parse_treet &parse_tree,
1694-
message_handlert &message_handler)
1691+
optionalt<class java_bytecode_parse_treet>
1692+
java_bytecode_parse(std::istream &istream, message_handlert &message_handler)
16951693
{
16961694
java_bytecode_parsert java_bytecode_parser;
16971695
java_bytecode_parser.in=&istream;
16981696
java_bytecode_parser.set_message_handler(message_handler);
16991697

17001698
bool parser_result=java_bytecode_parser.parse();
17011699

1702-
parse_tree.swap(java_bytecode_parser.parse_tree);
1700+
if(parser_result)
1701+
{
1702+
return {};
1703+
}
17031704

1704-
return parser_result;
1705+
return java_bytecode_parser.parse_tree;
17051706
}
17061707

1707-
bool java_bytecode_parse(
1708-
const std::string &file,
1709-
java_bytecode_parse_treet &parse_tree,
1710-
message_handlert &message_handler)
1708+
optionalt<class java_bytecode_parse_treet>
1709+
java_bytecode_parse(const std::string &file, message_handlert &message_handler)
17111710
{
17121711
std::ifstream in(file, std::ios::binary);
17131712

@@ -1716,10 +1715,10 @@ bool java_bytecode_parse(
17161715
messaget message(message_handler);
17171716
message.error() << "failed to open input file `"
17181717
<< file << '\'' << messaget::eom;
1719-
return true;
1718+
return {};
17201719
}
17211720

1722-
return java_bytecode_parse(in, parse_tree, message_handler);
1721+
return java_bytecode_parse(in, message_handler);
17231722
}
17241723

17251724
/// Parses the local variable type table of a method. The LVTT holds generic

‎jbmc/src/java_bytecode/java_bytecode_parser.h‎

Lines changed: 5 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -12,15 +12,12 @@ Author: Daniel Kroening, kroening@kroening.com
1212

1313
#include <iosfwd>
1414
#include <string>
15+
#include <util/optional.h>
1516

16-
bool java_bytecode_parse(
17-
const std::string &file,
18-
class java_bytecode_parse_treet &,
19-
class message_handlert &);
17+
optionalt<class java_bytecode_parse_treet>
18+
java_bytecode_parse(const std::string &file, class message_handlert &);
2019

21-
bool java_bytecode_parse(
22-
std::istream &,
23-
class java_bytecode_parse_treet &,
24-
class message_handlert &);
20+
optionalt<class java_bytecode_parse_treet>
21+
java_bytecode_parse(std::istream &, class message_handlert &);
2522

2623
#endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSER_H

‎jbmc/src/java_bytecode/java_class_loader.cpp‎

Lines changed: 5 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -97,11 +97,8 @@ optionalt<java_bytecode_parse_treet> java_class_loadert::get_class_from_jar(
9797
if(!data.has_value())
9898
return {};
9999

100-
java_bytecode_parse_treet parse_tree;
101100
std::istringstream istream(*data);
102-
if(java_bytecode_parse(istream, parse_tree, get_message_handler()))
103-
return {};
104-
return parse_tree;
101+
return java_bytecode_parse(istream, get_message_handler());
105102
}
106103

107104
static bool is_overlay_class(const java_bytecode_parse_treet::classt &c)
@@ -192,9 +189,10 @@ java_class_loadert::get_parse_tree(
192189
debug()
193190
<< "Getting class `" << class_name << "' from file " << full_path
194191
<< eom;
195-
java_bytecode_parse_treet parse_tree;
196-
if(!java_bytecode_parse(full_path, parse_tree, get_message_handler()))
197-
parse_trees.push_back(std::move(parse_tree));
192+
optionalt<java_bytecode_parse_treet> parse_tree =
193+
java_bytecode_parse(full_path, get_message_handler());
194+
if(parse_tree)
195+
parse_trees.push_back(std::move(*parse_tree));
198196
}
199197
}
200198
}

‎jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp‎

Lines changed: 16 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -33,17 +33,16 @@ SCENARIO(
3333
GIVEN(
3434
"A class with a static lambda variables from " + compiler + " compiler.")
3535
{
36-
java_bytecode_parse_treet parse_tree;
37-
java_bytecode_parse(
36+
optionalt<java_bytecode_parse_treet> parse_tree = java_bytecode_parse(
3837
"./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/" +
3938
compiler + "_classes/StaticLambdas.class",
40-
parse_tree,
4139
message_handler);
4240
WHEN("Parsing that class")
4341
{
44-
REQUIRE(parse_tree.loading_successful);
42+
REQUIRE(parse_tree);
43+
REQUIRE(parse_tree->loading_successful);
4544
const java_bytecode_parse_treet::classt parsed_class =
46-
parse_tree.parsed_class;
45+
parse_tree->parsed_class;
4746
REQUIRE(parsed_class.attribute_bootstrapmethods_read);
4847
REQUIRE(parsed_class.lambda_method_handle_map.size() == 12);
4948

@@ -345,17 +344,16 @@ SCENARIO(
345344
null_message_handlert message_handler;
346345
GIVEN("A method with local lambdas from " + compiler + " compiler.")
347346
{
348-
java_bytecode_parse_treet parse_tree;
349-
java_bytecode_parse(
347+
optionalt<java_bytecode_parse_treet> parse_tree = java_bytecode_parse(
350348
"./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/" +
351349
compiler + "_classes/LocalLambdas.class",
352-
parse_tree,
353350
message_handler);
354351
WHEN("Parsing that class")
355352
{
356-
REQUIRE(parse_tree.loading_successful);
353+
REQUIRE(parse_tree);
354+
REQUIRE(parse_tree->loading_successful);
357355
const java_bytecode_parse_treet::classt parsed_class =
358-
parse_tree.parsed_class;
356+
parse_tree->parsed_class;
359357
REQUIRE(parsed_class.attribute_bootstrapmethods_read);
360358
REQUIRE(parsed_class.lambda_method_handle_map.size() == 12);
361359

@@ -655,17 +653,16 @@ SCENARIO(
655653
"A class that has lambdas as member variables from " + compiler +
656654
" compiler.")
657655
{
658-
java_bytecode_parse_treet parse_tree;
659-
java_bytecode_parse(
656+
optionalt<java_bytecode_parse_treet> parse_tree = java_bytecode_parse(
660657
"./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/" +
661658
compiler + "_classes/MemberLambdas.class",
662-
parse_tree,
663659
message_handler);
664660
WHEN("Parsing that class")
665661
{
666-
REQUIRE(parse_tree.loading_successful);
662+
REQUIRE(parse_tree);
663+
REQUIRE(parse_tree->loading_successful);
667664
const java_bytecode_parse_treet::classt parsed_class =
668-
parse_tree.parsed_class;
665+
parse_tree->parsed_class;
669666
REQUIRE(parsed_class.attribute_bootstrapmethods_read);
670667
REQUIRE(parsed_class.lambda_method_handle_map.size() == 12);
671668

@@ -991,17 +988,16 @@ SCENARIO(
991988
"variables from " +
992989
compiler + " compiler.")
993990
{
994-
java_bytecode_parse_treet parse_tree;
995-
java_bytecode_parse(
991+
optionalt<java_bytecode_parse_treet> parse_tree = java_bytecode_parse(
996992
"./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/" +
997993
compiler + "_classes/OuterMemberLambdas$Inner.class",
998-
parse_tree,
999994
message_handler);
1000995
WHEN("Parsing that class")
1001996
{
1002-
REQUIRE(parse_tree.loading_successful);
997+
REQUIRE(parse_tree);
998+
REQUIRE(parse_tree->loading_successful);
1003999
const java_bytecode_parse_treet::classt parsed_class =
1004-
parse_tree.parsed_class;
1000+
parse_tree->parsed_class;
10051001
REQUIRE(parsed_class.attribute_bootstrapmethods_read);
10061002
REQUIRE(parsed_class.lambda_method_handle_map.size() == 3);
10071003

0 commit comments

Comments
 (0)