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.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information