LARA Inferring return values and path conditions for library functions Inferring return values and path conditions for library functions (report)