Enforce __CPROVER_loop_invariant contracts

Loop invariant annotations were being silently ignored when goto-instrument was
invoked with `--enforce-contracts` or `--enforce-contract`.
These flags now enforce both function and loop invariant contracts.

Author: SaswatPadhi

src/goto-instrument/code_contracts.cpp

@@ -933,6 +933,8 @@ bool code_contractst::enforce_contracts()
   {
     if(has_contract(goto_function.first))
       funs_to_enforce.insert(id2string(goto_function.first));
+    else
+      apply_loop_contract(goto_function.second);
   }
   return enforce_contracts(funs_to_enforce);
 }
@@ -943,14 +945,24 @@ bool code_contractst::enforce_contracts(
   bool fail = false;
   for(const auto &fun : funs_to_enforce)
   {
-    if(!has_contract(fun))
+    auto goto_function = goto_functions.function_map.find(fun);
+    if(goto_function == goto_functions.function_map.end())
     {
       fail = true;
       log.error() << "Could not find function '" << fun
                   << "' in goto-program; not enforcing contracts."
                   << messaget::eom;
       continue;
     }
+    apply_loop_contract(goto_function->second);
+
+    if(!has_contract(fun))
+    {
+      fail = true;
+      log.error() << "Could not find any contracts within function '" << fun
+                  << "'; nothing to enforce." << messaget::eom;
+      continue;
+    }
 
     if(!fail)
       fail = enforce_contract(fun);