New ` IntDomain0.IncompatibleIKinds` exceptions

[michael-schwarz]

It seems one of the PRs merged last week has now caused new ikind mismatch issues:

./goblint --conf conf.json --sets ana.specification /home/goblint/sv-benchmarks/c/properties/valid-memsafety.prp --sets exp.architecture 32bit /home/goblint/sv-benchmarks/c/list-ext-properties/test-0214_1.i

Fatal error: exception IntDomain0.IncompatibleIKinds("ikinds int and unsigned int are incompatible. Values: (Unknown int([-31,31]),[-2147483648,2147483647],not {} ([-31,31])) and 0")

For a total of 6 new cases in ValidMemSafety:

• c/list-ext-properties/test-0214_1.yml
• c/list-ext-properties/test-0217_1.yml
• c/memsafety/test-0214.yml
• c/memsafety/test-0217.yml
• c/memsafety/test-0218.yml
• c/ntdrivers/kbfiltr.i.cil-1.yml

[michael-schwarz]

As this seems to only surface for the Memsafety property, my money would spontaneously be on #1676.

[michael-schwarz]

It seems to come from:

        (* Binary operations on offsets should not generate overflow warnings in SV-COMP *)
        let bytes_offset = GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () -> Idx.mul item_size_in_bytes x in

So, x seems to be of a different ikind then Cilfacade.ptrdiff_ikind ().

[michael-schwarz]

Minimized program:

extern void abort(void);
#include <assert.h>
void reach_error() { assert(0); }

#include <stdlib.h>
#include <string.h>

extern int __VERIFIER_nondet_int(void);

int i = 0;

typedef void *list_t[2];
typedef list_t *list_p;
typedef enum {
    LIST_BEG,
    LIST_END
} end_point_t;

typedef void *item_t[2];
typedef item_t *item_p;
typedef enum {
    ITEM_PREV,
    ITEM_NEXT
} direction_t;

typedef struct {
    item_t head;
    char text[0x100 + /* terminating zero */ 1];
} *user_item_p;


int main()
{
    static list_t link;
    user_item_p item = malloc(sizeof *item);

    direction_t link_field = ITEM_NEXT;
    item->head[link_field] = link;

    return 0;
}

[michael-schwarz]

Further reduction yields this program:

#include <stdlib.h>

typedef enum {
    ITEM_PREV,
    ITEM_NEXT
} direction_t;

struct s {
    int head[2];
};


int main()
{
    struct s* item = malloc(sizeof(struct s));
    direction_t link_field = ITEM_NEXT;
    item->head[link_field] = 0;
    return 0;
}