Skip to content

Commit 030563e

Browse files
committed
string_constantt::to_array_expr must maintain the source location
The C front-end uses this method to create arrays from string literals. The resulting expression must have a source location to ensure the resulting GOTO instruction knows which source location to use. Fixes: #6994
1 parent 21ff086 commit 030563e

File tree

3 files changed

+15
-3
lines changed

3 files changed

+15
-3
lines changed

regression/cbmc/String_Literal1/main.c

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -52,4 +52,6 @@ int main()
5252

5353
// generic wide string, OS-dependent
5454
assert(sizeof(L""[0])==sizeof(wchar_t));
55+
56+
assert(0);
5557
}
Lines changed: 10 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,15 @@
11
CORE
22
main.c
3-
4-
^EXIT=0$
3+
--trace
4+
^State \d+ file main.c function main line 20 thread 0$
5+
^State \d+ file main.c function main line 36 thread 0$
6+
^State \d+ file main.c function main line 44 thread 0$
7+
^\*\* 1 of \d+ failed \(\d+ iterations\)$
8+
^VERIFICATION FAILED$
9+
^EXIT=10$
510
^SIGNAL=0$
6-
^VERIFICATION SUCCESSFUL$
711
--
812
^warning: ignoring
13+
^State \d+ (function main )?thread 0$
14+
--
15+
Each step in the trace must have a full source location, including line numbers.

src/util/string_constant.cpp

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -53,5 +53,8 @@ array_exprt string_constantt::to_array_expr() const
5353
*it = from_integer(ch, char_type);
5454
}
5555

56+
if(source_location().is_not_nil())
57+
dest.add_source_location() = source_location();
58+
5659
return dest;
5760
}

0 commit comments

Comments
 (0)