is_compile_time_constantt: honour short-circuit semantics

The C standard stipulates that short-circuit semantics should be honoured
when considering whether an expression is a "constant expression."

Author: tautschnig

src/ansi-c/c_typecheck_expr.cpp

@@ -81,6 +81,33 @@ class is_compile_time_constantt
     {
       return is_constant_address_of(to_address_of_expr(e).object());
     }
+    // we need to adhere to short-circuit semantics for the following
+    else if(e.id() == ID_if)
+    {
+      const if_exprt &if_expr = to_if_expr(e);
+      if(!is_constant(if_expr.cond()))
+        return false;
+      exprt const_cond = simplify_expr(if_expr.cond(), ns);
+      CHECK_RETURN(const_cond.is_constant());
+      if(const_cond.is_true())
+        return is_constant(if_expr.true_case());
+      else
+        return is_constant(if_expr.false_case());
+    }
+    else if(e.id() == ID_and || e.id() == ID_or)
+    {
+      for(const auto &op : e.operands())
+      {
+        if(!is_constant(op))
+          return false;
+        exprt const_cond = simplify_expr(op, ns);
+        CHECK_RETURN(const_cond.is_constant());
+        // stop when we hit false (for an and) or true (for an or)
+        if(const_cond == make_boolean_expr(e.id() == ID_or))
+          break;
+      }
+      return true;
+    }
     // we choose to accept the following expressions (over constant operands) as
     // constant expressions
     else if(
@@ -89,8 +116,7 @@ class is_compile_time_constantt
       e.id() == ID_struct || e.id() == ID_union || e.id() == ID_empty_union ||
       e.id() == ID_equal || e.id() == ID_notequal || e.id() == ID_lt ||
       e.id() == ID_le || e.id() == ID_gt || e.id() == ID_ge ||
-      e.id() == ID_if || e.id() == ID_not || e.id() == ID_and ||
-      e.id() == ID_or || e.id() == ID_bitnot || e.id() == ID_bitand ||
+      e.id() == ID_not || e.id() == ID_bitnot || e.id() == ID_bitand ||
       e.id() == ID_bitor || e.id() == ID_bitxor || e.id() == ID_vector)
     {
       return std::all_of(