Skip to content

Commit c688efd

Browse files
authored
Merge pull request #6880 from diffblue/fix_decl_assignment_loc
add missing source_location for assignments generated for initializers
2 parents 679ab3f + bcca9da commit c688efd

File tree

4 files changed

+5
-4
lines changed

4 files changed

+5
-4
lines changed

regression/cbmc-cover/location-multiline-statement/multi-file.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ multi-file.c
33
--cover location
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.coverage.2\] file multi-file.c line 13 function main block 2 \(lines [\w\- /\.\\:]*dereference.h:main:2; multi-file.c:main:10,13,14,16\): SATISFIED
6+
^\[main.coverage.2\] file multi-file.c line 10 function main block 2 \(lines [\w\- /\.\\:]*dereference.h:main:2; multi-file.c:main:10,13,14,16\): SATISFIED
77
--
88
^warning: ignoring
99
--

regression/cbmc-cover/location-multiline-statement/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ example.c
33
--cover location
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.coverage.2\] file example.c line 13 function main block 2 \(lines example.c:main:10,13,14\): SATISFIED$
6+
^\[main.coverage.2\] file example.c line 10 function main block 2 \(lines example.c:main:10,13,14\): SATISFIED$
77
--
88
^warning: ignoring
99
--

regression/cbmc-cover/location15/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ main.c
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[main.coverage.1\] file main.c line 10 function main block 1.*: SATISFIED$
7-
^\[main.coverage.2\] file main.c line 11 function main block 2.*: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 10 function main block 2.*: SATISFIED$
88
^\[main.coverage.3\] file main.c line 13 function main block 3.*: FAILED$
99
^\[main.coverage.4\] file main.c line 16 function main block 4.*: SATISFIED$
1010
^\[foo.coverage.1\] file main.c line 5 function foo block 1.*: FAILED$

src/goto-programs/goto_convert.cpp

+2-1
Original file line numberDiff line numberDiff line change
@@ -637,12 +637,13 @@ void goto_convertt::convert_frontend_decl(
637637
// Decl must be visible before initializer.
638638
copy(tmp, DECL, dest);
639639

640+
auto initializer_location = initializer.find_source_location();
640641
clean_expr(initializer, dest, mode);
641642

642643
if(initializer.is_not_nil())
643644
{
644645
code_assignt assign(code.op0(), initializer);
645-
assign.add_source_location() = initializer.find_source_location();
646+
assign.add_source_location() = initializer_location;
646647

647648
convert_assign(assign, dest, mode);
648649
}

0 commit comments

Comments
 (0)