From 4d215fae863d88279c60f2b5d846b8c79eab5914 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sun, 31 Jul 2022 09:44:27 +0100
Subject: [PATCH] fix for preincrement on _Bool

This fixes an issue with preincrement on _Bool during the conversion to goto
programs.
---
 regression/cbmc/Bool/bool6.desc               |  2 +-
 .../goto_convert_side_effect.cpp              | 24 +++++++++++++++----
 2 files changed, 21 insertions(+), 5 deletions(-)

diff --git a/regression/cbmc/Bool/bool6.desc b/regression/cbmc/Bool/bool6.desc
index 9e0fb674be7..59c4d81608f 100644
--- a/regression/cbmc/Bool/bool6.desc
+++ b/regression/cbmc/Bool/bool6.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 bool6.c
 
 ^EXIT=0$
diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp
index b6630a44c89..2d94df6a85e 100644
--- a/src/goto-programs/goto_convert_side_effect.cpp
+++ b/src/goto-programs/goto_convert_side_effect.cpp
@@ -223,12 +223,25 @@ void goto_convertt::remove_pre(
     op, statement == ID_preincrement ? ID_plus : ID_minus, std::move(constant)};
   rhs.add_source_location() = expr.source_location();
 
+  // Is there a typecast, e.g., for _Bool? If so, transform
+  // t1(op : t2) := op+1  -->  op := t2(op+1)
+  exprt lhs;
+  if(op.id() == ID_typecast)
+  {
+    lhs = to_typecast_expr(op).op();
+    rhs = typecast_exprt(rhs, lhs.type());
+  }
+  else
+  {
+    lhs = op;
+  }
+
   const bool cannot_use_lhs =
-    result_is_used && !address_taken && needs_cleaning(op);
+    result_is_used && !address_taken && needs_cleaning(lhs);
   if(cannot_use_lhs)
     make_temp_symbol(rhs, "pre", dest, mode);
 
-  code_assignt assignment(op, rhs);
+  code_assignt assignment(lhs, rhs);
   assignment.add_source_location()=expr.find_source_location();
 
   convert(assignment, dest, mode);
@@ -236,11 +249,14 @@ void goto_convertt::remove_pre(
   if(result_is_used)
   {
     if(cannot_use_lhs)
-      expr.swap(rhs);
+    {
+      auto tmp = typecast_exprt::conditional_cast(rhs, expr.type());
+      expr.swap(tmp);
+    }
     else
     {
       // revert to argument of pre-inc/pre-dec
-      exprt tmp = op;
+      auto tmp = typecast_exprt::conditional_cast(lhs, expr.type());
       expr.swap(tmp);
     }
   }