Skip to content

Commit e240abb

Browse files
author
svorenova
committed
Update method source location info
The line number is not the line number of the first instruction because that can be unassigned. Instead, set it to the line number of the first instruction that does have a line number assigned. Set location function to be the name of the method itself.
1 parent c24ff8a commit e240abb

File tree

1 file changed

+16
-3
lines changed

1 file changed

+16
-3
lines changed

jbmc/src/java_bytecode/java_bytecode_parser.cpp

Lines changed: 16 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1256,10 +1256,23 @@ void java_bytecode_parsert::rmethod_attribute(methodt &method)
12561256
id2string(method.name)+":"+method.descriptor);
12571257
}
12581258

1259-
// line number of method
1259+
// line number of method (the first line number available)
12601260
if(!method.instructions.empty())
1261-
method.source_location.set_line(
1262-
method.instructions.begin()->source_location.get_line());
1261+
{
1262+
const auto it = std::find_if(
1263+
method.instructions.begin(),
1264+
method.instructions.end(),
1265+
[&](const instructiont &instruction) {
1266+
return !instruction.source_location.get_line().empty();
1267+
});
1268+
if(it != method.instructions.end())
1269+
method.source_location.set_line(it->source_location.get_line());
1270+
}
1271+
1272+
// method name
1273+
method.source_location.set_function(
1274+
"java::" + id2string(parse_tree.parsed_class.name) + "." +
1275+
id2string(method.name) + ":" + method.descriptor);
12631276
}
12641277
else if(attribute_name=="Signature")
12651278
{

0 commit comments

Comments
 (0)