replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Move and reuse source_location.function 

If the assignment to the method.source_location.function is done first,
we can reuse it when assigning instruction.source_location.function
This commit is contained in:
svorenova 2019-07-12 11:42:42 +01:00
parent 07587bceb4
commit 85a1e8b3bc
1 changed files with 6 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
jbmc/src/java_bytecode/java_bytecode_parser.cpp
View File

@ -1238,6 +1238,11 @@ void java_bytecode_parsert::rmethod_attribute(methodt &method)
for(std::size_t j=0; j<attributes_count; j++)
rcode_attribute(method);
// method name
method.source_location.set_function(
"java::" + id2string(parse_tree.parsed_class.name) + "." +
id2string(method.name) + ":" + method.descriptor);
irep_idt line_number;
// add missing line numbers
@ -1250,10 +1255,7 @@ void java_bytecode_parsert::rmethod_attribute(methodt &method)
line_number=it->source_location.get_line();
else if(!line_number.empty())
it->source_location.set_line(line_number);
it->source_location
.set_function(
"java::"+id2string(parse_tree.parsed_class.name)+"."+
id2string(method.name)+":"+method.descriptor);
it->source_location.set_function(method.source_location.get_function());
}
// line number of method (the first line number available)
@ -1265,11 +1267,6 @@ void java_bytecode_parsert::rmethod_attribute(methodt &method)
});
if(it != method.instructions.end())
method.source_location.set_line(it->source_location.get_line());
// method name
method.source_location.set_function(
"java::" + id2string(parse_tree.parsed_class.name) + "." +
id2string(method.name) + ":" + method.descriptor);
}
else if(attribute_name=="Signature")
{