Should the error message not also contain some human-readable information such as
Check that the input program compiles with GCC. If it does, the specification of the library function in Goblint is likely incorrect or incomplete. When appropriate, you could also try commenting out the offending call.?

The current error message is only helpful to Goblint developers (who are familiar with the library mechanism); such an error message would also give other users a way to bypass this message or understand what's happening.

Should the error message not also contain some human-readable information such as
Check that the input program compiles with GCC. If it does, the specification of the library function in Goblint is likely incorrect or incomplete. When appropriate, you could also try commenting out the offending call.?

I'm not sure we should make exception strings such spoon-feedy text. If we want to be consistent about it, we should change every CIL lexing/parsing/typing/merging/etc error to also to print it. #1564 clearly shows it.
Or should we suggest the user delete their code to avoid Goblint erroring on it?

such an error message would also give other users a way to bypass this message

Not really. The only they have to be Goblint developers to actually fix LibraryFunctions.

Maybe we can find some compromise between my extremely wordy suggestion and the extremely terse message we currently have and then move forward and merge this?