I am trying to use CBMC (5.11) in linux (Ubuntu 16.04) like the following and CBMC returns ' RUNTIME ERROR: realpath failed: cannot allocate memory'
cbmc --xml-ui --32 --drop-unused-functions --show-properties --unwinding-assertions --object-bits 12 --unwind 25 --no-assertions --function entryFor_simpleConfig_SimpleComputation --pointer-check --div-by-zero-check --unsigned-overflow-check --signed-overflow-check --conversion-check --float-overflow-check --bounds-check --nan-check --memory-leak-check file.c
I observed that realpath is a library function called from file_util.cpp to find the current working directory. But could not find why finding current working directory is resulting in 'cannot allocate memory'. Any small clue could be very useful for me.
Thank you very much in advance.
Dinesh Kumar Rajamani