Opened 2 years ago

Last modified 21 months ago

#10 new defect

Memory leak from symbolic values.

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


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 (1)

comment:1 Changed 21 months ago by mornfall

Milestone: future5.0

Milestone renamed

Note: See TracTickets for help on using tickets.