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

[Lukáš Zaoral]

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

[Henrich Lauko]

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