Skip to content

Commit

Permalink
Do not use c_typecast in pointer-analysis
Browse files Browse the repository at this point in the history
goto-programs are not C specific.
  • Loading branch information
tautschnig committed Jun 6, 2018
1 parent 2ed63f5 commit d089ddd
Show file tree
Hide file tree
Showing 2 changed files with 4 additions and 10 deletions.
1 change: 0 additions & 1 deletion src/pointer-analysis/module_dependencies.txt
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
analyses
ansi-c # should go away
goto-programs
langapi # should go away
pointer-analysis
Expand Down
13 changes: 4 additions & 9 deletions src/pointer-analysis/value_set_dereference.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -31,8 +31,6 @@ Author: Daniel Kroening, [email protected]
#include <util/pointer_predicates.h>
#include <util/ssa_expr.h>

#include <ansi-c/c_typecast.h>

// global data, horrible
unsigned int value_set_dereferencet::invalid_counter=0;

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

binary_relation_exprt inequality(expr.index(), ID_ge, size_expr);

if(c_implicit_typecast(
inequality.op0(),
inequality.op1().type(),
ns))
throw "index address of wrong type";
binary_relation_exprt inequality(
typecast_exprt::conditional_cast(expr.index(), size_expr.type()),
ID_ge,
size_expr);

guardt tmp_guard(guard);
tmp_guard.add(inequality);
Expand Down

0 comments on commit d089ddd

Please sign in to comment.