Loop Contracts Annotation for While-Loop

[qinheping]

This PR introduce the loop contracts annotation for while-loops using proc-macro. The A while loop of the form

#[kani::loop_invariant(inv)]
while guard {
   body
}

is annotated as

while guard{
   body    
   kani::kani_loop_invariant_begin_marker();
   let __kani_loop_invariant_: bool = #inv;
   kani::kani_loop_invariant_end_marker();
}

where the place holder functions kani_loop_invariant_begin and kani_loop_invariant_begin are used to help codegen correctly generate a statement expression for the loop contracts and annotate the loop contracts to the correct named-sub of the loop latch node.

Some minor fixes are applied in CBMC side to make sure the loop contracts work correctly. I will add tests when CBMC is updated.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.