diff --git a/regression/cbmc-cover/location-multiline-statement/multi-file.desc b/regression/cbmc-cover/location-multiline-statement/multi-file.desc index a2959f14d76..44062ca1d90 100644 --- a/regression/cbmc-cover/location-multiline-statement/multi-file.desc +++ b/regression/cbmc-cover/location-multiline-statement/multi-file.desc @@ -3,7 +3,7 @@ multi-file.c --cover location ^EXIT=0$ ^SIGNAL=0$ -^\[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 +^\[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 -- ^warning: ignoring -- diff --git a/regression/cbmc-cover/location-multiline-statement/test.desc b/regression/cbmc-cover/location-multiline-statement/test.desc index 4a04211a303..e4583ebd325 100644 --- a/regression/cbmc-cover/location-multiline-statement/test.desc +++ b/regression/cbmc-cover/location-multiline-statement/test.desc @@ -3,7 +3,7 @@ example.c --cover location ^EXIT=0$ ^SIGNAL=0$ -^\[main.coverage.2\] file example.c line 13 function main block 2 \(lines example.c:main:10,13,14\): SATISFIED$ +^\[main.coverage.2\] file example.c line 10 function main block 2 \(lines example.c:main:10,13,14\): SATISFIED$ -- ^warning: ignoring -- diff --git a/regression/cbmc-cover/location15/test.desc b/regression/cbmc-cover/location15/test.desc index 2124e50ad44..d0ad52e5d80 100644 --- a/regression/cbmc-cover/location15/test.desc +++ b/regression/cbmc-cover/location15/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^\[main.coverage.1\] file main.c line 10 function main block 1.*: SATISFIED$ -^\[main.coverage.2\] file main.c line 11 function main block 2.*: SATISFIED$ +^\[main.coverage.2\] file main.c line 10 function main block 2.*: SATISFIED$ ^\[main.coverage.3\] file main.c line 13 function main block 3.*: FAILED$ ^\[main.coverage.4\] file main.c line 16 function main block 4.*: SATISFIED$ ^\[foo.coverage.1\] file main.c line 5 function foo block 1.*: FAILED$ diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 8fbd3b63edb..f2ffb1df759 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -637,12 +637,13 @@ void goto_convertt::convert_frontend_decl( // Decl must be visible before initializer. copy(tmp, DECL, dest); + auto initializer_location = initializer.find_source_location(); clean_expr(initializer, dest, mode); if(initializer.is_not_nil()) { code_assignt assign(code.op0(), initializer); - assign.add_source_location() = initializer.find_source_location(); + assign.add_source_location() = initializer_location; convert_assign(assign, dest, mode); }