Removes dead code

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Author: feliperodri

src/ansi-c/c_typecheck_base.cpp

@@ -724,28 +724,22 @@ void c_typecheck_baset::typecheck_declaration(
         // available
         auto &code_type = to_code_with_contract_type(new_symbol.type);
 
-        if(!as_const(code_type).requires().empty())
+        for(auto &requires : code_type.requires())
         {
-          for(auto &requires : code_type.requires())
-          {
-            typecheck_expr(requires);
-            implicit_typecast_bool(requires);
-            disallow_subexpr_by_id(
-              requires,
-              ID_old,
-              CPROVER_PREFIX "old is not allowed in preconditions.");
-            disallow_subexpr_by_id(
-              requires,
-              ID_loop_entry,
-              CPROVER_PREFIX "loop_entry is not allowed in preconditions.");
-          }
+          typecheck_expr(requires);
+          implicit_typecast_bool(requires);
+          disallow_subexpr_by_id(
+            requires,
+            ID_old,
+            CPROVER_PREFIX "old is not allowed in preconditions.");
+          disallow_subexpr_by_id(
+            requires,
+            ID_loop_entry,
+            CPROVER_PREFIX "loop_entry is not allowed in preconditions.");
         }
 
-        if(!as_const(code_type).assigns().empty())
-        {
-          for(auto &target : code_type.assigns())
-            typecheck_expr(target);
-        }
+        for(auto &target : code_type.assigns())
+          typecheck_expr(target);
 
         if(!as_const(code_type).ensures().empty())
         {

src/ansi-c/expr2c.cpp

@@ -577,22 +577,6 @@ std::string expr2ct::convert_rec(
         dest.resize(dest.size()-1);
     }
 
-    // contract, if any
-    for(auto &requires : to_code_with_contract_type(src).requires())
-    {
-      dest += " [[requires " + convert(requires) + "]]";
-    }
-
-    for(auto &assigns : to_code_with_contract_type(src).assigns())
-    {
-      dest += " [[assigns " + convert(assigns) + "]]";
-    }
-
-    for(auto &ensures : to_code_with_contract_type(src).ensures())
-    {
-      dest += " [[ensures " + convert(ensures) + "]]";
-    }
-
     return dest;
   }
   else if(src.id()==ID_vector)