Skip to content

Commit a29bc10

Browse files
committed
fallback formatter: don't print #source_location=""
This makes default-formatted expressions less verbose.
1 parent d0e7c3d commit a29bc10

File tree

2 files changed

+2
-2
lines changed

2 files changed

+2
-2
lines changed

regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
double_deref_with_pointer_arithmetic.c
33
--show-vcc
4-
^\{-[0-9]+\} derefd_pointer::derefd_pointer!0#1 = \{ symex_dynamic::dynamic_object1#3\[\[0\]\], symex_dynamic::dynamic_object1#3\[\[1\]\] \}\[cast\(mod #source_location=""\(main::argc!0@1#1, 2\), signedbv\[64\]\)\]
4+
^\{-[0-9]+\} derefd_pointer::derefd_pointer!0#1 = \{ symex_dynamic::dynamic_object1#3\[\[0\]\], symex_dynamic::dynamic_object1#3\[\[1\]\] \}\[cast\(mod\(main::argc!0@1#1, 2\), signedbv\[64\]\)\]
55
^\{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object[23]\) \? main::argc!0@1#1 = 2 : \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object[23]\) \? main::argc!0@1#1 = 1 : symex::invalid_object!0#0 = main::argc!0@1#1\)\)
66
^EXIT=0$
77
^SIGNAL=0$

src/util/format_expr.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -223,7 +223,7 @@ std::ostream &fallback_format_rec(std::ostream &os, const exprt &expr)
223223
os << expr.id();
224224

225225
for(const auto &s : expr.get_named_sub())
226-
if(s.first != ID_type)
226+
if(s.first != ID_type && s.first != ID_C_source_location)
227227
os << ' ' << s.first << "=\"" << s.second.id() << '"';
228228

229229
if(expr.has_operands())

0 commit comments

Comments
 (0)