Opened 2 weeks ago

#10 new defect

Memory leak from symbolic values.

Reported by: Henrich Lauko Owned by:
Priority: major Milestone:
Component: DiOS Keywords: sym, sv-comp
Cc:

Description

Problem with:

divine check --lart leak-check --symbolic ~/repo/sv-benchmarks/c/memsafety-ext3/freeAlloca_false-valid-free.c}}}

With patches from ~xstill/DIVINE/svc-2019, namely the leak-check patch. There is a spurious memory leak, probably related to --symbolic. A minimal example of the same error:
{{{
int __VERIFIER_nondet_int();

int main() {
    int x = __VERIFIER_nondet_int();
    int y = __VERIFIER_nondet_int();
    return 0;
}
}}}

As a sanity check, the previous minimal example with --lart svc-undef-nondet instead of --symbolic (this causes __VERIFIER_nondet_* to return undefined value) does not have any memory leaks.

Change History (0)

Note: See TracTickets for help on using tickets.