Opened 9 months ago

Closed 9 months ago

#108 closed defect (duplicate)

symbolic: __VERIFIER_nondet_(u)int() causes a memory leak

Reported by: Lukáš Zaoral Owned by:
Priority: major Milestone: 4.4
Component: DiOS Keywords:
Cc: kdudka@…, lzaoral@…

Description

Hi,
whenever the __VERIFIER_nondet_int() (or uint) function is used, Divine 4.4.2 reports a memory leak even though no heap memory allocation was performed in the code itself. Thanks.

Minimal reproducer:

extern int __VERIFIER_nondet_int();

int main(void)
{
    int a = __VERIFIER_nondet_int();
}

Report:

$ divine verify --symbolic --leakcheck exit symb_leak.c
compiling symb_leak.c
loading bitcode … DiOS … LART … RR … constants … done
booting … done
states per second: 133.333                                                        
state count: 2
mips: 0.48
symbolic: 1

error found: yes
error trace: |
  FAULT: leaked [marked* f25e480e 0]
  [0] FATAL: memory leak in userspace

active stack:
  - symbol: void __dios::FaultBase::handler<__dios::Context>(_VM_Fault, _VM_Frame*, void (*)())
    location: dios/sys/fault.hpp:119
  - symbol: _Exit
    location: dios/libc/stdlib/_Exit.c:14
  - symbol: exit
    location: dios/libc/stdlib/exit.c:6
  - symbol: __dios_start
    location: dios/libc/sys/start.cpp:110
a report was written to symb_leak.report

Change History (1)

comment:1 Changed 9 months ago by Henrich Lauko

Resolution: duplicate
Status: newclosed

This is a duplication of #10. Unfortunately symbolic values currently produce leak errors.

Note: See TracTickets for help on using tickets.