Skip to content

Commit c09873b

Browse files
committed
Replace side effects expressions inside address_of
The C++ front-end may generate expressions that take the address of side effects, such as temporary objects or assignments, when a reference is taken. These side effects need to be replaced, just as is done outside address_of expressions.
1 parent bfc11dc commit c09873b

File tree

8 files changed

+41
-6
lines changed

8 files changed

+41
-6
lines changed

regression/cbmc-cpp/lvalue1/main.cpp

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
#include <cassert>
2+
enum asd
3+
{
4+
ASD,
5+
ABC
6+
};
7+
8+
int main()
9+
{
10+
asd a = ASD, b = ASD;
11+
12+
// casts to references are lvalues
13+
asd &c = (asd &)((int &)a |= (int &)b);
14+
assert(a == ASD);
15+
c = ABC;
16+
assert(a == ABC);
17+
18+
// in C++, comma expressions are lvalues
19+
(a, b) = ASD;
20+
}

regression/cbmc-cpp/lvalue1/test.desc

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.cpp
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
VERIFICATION SUCCESSFUL
7+
--
8+
^warning: ignoring
9+
^CONVERSION ERROR$
10+
--

regression/systemc/Masc1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.cpp
33

44
^EXIT=0$

regression/systemc/MascInst1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.cpp
33

44
^EXIT=0$

regression/systemc/This1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.cpp
33

44
^EXIT=0$

src/cpp/cpp_constructor.cpp

+2-3
Original file line numberDiff line numberDiff line change
@@ -269,9 +269,8 @@ void cpp_typecheckt::new_temporary(
269269
exprt &temporary)
270270
{
271271
// create temporary object
272-
exprt tmp_object_expr=exprt(ID_side_effect, type);
273-
tmp_object_expr.set(ID_statement, ID_temporary_object);
274-
tmp_object_expr.add_source_location()= source_location;
272+
side_effect_exprt tmp_object_expr(ID_temporary_object, type, source_location);
273+
tmp_object_expr.set(ID_mode, ID_cpp);
275274

276275
exprt new_object(ID_new_object);
277276
new_object.add_source_location()=tmp_object_expr.source_location();

src/cpp/cpp_typecheck_conversions.cpp

+2
Original file line numberDiff line numberDiff line change
@@ -911,6 +911,7 @@ bool cpp_typecheckt::user_defined_conversion_sequence(
911911
ID_temporary_object, type, expr.source_location());
912912
tmp_object_expr.copy_to_operands(deref);
913913
tmp_object_expr.set(ID_C_lvalue, true);
914+
tmp_object_expr.set(ID_mode, ID_cpp);
914915

915916
new_expr.swap(tmp_object_expr);
916917
return true;
@@ -1390,6 +1391,7 @@ bool cpp_typecheckt::reference_binding(
13901391
// create temporary object
13911392
side_effect_exprt tmp(
13921393
ID_temporary_object, type.subtype(), expr.source_location());
1394+
tmp.set(ID_mode, ID_cpp);
13931395
// tmp.set(ID_C_lvalue, true);
13941396
tmp.add_to_operands(std::move(new_expr));
13951397
new_expr.swap(tmp);

src/goto-programs/goto_clean_expr.cpp

+4
Original file line numberDiff line numberDiff line change
@@ -487,6 +487,10 @@ void goto_convertt::clean_expr_address_of(
487487
// do again
488488
clean_expr_address_of(expr, dest, mode);
489489
}
490+
else if(expr.id() == ID_side_effect)
491+
{
492+
remove_side_effect(to_side_effect_expr(expr), dest, mode, true);
493+
}
490494
else
491495
Forall_operands(it, expr)
492496
clean_expr_address_of(*it, dest, mode);

0 commit comments

Comments
 (0)