AstraVer Toolset » Deductive Verification Tools for Linux Kernel

$ frama-c -av nlist_init.c

[kernel] Parsing nlist_init.c (with preprocessing)
In file included from nlist_init.c:1:
nlist.h:6: warning: "NULL" redefined
    6 | #define NULL ((void*) 0)
      | 
In file included from /home/work/.opam/astraver/share/frama-c/astraver/astraver_spec_prolog.h:33,
                 from <command-line>:
/usr/lib/gcc/x86_64-linux-gnu/9/include/stddef.h:395: note: this is the location of the previous definition
  395 | #define NULL ((void *)0)
      | 
/home/work/.opam/astraver/share/frama-c/astraver/astraver_spec_prolog.h:131: warning: "NULL" redefined
/tmp/ppannot718bab.c:390: note: this is the location of the previous definition
  390 | #define NULL ((void *)0)
      | 
[av] Starting AstraVer translation
[av] Warning: \separated is not supported by AstraVer. This predicate will be ignored
[av] Producing files for AstraVer in subdir nlist_init.c.av
[av] File nlist_init.c.av/nlist_init_c.jc written.
[av] File nlist_init.c.av/nlist_init_c.cloc written.
[av] Calling AstraVer tool in subdir nlist_init.c.av
FIXME: Warning: ignoring second declaration of function linked_n_starting_from_null_empty
FIXME: Warning: ignoring second declaration of function linked_n_all_elements_valid
FIXME: Warning: ignoring second declaration of function linked_n_first_valid
FIXME: Warning: ignoring second declaration of function linked_n_bounds
FIXME: Warning: ignoring second declaration of function linked_n_valid_range
FIXME: Warning: ignoring second declaration of function linked_n_next_of_all_indexes
FIXME: Warning: ignoring second declaration of function linked_n_before_last
FIXME: Warning: ignoring second declaration of function linked_n_split_segment
FIXME: Warning: ignoring second declaration of function linked_n_split_segment_direct
FIXME: Warning: ignoring second declaration of function linked_n_split_segment_right
FIXME: Warning: ignoring second declaration of function linked_n_split_segment_right_direct
FIXME: Warning: ignoring second declaration of function linked_n_merge_segment
FIXME: Warning: ignoring second declaration of function linked_n_merge_segment_right
FIXME: Warning: ignoring second declaration of function linked_n_all_elements
FIXME: Warning: ignoring second declaration of function index_of_not_in_subrange
FIXME: Warning: ignoring second declaration of function index_of_unexisting_item
FIXME: Warning: ignoring second declaration of function index_of_up_unexisting_item
FIXME: Warning: ignoring second declaration of function index_of_inter_existing_item
FIXME: Warning: ignoring second declaration of function index_of
FIXME: Warning: ignoring second declaration of function index_of_bounds_weak
FIXME: Warning: ignoring second declaration of function index_of_existing_item_weak
File "nlist_init_c.jc", line 694, characters 44-283: typing error: Unsupported range in term, sorry
[av] User Error: AstraVer subprocess failed:   astraver    -v       -locs nlist_init_c.cloc nlist_init_c.jc
[kernel] Plug-in av aborted: invalid user input.