Enable goto-model validation for ternary and bitvector expressions

The code was almost there, but was never triggered.

Author: tautschnig

src/util/std_expr.h

@@ -79,6 +79,14 @@ class ternary_exprt : public expr_protectedt
       expr.operands().size() == 3,
       "ternary expression must have three operands");
   }
+
+  static void validate(
+    const exprt &expr,
+    const namespacet &,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    check(expr, vm);
+  }
 };
 
 /// \brief Cast an exprt to a \ref ternary_exprt
@@ -2294,6 +2302,21 @@ class if_exprt : public ternary_exprt
   {
     return op2();
   }
+
+  static void check(
+    const exprt &expr,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    ternary_exprt::check(expr, vm);
+  }
+
+  static void validate(
+    const exprt &expr,
+    const namespacet &ns,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    ternary_exprt::validate(expr, ns, vm);
+  }
 };
 
 template <>
@@ -2563,6 +2586,21 @@ class update_exprt : public ternary_exprt
   {
     return op2();
   }
+
+  static void check(
+    const exprt &expr,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    ternary_exprt::check(expr, vm);
+  }
+
+  static void validate(
+    const exprt &expr,
+    const namespacet &ns,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    ternary_exprt::validate(expr, ns, vm);
+  }
 };
 
 template <>

src/util/validate_expressions.cpp

@@ -13,6 +13,7 @@ Author: Daniel Poetzl
 #include <iostream>
 #endif
 
+#include "bitvector_expr.h"
 #include "pointer_expr.h"
 #include "ssa_expr.h"
 
@@ -46,6 +47,22 @@ void call_on_expr(const exprt &expr, Args &&... args)
   {
     CALL_ON_EXPR(constant_exprt);
   }
+  else if(expr.id() == ID_if)
+  {
+    CALL_ON_EXPR(if_exprt);
+  }
+  else if(expr.id() == ID_update)
+  {
+    CALL_ON_EXPR(update_exprt);
+  }
+  else if(expr.id() == ID_overflow_unary_minus)
+  {
+    CALL_ON_EXPR(unary_minus_overflow_exprt);
+  }
+  else if(expr.id() == ID_count_leading_zeros)
+  {
+    CALL_ON_EXPR(count_leading_zeros_exprt);
+  }
   else
   {
 #ifdef REPORT_UNIMPLEMENTED_EXPRESSION_CHECKS