real path failed: cannot allocate memory

10 views
Skip to first unread message

Dinesh Kumar

unread,
Mar 16, 2020, 8:37:27 AM3/16/20
to CProver Support
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

unread,
Mar 16, 2020, 1:54:45 PM3/16/20
to cprover...@googlegroups.com
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


Reply all
Reply to author
Forward
0 new messages