double free not detected in SV-COMP 26 #1861
Description
A wrong verdict true in svcomp as observable by
./goblint --set ana.sv-comp.enabled true --set ana.sv-comp.functions true --set ana.path_sens[+] base --sets ana.specification /home/goblint/sv-benchmarks/c/properties/valid-memsafety.prp --sets exp.architecture 32bit /home/goblint/sv-benchmarks/c/ldv-memsafety/memleaks_test19-2.i --set ana.autotune.enabled false --set ana.malloc.unique_address_count 5
gives rise to the following snipped, simplified by @michael-schwarz
//PARAM: --set ana.activated[+] useAfterFree
#include <stdlib.h>
#include <stddef.h>
#include <stdio.h>
#include <string.h>
#include <wchar.h>
struct A19 {
int *p;
};
void init(struct A19 *a) {
a->p = (int *)malloc(sizeof(int));
free(a->p);
free(a->p); //WARN
}
void main(void) {
struct A19 a19;
a19.p = NULL;
init(&a19);
}Here, we miss the warning as marked in the code.