We had a bachelor's student look at Goblint's behavior on Juliet suite and he also created some simplified tests, which I committed here in 91d3513.

None of them pass for various reasons, but since #338 it would be possible to add CWE-specific warnings:

• Interval analysis only warns about signed overflow, since that's what SV-COMP wanted, but now we should also warn (with different tags) about unsigned overflow.
• We don't distinguish overflow from underflow, but CWE does. For precise warnings we should as well.
• Even if temporarily removing the isSigned check, we don't warn about char overflows. Probably because arithmetic with char is performed as int and then cast back. So overflow in cast should warn as well.
• dbg.print_dead_code prints some warnings about always true/false conditions, but they have the wrong location: they are printed at the first dead line in the branch body, not the if itself. I guess technically for Juliet suite it doesn't matter (?), but it would indeed make more sense to print it at the if since the warning contains the expression.
• Conditional expression evaluation sometimes is less precise than invariant. Dead branch warnings are printed based on the former, but in 50/08 nothing is printed despite the body being a dead node. Apparently it only becomes dead after refining using invariant. This is semi-intentional: invariant is more expensive than eval_rv (on base), so all of its logic maybe shouldn't be fallback for eval_rv.
• Always true condition warnings aren't printed when the if has no else branch or it is empty. Dead branch warnings are somehow tracked separately but also checked using dead lines (?). Since there's no dead node/line in the else branch, this is not detected, despite branch raising Deadcode.