Generate more helpers for loop specifications

[anvacaru]

Generate more helpers for loop specifications:

• Extract from the solidity compiler the loop head points, and generated K macros which allow making more resilient specs.
• Generate specs automatically for loops in copying/encoding data (Solidity compiler generic loops).
• Generate spec templates for other loops, which then can have the actual invariant filled in manually.
• Annotate the Solidity with comments to name each loop, so we can easily refer to them in the loop invariant using some sugared syntax for each contract.

[palinatolmach]

As discussed with @ehildenb, we can generate macros for function entry/exit points, including those of internal functions, which can be useful for compositional symbolic execution (#130).