From afc448095dc9c93bbbc80d73c66306e07ef4585a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Mon, 16 Jan 2017 14:30:03 +0100 Subject: [PATCH] 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 ++++++++++++++++++++------ 1 file changed, 20 insertions(+), 6 deletions(-) diff --git a/src/util/expr.cpp b/src/util/expr.cpp index b317b434e41..7f77a06457c 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_integer(0); + } + } + 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; } /*******************************************************************\