Frama-C should exit with non-zero if proving failed
$ frama-c -wp -wp-rte snippets/range_size.c
[kernel] Parsing snippets/range_size.c (with preprocessing)
[rte] annotating function range_size
[wp] 4 goals scheduled
[wp] [Alt-Ergo 2.2.0] Goal typed_range_size_ensures : Timeout (Qed:2ms) (10s)
[wp] Proved goals: 3 / 4
Qed: 1 (0.50ms-0.78ms)
Alt-Ergo 2.2.0: 2 (13ms-15ms) (80) (interrupted: 1)
Proving failed, but frama-c still exits with a zero exit code:
$ echo $?
0
This problem makes it harder to use frama-c from automated CI systems.