[Eva] Do not fail on recursive calls without specification.

Instead, emits an error but continues the analysis with the probably unsound
specification generated by the kernel.
Also prints the callstack when -eva-print-callstacks is enabled.