Fixes formatting.

Author: ArenBabikian

regression/contracts/quantifiers-exists-ensures-01/main.c

@@ -1,7 +1,7 @@
-int f1(int *arr)
-  __CPROVER_ensures(
-    __CPROVER_exists {int i; (0 <= i && i < 10) && arr[i] == i}
-  )
+int f1(int *arr) __CPROVER_ensures(__CPROVER_exists {
+  int i;
+  (0 <= i && i < 10) && arr[i] == i
+})
 {
   for(int i = 0; i < 10; i++)
   {

regression/contracts/quantifiers-exists-ensures-02/main.c

@@ -1,7 +1,7 @@
-int f1(int *arr)
-  __CPROVER_ensures(
-    __CPROVER_exists {int i; (0 <= i && i < 10) && arr[i] != 0}
-  )
+int f1(int *arr) __CPROVER_ensures(__CPROVER_exists {
+  int i;
+  (0 <= i && i < 10) && arr[i] != 0
+})
 {
   for(int i = 0; i < 10; i++)
   {

regression/contracts/quantifiers-forall-ensures-01/main.c

@@ -1,7 +1,9 @@
-int f1(int *arr)
-  __CPROVER_ensures(
-    __CPROVER_forall {int i; (0 <= i && i < 10) ==> arr[i] == 0}
-  )
+// clang-format oFF
+int f1(int *arr) __CPROVER_ensures(__CPROVER_forall {
+  int i;
+  (0 <= i && i < 10) ==> arr[i] == 0
+})
+// clang-format on
 {
   for(int i = 0; i < 10; i++)
   {

regression/contracts/quantifiers-forall-ensures-02/main.c

@@ -1,12 +1,16 @@
-int f1(int *arr)
-  __CPROVER_ensures(
-    __CPROVER_forall {int i; (0 <= i && i < 10) ==> arr[i] == i}
-  )
+// clang-format oFF
+int f1(int *arr) __CPROVER_ensures(__CPROVER_forall {
+  int i;
+  (0 <= i && i < 10) ==> arr[i] == i
+})
+// clang-format on
 {
   for(int i = 0; i < 10; i++)
   {
-    if (i == 0) arr[i] = -1;
-    else arr[i] = i;
+    if(i == 0)
+      arr[i] = -1;
+    else
+      arr[i] = i;
   }
 
   return 0;

src/goto-instrument/code_contracts.cpp

@@ -149,7 +149,7 @@ static void check_apply_invariants(
 
   // change the back edge into assume(false) or assume(guard)
   loop_end->targets.clear();
-  loop_end->type=ASSUME;
+  loop_end->type = ASSUME;
   if(loop_head->is_goto())
     loop_end->set_condition(false_exprt());
   else
@@ -168,20 +168,21 @@ void code_contractst::add_quantified_variable(
   replace_symbolt &replace,
   irep_idt mode)
 {
-  //If the expression is a quantified expression, this function adds
-  //the quantified variable to the symbol table and to the expression map
+  // If the expression is a quantified expression, this function adds
+  // the quantified variable to the symbol table and to the expression map
 
-  //TODO Currently only works if the contract contains only a single quantified formula
+  // TODO Currently only works if the contract contains only a single 
+  // quantified formula
   // i.e. (1) the top-level element is a quantifier formula
-  //and (2) there are no inner quantifier formulae
+  // and (2) there are no inner quantifier formulae
   if(expression.id() == ID_exists || expression.id() == ID_forall)
   {
-    //get quantified symbol
+    // get quantified symbol
     exprt tuple = expression.operands().front();
     exprt quantified_variable = tuple.operands().front();
     symbol_exprt quantified_symbol = to_symbol_expr(quantified_variable);
 
-    //create fresh symbol
+    // create fresh symbol
     symbolt new_symbol = get_fresh_aux_symbol(
       quantified_symbol.type(),
       id2string(quantified_symbol.get_identifier()),
@@ -264,7 +265,7 @@ bool code_contractst::apply_function_contract(
   }
 
   // Replace formal parameters
-  code_function_callt::argumentst::const_iterator a_it=
+  code_function_callt::argumentst::const_iterator a_it =
     call.arguments().begin();
   for(code_typet::parameterst::const_iterator p_it = type.parameters().begin();
       p_it != type.parameters().end() && a_it != call.arguments().end();
@@ -479,38 +480,38 @@ void code_contractst::instrument_call_statement(
 
     return;
   }
-    else // Called function has assigns clause
+  else // Called function has assigns clause
+  {
+    replace_symbolt replace;
+    // Replace formal parameters
+    code_function_callt::argumentst::const_iterator a_it =
+      call.arguments().begin();
+    for(code_typet::parameterst::const_iterator p_it =
+          called_type.parameters().begin();
+        p_it != called_type.parameters().end() &&
+        a_it != call.arguments().end();
+        ++p_it, ++a_it)
     {
-      replace_symbolt replace;
-      // Replace formal parameters
-      code_function_callt::argumentst::const_iterator a_it =
-        call.arguments().begin();
-      for(code_typet::parameterst::const_iterator p_it =
-            called_type.parameters().begin();
-          p_it != called_type.parameters().end() &&
-          a_it != call.arguments().end();
-          ++p_it, ++a_it)
+      if(!p_it->get_identifier().empty())
       {
-        if(!p_it->get_identifier().empty())
-        {
-          symbol_exprt p(p_it->get_identifier(), p_it->type());
-          replace.insert(p, *a_it);
-        }
+        symbol_exprt p(p_it->get_identifier(), p_it->type());
+        replace.insert(p, *a_it);
       }
-
-      replace(called_assigns);
-
-      // check compatibility of assigns clause with the called function
-      assigns_clauset called_assigns_clause(
-        called_assigns, *this, function_id, log);
-      exprt compatible =
-        assigns_clause.compatible_expression(called_assigns_clause);
-      goto_programt alias_assertion;
-      alias_assertion.add(goto_programt::make_assertion(
-        compatible, instruction_iterator->source_location));
-      program.insert_before_swap(instruction_iterator, alias_assertion);
-      ++instruction_iterator;
     }
+
+    replace(called_assigns);
+
+    // check compatibility of assigns clause with the called function
+    assigns_clauset called_assigns_clause(
+      called_assigns, *this, function_id, log);
+    exprt compatible =
+      assigns_clause.compatible_expression(called_assigns_clause);
+    goto_programt alias_assertion;
+    alias_assertion.add(goto_programt::make_assertion(
+      compatible, instruction_iterator->source_location));
+    program.insert_before_swap(instruction_iterator, alias_assertion);
+    ++instruction_iterator;
+  }
 }
 
 bool code_contractst::check_for_looped_mallocs(const goto_programt &program)
@@ -784,7 +785,7 @@ void code_contractst::add_contract_check(
                        .symbol_expr();
     check.add(goto_programt::make_decl(r, skip->source_location));
 
-    call.lhs()=r;
+    call.lhs() = r;
     return_stmt = code_returnt(r);
 
     symbol_exprt ret_val(CPROVER_PREFIX "return_value", call.lhs().type());

src/goto-instrument/code_contracts.h

@@ -25,7 +25,6 @@ Date: February 2016
 #include <util/message.h>
 #include <util/namespace.h>
 #include <util/pointer_expr.h>
-#include <util/pointer_expr.h>
 #include <util/replace_symbol.h>
 
 class messaget;
@@ -168,8 +167,8 @@ class code_contractst
   void
   add_contract_check(const irep_idt &, const irep_idt &, goto_programt &dest);
 
-  //If the expression is a quantified expression, this function adds
-  //the quantified variable to the symbol table and to the expression map
+  // If the expression is a quantified expression, this function adds
+  // the quantified variable to the symbol table and to the expression map
   void add_quantified_variable(
     exprt expression,
     replace_symbolt &replace,