Skip to content

Commit 0e5b254

Browse files
committed
Java frontend: Set source locations on instructions in code_blocks
This could lead to coverage goals not being assigned when the only instructions in a function were putstatic or other Java instructions that compile to a composite block.
1 parent 71ace43 commit 0e5b254

File tree

6 files changed

+49
-1
lines changed

6 files changed

+49
-1
lines changed
Binary file not shown.
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
test.class
3+
--show-goto-functions
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
test\.java line 5 function java::test.main:\(\)V bytecode_index 1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
public class test {
2+
3+
public static int x;
4+
public static void main() {
5+
x = 1;
6+
}
7+
static {
8+
x = 0;
9+
}
10+
11+
}

src/java_bytecode/java_bytecode_convert_method.cpp

+19-1
Original file line numberDiff line numberDiff line change
@@ -982,6 +982,24 @@ static unsigned get_bytecode_type_width(const typet &ty)
982982
return ty.get_unsigned_int(ID_width);
983983
}
984984

985+
/// Merge code's source location with source_location, and recursively
986+
/// do the same to operand code. Typically this is used for a code_blockt
987+
/// as is generated for some Java operations such as "putstatic", but will
988+
/// also work if they generate conditionals, loops, etc.
989+
/// Merge means that any fields already set in code.add_source_location()
990+
/// remain so; any new ones from source_location are added.
991+
static void merge_source_location_rec(
992+
codet &code,
993+
const source_locationt &source_location)
994+
{
995+
code.add_source_location().merge(source_location);
996+
for(exprt &op : code.operands())
997+
{
998+
if(op.id()==ID_code)
999+
merge_source_location_rec(to_code(op), source_location);
1000+
}
1001+
}
1002+
9851003
codet java_bytecode_convert_methodt::convert_instructions(
9861004
const methodt &method,
9871005
const code_typet &method_type,
@@ -2376,7 +2394,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
23762394
}
23772395

23782396
if(!i_it->source_location.get_line().empty())
2379-
c.add_source_location()=i_it->source_location;
2397+
merge_source_location_rec(c, i_it->source_location);
23802398

23812399
push(results);
23822400

src/util/source_location.cpp

+9
Original file line numberDiff line numberDiff line change
@@ -62,6 +62,15 @@ std::string source_locationt::as_string(bool print_cwd) const
6262
return dest;
6363
}
6464

65+
void source_locationt::merge(const source_locationt &from)
66+
{
67+
forall_named_irep(it, from.get_named_sub())
68+
{
69+
if(get(it->first).empty())
70+
set(it->first, it->second);
71+
}
72+
}
73+
6574
std::ostream &operator << (
6675
std::ostream &out,
6776
const source_locationt &source_location)

src/util/source_location.h

+4
Original file line numberDiff line numberDiff line change
@@ -162,6 +162,10 @@ class source_locationt:public irept
162162
return is_built_in(id2string(get_file()));
163163
}
164164

165+
/// Set all unset source-location fields in this object to their values in
166+
/// 'from'. Leave set fields in this object alone.
167+
void merge(const source_locationt &from);
168+
165169
static const source_locationt &nil()
166170
{
167171
return static_cast<const source_locationt &>(get_nil_irep());

0 commit comments

Comments
 (0)