Skip to content

string_constantt::to_array_expr must maintain the source location #6995

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions regression/cbmc/String_Literal1/main.c
Original file line number Diff line number Diff line change
Expand Up @@ -52,4 +52,6 @@ int main()

// generic wide string, OS-dependent
assert(sizeof(L""[0])==sizeof(wchar_t));

assert(0);
}
13 changes: 10 additions & 3 deletions regression/cbmc/String_Literal1/test.desc
Original file line number Diff line number Diff line change
@@ -1,8 +1,15 @@
CORE
main.c

^EXIT=0$
--trace
^State \d+ file main.c function main line 20 thread 0$
^State \d+ file main.c function main line 36 thread 0$
^State \d+ file main.c function main line 44 thread 0$
^\*\* 1 of \d+ failed \(\d+ iterations\)$
^VERIFICATION FAILED$
^EXIT=10$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
^State \d+ (function main )?thread 0$
--
Each step in the trace must have a full source location, including line numbers.
24 changes: 24 additions & 0 deletions src/util/expr.h
Original file line number Diff line number Diff line change
Expand Up @@ -98,6 +98,30 @@ class exprt:public irept
const operandst &operands() const
{ return (const operandst &)get_sub(); }

/// Add the source location from \p other, if it has any.
template <typename T>
T &with_source_location(const exprt &other) &
{
static_assert(
std::is_base_of<exprt, T>::value,
"The template argument T must be derived from exprt.");
if(other.source_location().is_not_nil())
add_source_location() = other.source_location();
return *static_cast<T *>(this);
}

/// Add the source location from \p other, if it has any.
template <typename T>
T &&with_source_location(const exprt &other) &&
{
static_assert(
std::is_base_of<exprt, T>::value,
"The template argument T must be derived from exprt.");
if(other.source_location().is_not_nil())
add_source_location() = other.source_location();
return std::move(*static_cast<T *>(this));
}

protected:
exprt &op0()
{ return operands().front(); }
Expand Down
10 changes: 10 additions & 0 deletions src/util/std_expr.h
Original file line number Diff line number Diff line change
Expand Up @@ -1571,6 +1571,16 @@ class array_exprt : public multi_ary_exprt
{
return static_cast<array_typet &>(multi_ary_exprt::type());
}

array_exprt &with_source_location(const exprt &other) &
{
return exprt::with_source_location<array_exprt>(other);
}

array_exprt &&with_source_location(const exprt &other) &&
{
return std::move(*this).exprt::with_source_location<array_exprt>(other);
}
};

template <>
Expand Down
2 changes: 1 addition & 1 deletion src/util/string_constant.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -53,5 +53,5 @@ array_exprt string_constantt::to_array_expr() const
*it = from_integer(ch, char_type);
}

return dest;
return std::move(dest).with_source_location(*this);
}
1 change: 0 additions & 1 deletion src/util/string_constant.h
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,6 @@ class string_constantt : public nullary_exprt
}

array_exprt to_array_expr() const;
bool from_array_expr(const array_exprt &);
};

template <>
Expand Down