Fix the bug that assign clause cannot be inferred for the inner loop of nested loops (#4179)

This PR fixes the bug that assign clause cannot be inferred for the
inner loop of nested loops.

General ideas: For local variables of the outer loop, after the
loop-contracts transformation, if their StorageLive/StorageDead
statements are still inside the outer loop body, CBMC cannot infer the
assign clause for the inner loop if those variables are assigned inside
the inner loop's body. We have to move their StorageLive to the loop
head of the outer-loop and their StorageDead to the block right after
where the outer loop terminates. Together with the StorageLive, we have
to initiate the variables with the values they are initiated with inside
the outer loop's body. Note that we handle three ways how a variable is
initiated in MIR: by an assign statement following after a StorageLive
one, by a Terminator for function call, and by a group of five
statements which perform the `clone()` function.

Resolves #4159

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

Author: thanhnguyen-aws