set_interval_marked  456 src/alloc.c    static void set_interval_marked (INTERVAL);
set_interval_marked 1470 src/alloc.c      set_interval_marked (i);