Problem with cast form abstract int to abstract pointer.

[Henrich Lauko]

The following code (run with divine check --symbolic) fails with spurious FAULT: null pointer dereference: [global* 0 2 ddn]:

#include <assert.h>

unsigned long __VERIFIER_nondet_ulong( void );
void *foo() {
    return __VERIFIER_nondet_ulong();
}

int main() {
    _Bool b = foo();
    assert( !b );
}

error trace: |
  FAULT: null pointer dereference: [global* 0 2 ddn]
  [0] FATAL: memory error in userspace

active stack:
  - symbol: void __dios::Fault<__dios::Scheduler<__dios::MachineParams<__dios::MonitorManager<__dios::BaseContext> > > >::handler<__dios::fs::VFS<__dios::ProcessManager<__dios::Fault<__dios::Scheduler<__dios::MachineParams<__dios::MonitorManager<__dios::BaseContext> > > > > > >(_VM_Fault, _VM_Frame*, void (*)())
    location: /dios/include/dios/sys/fault.hpp:193
  - symbol: __sym_zext
    location: /dios/include/sys/lart.h:277
  - symbol: lart.sym.zext.i1.i8
    location: (unknown location)
  - symbol: main
    location: sym-bool.c:9
  - symbol: _start
    location: /dios/src/libc/sys/start.cpp:87

however, if the cast to pointer is removed, the result is OK:

#include <assert.h>

unsigned long __VERIFIER_nondet_ulong( void );
unsigned long foo() {
    return __VERIFIER_nondet_ulong();
}

int main() {     
    _Bool b = foo();
    assert( !b );
}

error trace: |
  ASSUME (= ((_ extract 0 0) (ite (not (= var_0 #x0000000000000000)) #x01 #x00)) #b1)
  (0) Assertion failed: !b, file sym-bool.c, line 10.
  [0] FATAL: assertion failure in userspace

[Henrich Lauko]

FIXED!