Fixes formatting

Author: ArenBabikian

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

@@ -1,14 +1,13 @@
-int f1(int *arr)
-  __CPROVER_requires(
-    __CPROVER_exists {int i; (0 <= i && i < 10) && arr[i] == 4}
-  )
-  __CPROVER_ensures(__CPROVER_return_value == 0)
+int f1(int *arr) __CPROVER_requires(__CPROVER_exists {
+  int i;
+  (0 <= i && i < 10) && arr[i] == 4
+}) __CPROVER_ensures(__CPROVER_return_value == 0)
 {
   return 0;
 }
 
 int main()
 {
-  int arr[10] = {0,1,2,3,4,5,6,7,8,9};
+  int arr[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9};
   f1(arr);
 }

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

@@ -1,14 +1,13 @@
-int f1(int *arr)
-  __CPROVER_requires(
-    __CPROVER_exists {int i; (0 <= i && i < 10) && arr[i] == 1}
-  )
-  __CPROVER_ensures(__CPROVER_return_value == 0)
+int f1(int *arr) __CPROVER_requires(__CPROVER_exists {
+  int i;
+  (0 <= i && i < 10) && arr[i] == 1
+}) __CPROVER_ensures(__CPROVER_return_value == 0)
 {
   return 0;
 }
 
 int main()
 {
-  int arr[10] = {0,0,0,0,0,0,0,0,0,0};
+  int arr[10] = {0, 0, 0, 0, 0, 0, 0, 0, 0, 0};
   f1(arr);
 }

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

@@ -1,14 +1,15 @@
-int f1(int *arr)
-  __CPROVER_requires(
-    __CPROVER_forall {int i; (0 <= i && i < 10) ==> arr[i] == i}
-  )
-  __CPROVER_ensures(__CPROVER_return_value == 0)
+// clang-format off
+int f1(int *arr) __CPROVER_requires(__CPROVER_forall {
+  int i;
+  (0 <= i && i < 10) ==> arr[i] == i
+}) __CPROVER_ensures(__CPROVER_return_value == 0)
+// clang-format on
 {
   return 0;
 }
 
 int main()
 {
-  int arr[10] = {0,1,2,3,4,5,6,7,8,9};
+  int arr[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9};
   f1(arr);
 }

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

@@ -1,14 +1,15 @@
-int f1(int *arr)
-  __CPROVER_requires(
-    __CPROVER_forall {int i; (0 <= i && i < 10) ==> arr[i] == i}
-  )
-  __CPROVER_ensures(__CPROVER_return_value == 0)
+// clang-format off
+int f1(int *arr) __CPROVER_requires(__CPROVER_forall {
+  int i;
+  (0 <= i && i < 10) ==> arr[i] == i
+}) __CPROVER_ensures(__CPROVER_return_value == 0)
+// clang-format on
 {
   return 0;
 }
 
 int main()
 {
-  int arr[10] = {-1,1,2,3,4,5,6,7,8,9};
+  int arr[10] = {-1, 1, 2, 3, 4, 5, 6, 7, 8, 9};
   f1(arr);
 }

src/goto-instrument/code_contracts.cpp

@@ -164,17 +164,18 @@ bool code_contractst::has_contract(const irep_idt fun_name)
 }
 
 void code_contractst::add_quantified_variable(
-  exprt expression, replace_symbolt &replace, irep_idt mode)
+  exprt expression,
+  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
 
   //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
-  if(expression.id()==ID_exists || expression.id()==ID_forall)
+  if(expression.id() == ID_exists || expression.id() == ID_forall)
   {
-
     //get quantified symbol
     exprt tuple = expression.operands().front();
     exprt quantified_variable = tuple.operands().front();
@@ -190,7 +191,8 @@ void code_contractst::add_quantified_variable(
       symbol_table);
 
     // add created fresh symbol to expression map
-    symbol_exprt q(quantified_symbol.get_identifier(), quantified_symbol.type());
+    symbol_exprt q(
+      quantified_symbol.get_identifier(), quantified_symbol.type());
     replace.insert(q, new_symbol.symbol_expr());
   }
 }
@@ -276,7 +278,7 @@ bool code_contractst::apply_function_contract(
   }
 
   // Add quantified variables in contracts to the symbol map
-  irep_idt mode =  symbol_table.lookup_ref(function).mode;
+  irep_idt mode = symbol_table.lookup_ref(function).mode;
   code_contractst::add_quantified_variable(ensures, replace, mode);
   code_contractst::add_quantified_variable(requires, replace, mode);
 
@@ -816,8 +818,10 @@ void code_contractst::add_contract_check(
   }
 
   // Add quantified variables in contracts to the symbol map
-  code_contractst::add_quantified_variable(ensures, replace, function_symbol.mode);
-  code_contractst::add_quantified_variable(requires, replace, function_symbol.mode);
+  code_contractst::add_quantified_variable(
+    ensures, replace, function_symbol.mode);
+  code_contractst::add_quantified_variable(
+    requires, replace, function_symbol.mode);
 
   // assume(requires)
   if(requires.is_not_nil())

src/goto-instrument/code_contracts.h

@@ -171,7 +171,7 @@ class code_contractst
   //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, 
+    exprt expression,
     replace_symbolt &replace,
     irep_idt mode);
 };