Skip to content

Commit d089ddd

Browse files
committed
Do not use c_typecast in pointer-analysis
goto-programs are not C specific.
1 parent 2ed63f5 commit d089ddd

File tree

2 files changed

+4
-10
lines changed

2 files changed

+4
-10
lines changed

src/pointer-analysis/module_dependencies.txt

-1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
11
analyses
2-
ansi-c # should go away
32
goto-programs
43
langapi # should go away
54
pointer-analysis

src/pointer-analysis/value_set_dereference.cpp

+4-9
Original file line numberDiff line numberDiff line change
@@ -31,8 +31,6 @@ Author: Daniel Kroening, [email protected]
3131
#include <util/pointer_predicates.h>
3232
#include <util/ssa_expr.h>
3333

34-
#include <ansi-c/c_typecast.h>
35-
3634
// global data, horrible
3735
unsigned int value_set_dereferencet::invalid_counter=0;
3836

@@ -712,13 +710,10 @@ void value_set_dereferencet::bounds_check(
712710
if(size_expr.is_nil())
713711
throw "index array operand of wrong type";
714712

715-
binary_relation_exprt inequality(expr.index(), ID_ge, size_expr);
716-
717-
if(c_implicit_typecast(
718-
inequality.op0(),
719-
inequality.op1().type(),
720-
ns))
721-
throw "index address of wrong type";
713+
binary_relation_exprt inequality(
714+
typecast_exprt::conditional_cast(expr.index(), size_expr.type()),
715+
ID_ge,
716+
size_expr);
722717

723718
guardt tmp_guard(guard);
724719
tmp_guard.add(inequality);

0 commit comments

Comments
 (0)