added assumptions about the type of parameters and return values to the
boogie procedures.