Fix based on comments

Author: Petr Bauch

src/goto-programs/goto_program.cpp

@@ -749,8 +749,8 @@ void goto_programt::instructiont::validate(
     DATA_CHECK_WITH_DIAGNOSTICS(
       vm,
       !ns.lookup(to_code_decl(code).get_identifier(), table_symbol),
-      "declaring unknown symbol: " +
-        id2string(to_code_decl(code).get_identifier()),
+      "declared symbols should be known",
+      id2string(to_code_decl(code).get_identifier()),
       source_location);
     break;
   case DEAD:
@@ -762,8 +762,8 @@ void goto_programt::instructiont::validate(
     DATA_CHECK_WITH_DIAGNOSTICS(
       vm,
       !ns.lookup(to_code_dead(code).get_identifier(), table_symbol),
-      "removing unknown symbol: " +
-        id2string(to_code_dead(code).get_identifier()) + " from scope",
+      "removed symbols should be known",
+      id2string(to_code_dead(code).get_identifier()),
       source_location);
     break;
   case FUNCTION_CALL:

src/util/std_expr.cpp

@@ -215,7 +215,7 @@ bool evaluates_to_boolean(const exprt &e)
   if(e.type().id() != ID_bool)
     return false;
   if(e.id() == ID_typecast)
-    return e.type().id() == ID_bool;
+    return true;
 
   // Boolean constants
   if(e.id() == ID_true || e.id() == ID_false)

unit/Makefile

@@ -17,6 +17,7 @@ SRC += analyses/ai/ai.cpp \
        compound_block_locations.cpp \
        goto-programs/goto_trace_output.cpp \
        goto-programs/goto_program_assume.cpp \
+       goto-programs/goto_program_dead.cpp \
        goto-programs/goto_program_declaration.cpp \
        goto-programs/goto_program_function_call.cpp \
        goto-programs/goto_program_goto_target.cpp \

unit/goto-programs/goto_program_dead.cpp

@@ -0,0 +1,66 @@
+/*******************************************************************\
+
+  Module: Unit tests for goto_program::validate
+
+  Author: Diffblue Ltd.
+
+ \*******************************************************************/
+
+#include <goto-programs/goto_function.h>
+#include <testing-utils/catch.hpp>
+#include <util/arith_tools.h>
+
+SCENARIO(
+  "Validation of well-formed symbol removing codes",
+  "[core][goto-programs][validate]")
+{
+  GIVEN("A program with one symbol removal")
+  {
+    symbol_tablet symbol_table;
+    const signedbv_typet type1(32);
+
+    symbolt var_symbol;
+    irep_idt var_symbol_name = "a";
+    var_symbol.type = type1;
+    var_symbol.name = var_symbol_name;
+    symbol_exprt var_a(var_symbol_name, type1);
+
+    goto_functiont goto_function;
+    auto &instructions = goto_function.body.instructions;
+    instructions.emplace_back(goto_program_instruction_typet::DEAD);
+    code_deadt removal(var_a);
+    instructions.back().make_dead();
+    instructions.back().code = removal;
+
+    WHEN("Removing known symbol")
+    {
+      symbol_table.insert(var_symbol);
+      const namespacet ns(symbol_table);
+
+      THEN("The consistency check succeeds")
+      {
+        goto_function.body.validate(ns, validation_modet::INVARIANT);
+        REQUIRE(true);
+      }
+    }
+
+    WHEN("Removing unknown symbol")
+    {
+      const namespacet ns(symbol_table);
+
+      THEN("The consistency check fails")
+      {
+        bool caught = false;
+        try
+        {
+          goto_function.body.validate(ns, validation_modet::EXCEPTION);
+        }
+        catch(incorrect_goto_program_exceptiont &e)
+        {
+          caught = true;
+        }
+        REQUIRE(caught);
+      }
+    }
+  }
+}