replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

type simplify_bitnot 

This improves memory safety.
This commit is contained in:
Daniel Kroening 2019-07-07 13:34:44 +01:00
parent b42d47d914
commit 866acc9a0a
3 changed files with 6 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/util/simplify_expr.cpp
View File

@ -2278,7 +2278,7 @@ bool simplify_exprt::simplify_node(exprt &expr)
} }
else if(expr.id()==ID_bitnot) else if(expr.id()==ID_bitnot)
{ {
r = simplify_bitnot(expr); r = simplify_bitnot(to_bitnot_expr(expr));
} }
else if(expr.id()==ID_bitand || else if(expr.id()==ID_bitand ||
expr.id()==ID_bitor || expr.id()==ID_bitor ||

3
src/util/simplify_expr_class.h
View File

@ -30,6 +30,7 @@ class abs_exprt;
class address_of_exprt; class address_of_exprt;
class array_exprt; class array_exprt;
class binary_relation_exprt; class binary_relation_exprt;
class bitnot_exprt;
class bswap_exprt; class bswap_exprt;
class byte_extract_exprt; class byte_extract_exprt;
class byte_update_exprt; class byte_update_exprt;
@ -146,7 +147,7 @@ public:
NODISCARD resultt<> simplify_bitwise(const exprt &); NODISCARD resultt<> simplify_bitwise(const exprt &);
bool simplify_if_preorder(if_exprt &expr); bool simplify_if_preorder(if_exprt &expr);
NODISCARD resultt<> simplify_if(const if_exprt &); NODISCARD resultt<> simplify_if(const if_exprt &);
NODISCARD resultt<> simplify_bitnot(const exprt &); NODISCARD resultt<> simplify_bitnot(const bitnot_exprt &);
NODISCARD resultt<> simplify_not(const exprt &); NODISCARD resultt<> simplify_not(const exprt &);
NODISCARD resultt<> simplify_boolean(const exprt &); NODISCARD resultt<> simplify_boolean(const exprt &);
NODISCARD resultt<> simplify_inequality(const exprt &); NODISCARD resultt<> simplify_inequality(const exprt &);

10
src/util/simplify_expr_int.cpp
View File

@ -1182,14 +1182,10 @@ simplify_exprt::simplify_unary_minus(const exprt &expr)
return unchanged(expr); return unchanged(expr);
} }
simplify_exprt::resultt<> simplify_exprt::simplify_bitnot(const exprt &expr) simplify_exprt::resultt<>
simplify_exprt::simplify_bitnot(const bitnot_exprt &expr)
{ {
const exprt::operandst &operands = expr.operands(); const exprt &op = expr.op();
if(operands.size()!=1)
return unchanged(expr);
const exprt &op = operands.front();
const auto &type = expr.type(); const auto &type = expr.type();