On top of #1234 with path-sensitive MemLeak analysis, the generation of witnesses fails with an error message
Fatal error: exception Failure("Node.move_opt: ambiguous moved index")
The reduced program (with a manual config e.g. without autotuning and loop unrolling (so unrelated to #1225)) is the following:
//PARAM: --enable witness.graphml.enabled --enable ana.sv-comp.functions --enable ana.sv-comp.enabled --sets ana.specification /home/michael/Documents/sv-comp/sv-benchmarks/c/properties/valid-memsafety.prp --sets ana.activated[+] "memLeak" --set ana.malloc.unique_address_count 1
struct _twoIntsStruct {
int intOne ;
int intTwo ;
};
typedef struct _twoIntsStruct twoIntsStruct;
void printStructLine(twoIntsStruct const *structTwoIntsStruct)
{
return;
}
int main(int argc, char **argv)
{
twoIntsStruct *data;
int tmp_1;
if (tmp_1 != 0) {
twoIntsStruct *dataBuffer = malloc(800UL);
data = dataBuffer;
}
else {
twoIntsStruct *dataBuffer_0 = malloc(800UL);
data = dataBuffer_0;
}
printStructLine((twoIntsStruct const *)data);
free((void *)data);
return;
}The problem seems to be related to the call of printStructLine, so I started wondering if the issue has to do with path-sensitivity...
We should probably aim to fix this or at least return trivial witnesses in such cases to still get points if fixing is out-of-reach.
On top of #1234 with path-sensitive MemLeak analysis, the generation of witnesses fails with an error message
The reduced program (with a manual config e.g. without autotuning and loop unrolling (so unrelated to #1225)) is the following:
The problem seems to be related to the call of
printStructLine, so I started wondering if the issue has to do with path-sensitivity...We should probably aim to fix this or at least return trivial witnesses in such cases to still get points if fixing is out-of-reach.