check for side effects in quantifiers in the front-end

This fixes a failed attempt to check for quantifiers during goto conversion
by checking earlier in the C front-end.

Author: Daniel Kroening

regression/cbmc/Quantifiers1/quantifier-with-side-effect.c

@@ -0,0 +1,12 @@
+int func()
+{
+  return 1;
+}
+
+int main()
+{
+  // no side effects!
+  assert(__CPROVER_forall { int i; func() } );
+
+  return 0;
+}

regression/cbmc/Quantifiers1/quantifier-with-side-effect.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+^file .* line 9 function main: quantifier must not contain side effects$
+--

src/ansi-c/c_typecheck_expr.cpp

@@ -166,6 +166,18 @@ bool c_typecheck_baset::gcc_types_compatible_p(
   return false;
 }
 
+static bool has_side_effect(const exprt &expr)
+{
+  if(expr.id() == ID_side_effect)
+    return true;
+
+  for(const auto &op : expr.operands())
+    if(has_side_effect(op))
+      return true;
+
+  return false;
+}
+
 void c_typecheck_baset::typecheck_expr_main(exprt &expr)
 {
   if(expr.id()==ID_side_effect)
@@ -303,6 +315,13 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
       throw 0;
     }
 
+    if(has_side_effect(expr.op1()))
+    {
+      err_location(expr);
+      error() << "quantifier must not contain side effects" << eom;
+      throw 0;
+    }
+
     // replace declaration by symbol expression
     symbol_exprt bound=to_symbol_expr(expr.op0().op0());
     expr.op0().swap(bound);

src/goto-programs/goto_clean_expr.cpp

@@ -405,18 +405,7 @@ void goto_convertt::clean_expr(
   }
   else if(expr.id()==ID_forall || expr.id()==ID_exists)
   {
-    assert(expr.operands().size()==2);
-    // check if there are side-effects
-    goto_programt tmp;
-    clean_expr(expr.op1(), tmp, mode, true);
-    if(tmp.instructions.empty())
-    {
-      error().source_location=expr.find_source_location();
-      error() << "no side-effects in quantified expressions allowed"
-              << eom;
-      throw 0;
-    }
-    return;
+    // the front-end checks these for side-effects
   }
   else if(expr.id()==ID_address_of)
   {