Refactoring to generate an f__pre(in) function for each procedure.
Refactoring to generate an f__pre(in) function for each procedure.

This allows us to easily check the input type conditions and
preconditions.
Also spread these definitions across more lines, for readability.
(basically, each conjunction starts on a new line).

Current results are mostly unchanged.

utting/whiley2boogie,utting/whiley2boogie,utting/whiley2boogie