Skip to content

GitLab

Closed
Created by libguestfs@libguestfs

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.

Edited by libguestfs
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information