From 8f3d1414e3ee9cdc23d3e6815b1685747620155b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Wed, 7 Sep 2016 12:15:13 +0200 Subject: [PATCH 1/2] direct support for ID_c_bool in exprt The `is_true()` / `is_false()` functions in `exprt` currently support only the `ID_bool` type. In Java, Boolean values are represented as `ID_c_bool` due to the internal JVM usage of integers. Adding this support here seems easier than having special treatment in `java_bytecode`. --- src/util/expr.cpp | 26 ++++++++++++++++++++------ src/util/mp_arith.h | 1 + 2 files changed, 21 insertions(+), 6 deletions(-) diff --git a/src/util/expr.cpp b/src/util/expr.cpp index e31f18d688d..3b3525dd9ac 100644 --- a/src/util/expr.cpp +++ b/src/util/expr.cpp @@ -245,9 +245,18 @@ Function: exprt::is_true bool exprt::is_true() const { - return is_constant() && - type().id()==ID_bool && - get(ID_value)!=ID_false; + if(is_constant()) + { + if(type().id()==ID_bool) + return get(ID_value)!=ID_false; + else if(type().id()==ID_c_bool) + { + mp_integer i; + to_integer(*this,i); + return i!=mp_zero; + } + } + return false; } /*******************************************************************\ @@ -264,9 +273,14 @@ Function: exprt::is_false bool exprt::is_false() const { - return is_constant() && - type().id()==ID_bool && - get(ID_value)==ID_false; + if(is_constant()) + { + if(type().id()==ID_bool) + return get(ID_value)==ID_false; + else if(type().id()==ID_c_bool) + return !is_true(); + } + return false; } /*******************************************************************\ diff --git a/src/util/mp_arith.h b/src/util/mp_arith.h index 007e477b62b..0f1f8205177 100644 --- a/src/util/mp_arith.h +++ b/src/util/mp_arith.h @@ -27,5 +27,6 @@ const mp_integer binary2integer(const std::string &, bool is_signed); mp_integer::ullong_t integer2ulong(const mp_integer &); std::size_t integer2size_t(const mp_integer &); unsigned integer2unsigned(const mp_integer &); +const mp_integer mp_zero=string2integer("0"); #endif From 5c0757ce14de5c7a1b6d02c260d6d94afd1342b0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Thu, 27 Oct 2016 14:20:36 +0200 Subject: [PATCH 2/2] take comment into account --- src/util/expr.cpp | 2 +- src/util/mp_arith.h | 1 - 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/src/util/expr.cpp b/src/util/expr.cpp index 3b3525dd9ac..8cf61eb2d27 100644 --- a/src/util/expr.cpp +++ b/src/util/expr.cpp @@ -253,7 +253,7 @@ bool exprt::is_true() const { mp_integer i; to_integer(*this,i); - return i!=mp_zero; + return i!=mp_integer(0); } } return false; diff --git a/src/util/mp_arith.h b/src/util/mp_arith.h index 0f1f8205177..007e477b62b 100644 --- a/src/util/mp_arith.h +++ b/src/util/mp_arith.h @@ -27,6 +27,5 @@ const mp_integer binary2integer(const std::string &, bool is_signed); mp_integer::ullong_t integer2ulong(const mp_integer &); std::size_t integer2size_t(const mp_integer &); unsigned integer2unsigned(const mp_integer &); -const mp_integer mp_zero=string2integer("0"); #endif