Generate warnings when generating code containing recursive functions or opaque/external functions

[sonmarcho]

It would be good to generate warnings (depending on the backend) when:

• generating recursive functions for a backend which doesn't support the fixed-point encoding, so that the user is aware that they may have to generate the files with options -use-fuel or -decreases-clauses
• when generating template files (for decreases clauses or external definitions), so that the user is aware they may need to manually provide models (something extra would be to check if there already exists the required files, and only print a warning if there is a diff in the generated template files)