real path failed: cannot allocate memory

[Dinesh Kumar]

Hi,

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.

Regards,

Dinesh Kumar Rajamani

[Martin Nyx Brain]

This is quite an unusual error. Is there anything strange about how
you have your file system set up? A large number of symlinks or the
like?

Could you try running with strace and ltrace and posting the relevant
parts of the output?

Cheers,
- Martin