Skip to content

Commit 5d451cc

Browse files
author
Daniel Kroening
committed
introduce protected_exprt
This will serve as the interface that we aspire exprt to offer; in particular, access to opX is protected.
1 parent e12c7ee commit 5d451cc

File tree

9 files changed

+134
-99
lines changed

9 files changed

+134
-99
lines changed

src/ansi-c/expr2c.cpp

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1939,9 +1939,11 @@ std::string expr2ct::convert_constant(
19391939
if(src.operands().size()!=1)
19401940
return convert_norep(src, precedence);
19411941

1942-
if(src.op0().id()==ID_constant)
1942+
const auto &annotation = to_unary_expr(src).op();
1943+
1944+
if(annotation.id() == ID_constant)
19431945
{
1944-
const irep_idt &op_value=src.op0().get(ID_value);
1946+
const irep_idt &op_value = to_constant_expr(annotation).get_value();
19451947

19461948
if(op_value=="INVALID" ||
19471949
has_prefix(id2string(op_value), "INVALID-") ||
@@ -1951,7 +1953,7 @@ std::string expr2ct::convert_constant(
19511953
return convert_norep(src, precedence);
19521954
}
19531955
else
1954-
return convert_with_precedence(src.op0(), precedence);
1956+
return convert_with_precedence(annotation, precedence);
19551957
}
19561958
}
19571959
else if(type.id()==ID_string)

src/goto-programs/remove_function_pointers.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -391,13 +391,13 @@ void remove_function_pointerst::remove_function_pointer(
391391
t3->make_goto(t_final, true_exprt());
392392

393393
// goto to call
394-
address_of_exprt address_of(fun, pointer_type(fun.type()));
394+
const address_of_exprt address_of(fun, pointer_type(fun.type()));
395395

396-
if(address_of.type()!=pointer.type())
397-
address_of.make_typecast(pointer.type());
396+
const auto casted_address =
397+
typecast_exprt::conditional_cast(address_of, pointer.type());
398398

399399
goto_programt::targett t4=new_code_gotos.add_instruction();
400-
t4->make_goto(t1, equal_exprt(pointer, address_of));
400+
t4->make_goto(t1, equal_exprt(pointer, casted_address));
401401
}
402402

403403
// fall-through

src/pointer-analysis/value_set_fi.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -850,8 +850,8 @@ void value_set_fit::get_reference_set_sharing_rec(
850850
insert(dest, exprt(ID_unknown, expr.type()));
851851
else
852852
{
853-
index_exprt index_expr(
854-
object, from_integer(0, index_type()), expr.type());
853+
exprt index_expr =
854+
index_exprt(object, from_integer(0, index_type()), expr.type());
855855

856856
// adjust type?
857857
if(object.type().id() != "#REF#" && object.type() != array_type)

src/pointer-analysis/value_set_fivr.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -961,8 +961,8 @@ void value_set_fivrt::get_reference_set_sharing_rec(
961961
insert_from(dest, exprt(ID_unknown, expr.type()));
962962
else
963963
{
964-
index_exprt index_expr(
965-
object, from_integer(0, index_type()), expr.type());
964+
exprt index_expr =
965+
index_exprt(object, from_integer(0, index_type()), expr.type());
966966

967967
// adjust type?
968968
if(object.type().id() != "#REF#" && object.type() != array_type)

src/pointer-analysis/value_set_fivrns.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -654,8 +654,8 @@ void value_set_fivrnst::get_reference_set_rec(
654654
insert_from(dest, exprt(ID_unknown, expr.type()));
655655
else
656656
{
657-
index_exprt index_expr(
658-
object, from_integer(0, index_type()), expr.type());
657+
exprt index_expr =
658+
index_exprt(object, from_integer(0, index_type()), expr.type());
659659

660660
// adjust type?
661661
if(object.type() != array_type)

src/util/expr.h

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -319,6 +319,40 @@ class exprt:public irept
319319
const_unique_depth_iteratort unique_depth_cend() const;
320320
};
321321

322+
/// Protected class for all expressions.
323+
/// This API will eventually replace exprt.
324+
class expr_protectedt : public exprt
325+
{
326+
protected:
327+
// constructors
328+
DEPRECATED("use expr_protectedt(id, type) instead")
329+
expr_protectedt() : exprt()
330+
{
331+
}
332+
333+
DEPRECATED("use expr_protectedt(id, type) instead")
334+
explicit expr_protectedt(const irep_idt &_id) : exprt(_id)
335+
{
336+
}
337+
338+
expr_protectedt(const irep_idt &_id, const typet &_type) : exprt(_id, _type)
339+
{
340+
}
341+
342+
// protect these low-level methods
343+
using exprt::make_bool;
344+
using exprt::make_typecast;
345+
using exprt::op0;
346+
using exprt::op1;
347+
using exprt::op2;
348+
using exprt::op3;
349+
// using exprt::find;
350+
// using exprt::get;
351+
// using exprt::set;
352+
using exprt::add;
353+
using exprt::remove;
354+
};
355+
322356
class expr_visitort
323357
{
324358
public:

src/util/pointer_offset_size.cpp

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -593,8 +593,11 @@ exprt build_sizeof_expr(
593593
const constant_exprt &expr,
594594
const namespacet &ns)
595595
{
596-
const typet &type=
597-
static_cast<const typet &>(expr.find(ID_C_c_sizeof_type));
596+
// need to cast down to access 'find'
597+
const auto &expr_as_irep = static_cast<const irept &>(expr);
598+
599+
const typet &type =
600+
static_cast<const typet &>(expr_as_irep.find(ID_C_c_sizeof_type));
598601

599602
if(type.is_nil())
600603
return nil_exprt();

src/util/std_expr.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -150,8 +150,8 @@ extractbits_exprt::extractbits_exprt(
150150
const exprt &_src,
151151
const std::size_t _upper,
152152
const std::size_t _lower,
153-
const typet &_type):
154-
exprt(ID_extractbits, _type)
153+
const typet &_type)
154+
: expr_protectedt(ID_extractbits, _type)
155155
{
156156
PRECONDITION(_upper >= _lower);
157157
operands().resize(3);

0 commit comments

Comments
 (0)