I am new to goto-gcc. I try to use it to Compile the source files into a GOTO binary. I have file1.c:
#include <assert.h>
int multiply(int a, int b)
{
return a * b;
}
file2.c:
#include <assert.h>
extern int multiply(int a, int b);
void check_multiply()
{
int result = multiply(2, 3);
assert(result == 6);
}
Now i use the following command:
goto-cc file1.c file2.c -o allfiles
And i got : realpath failed: Invalid argument
I tried to use: strace goto-cc file1.c file2.c -o allfiles . and here are information i got:
execve("/usr/bin/goto-cc", ["goto-cc", "file1.c", "file2.c", "-o", "allfiles"], 0x7ffedb3c19e0 /* 40 vars */) = 0
brk(NULL) = 0x560da1462000
arch_prctl(0x3001 /* ARCH_??? */, 0x7ffed91fd230) = -1 EINVAL (Invalid argument)
mmap(NULL, 8192, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f1816c2c000
access("/etc/ld.so.preload", R_OK) = -1 ENOENT (No such file or directory)
openat(AT_FDCWD, "/etc/ld.so.cache", O_RDONLY|O_CLOEXEC) = 3
newfstatat(3, "", {st_mode=S_IFREG|0644, st_size=31963, ...}, AT_EMPTY_PATH) = 0
mmap(NULL, 31963, PROT_READ, MAP_PRIVATE, 3, 0) = 0x7f1816c24000
close(3) = 0
openat(AT_FDCWD, "/lib/x86_64-linux-gnu/libstdc++.so.6", O_RDONLY|O_CLOEXEC) = 3
read(3, "\177ELF\2\1\1\3\0\0\0\0\0\0\0\0\3\0>\0\1\0\0\0\0\0\0\0\0\0\0\0"..., 832) = 832
newfstatat(3, "", {st_mode=S_IFREG|0644, st_size=2252096, ...}, AT_EMPTY_PATH) = 0
mmap(NULL, 2267328, PROT_READ, MAP_PRIVATE|MAP_DENYWRITE, 3, 0) = 0x7f18169fa000
mmap(0x7f1816a94000, 1114112, PROT_READ|PROT_EXEC, MAP_PRIVATE|MAP_FIXED|MAP_DENYWRITE, 3, 0x9a000) = 0x7f1816a94000
mmap(0x7f1816ba4000, 454656, PROT_READ, MAP_PRIVATE|MAP_FIXED|MAP_DENYWRITE, 3, 0x1aa000) = 0x7f1816ba4000
mmap(0x7f1816c13000, 57344, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_FIXED|MAP_DENYWRITE, 3, 0x218000) = 0x7f1816c13000
mmap(0x7f1816c21000, 10432, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_FIXED|MAP_ANONYMOUS, -1, 0) = 0x7f1816c21000
close(3) = 0
openat(AT_FDCWD, "/lib/x86_64-linux-gnu/libgcc_s.so.1", O_RDONLY|O_CLOEXEC) = 3
read(3, "\177ELF\2\1\1\0\0\0\0\0\0\0\0\0\3\0>\0\1\0\0\0\0\0\0\0\0\0\0\0"..., 832) = 832
newfstatat(3, "", {st_mode=S_IFREG|0644, st_size=125488, ...}, AT_EMPTY_PATH) = 0
mmap(NULL, 127720, PROT_READ, MAP_PRIVATE|MAP_DENYWRITE, 3, 0) = 0x7f18169da000
mmap(0x7f18169dd000, 94208, PROT_READ|PROT_EXEC, MAP_PRIVATE|MAP_FIXED|MAP_DENYWRITE, 3, 0x3000) = 0x7f18169dd000
mmap(0x7f18169f4000, 16384, PROT_READ, MAP_PRIVATE|MAP_FIXED|MAP_DENYWRITE, 3, 0x1a000) = 0x7f18169f4000
mmap(0x7f18169f8000, 8192, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_FIXED|MAP_DENYWRITE, 3, 0x1d000) = 0x7f18169f8000
close(3) = 0
openat(AT_FDCWD, "/lib/x86_64-linux-gnu/libc.so.6", O_RDONLY|O_CLOEXEC) = 3
read(3, "\177ELF\2\1\1\3\0\0\0\0\0\0\0\0\3\0>\0\1\0\0\0P\237\2\0\0\0\0\0"..., 832) = 832
pread64(3, "\6\0\0\0\4\0\0\0@\0\0\0\0\0\0\0@\0\0\0\0\0\0\0@\0\0\0\0\0\0\0"..., 784, 64) = 784
pread64(3, "\4\0\0\0 \0\0\0\5\0\0\0GNU\0\2\0\0\300\4\0\0\0\3\0\0\0\0\0\0\0"..., 48, 848) = 48
pread64(3, "\4\0\0\0\24\0\0\0\3\0\0\0GNU\0i8\235HZ\227\223\333\350s\360\352,\223\340."..., 68, 896) = 68
newfstatat(3, "", {st_mode=S_IFREG|0644, st_size=2216304, ...}, AT_EMPTY_PATH) = 0
pread64(3, "\6\0\0\0\4\0\0\0@\0\0\0\0\0\0\0@\0\0\0\0\0\0\0@\0\0\0\0\0\0\0"..., 784, 64) = 784
mmap(NULL, 2260560, PROT_READ, MAP_PRIVATE|MAP_DENYWRITE, 3, 0) = 0x7f18167b2000
mmap(0x7f18167da000, 1658880, PROT_READ|PROT_EXEC, MAP_PRIVATE|MAP_FIXED|MAP_DENYWRITE, 3, 0x28000) = 0x7f18167da000
mmap(0x7f181696f000, 360448, PROT_READ, MAP_PRIVATE|MAP_FIXED|MAP_DENYWRITE, 3, 0x1bd000) = 0x7f181696f000
mmap(0x7f18169c7000, 24576, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_FIXED|MAP_DENYWRITE, 3, 0x214000) = 0x7f18169c7000
mmap(0x7f18169cd000, 52816, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_FIXED|MAP_ANONYMOUS, -1, 0) = 0x7f18169cd000
close(3) = 0
openat(AT_FDCWD, "/lib/x86_64-linux-gnu/libm.so.6", O_RDONLY|O_CLOEXEC) = 3
read(3, "\177ELF\2\1\1\3\0\0\0\0\0\0\0\0\3\0>\0\1\0\0\0\0\0\0\0\0\0\0\0"..., 832) = 832
newfstatat(3, "", {st_mode=S_IFREG|0644, st_size=940560, ...}, AT_EMPTY_PATH) = 0
mmap(NULL, 942344, PROT_READ, MAP_PRIVATE|MAP_DENYWRITE, 3, 0) = 0x7f18166cb000
mmap(0x7f18166d9000, 507904, PROT_READ|PROT_EXEC, MAP_PRIVATE|MAP_FIXED|MAP_DENYWRITE, 3, 0xe000) = 0x7f18166d9000
mmap(0x7f1816755000, 372736, PROT_READ, MAP_PRIVATE|MAP_FIXED|MAP_DENYWRITE, 3, 0x8a000) = 0x7f1816755000
mmap(0x7f18167b0000, 8192, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_FIXED|MAP_DENYWRITE, 3, 0xe4000) = 0x7f18167b0000
close(3) = 0
mmap(NULL, 8192, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f18166c9000
arch_prctl(ARCH_SET_FS, 0x7f18166ca3c0) = 0
set_tid_address(0x7f18166ca690) = 2370
set_robust_list(0x7f18166ca6a0, 24) = 0
rseq(0x7f18166cad60, 0x20, 0, 0x53053053) = 0
mprotect(0x7f18169c7000, 16384, PROT_READ) = 0
mprotect(0x7f18167b0000, 4096, PROT_READ) = 0
mprotect(0x7f18169f8000, 4096, PROT_READ) = 0
mmap(NULL, 8192, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7f18166c7000
mprotect(0x7f1816c13000, 45056, PROT_READ) = 0
mprotect(0x560da0b17000, 20480, PROT_READ) = 0
mprotect(0x7f1816c66000, 8192, PROT_READ) = 0
prlimit64(0, RLIMIT_STACK, NULL, {rlim_cur=8192*1024, rlim_max=RLIM64_INFINITY}) = 0
munmap(0x7f1816c24000, 31963) = 0
getrandom("\x70\xed\x7e\x45\x46\x5e\x17\x32", 8, GRND_NONBLOCK) = 8
brk(NULL) = 0x560da1462000
brk(0x560da1483000) = 0x560da1483000
futex(0x7f1816c2177c, FUTEX_WAKE_PRIVATE, 2147483647) = 0
brk(0x560da14a4000) = 0x560da14a4000
ioctl(1, TCGETS, {B38400 opost isig icanon echo ...}) = 0
brk(0x560da14c5000) = 0x560da14c5000
getpid() = 2370
openat(AT_FDCWD, "/tmp/goto-gcc.2370.MLxqk7.in", O_RDWR|O_CREAT|O_EXCL, 0600) = 3
close(3) = 0
getpid() = 2370
getrandom("\xcf\xb9\x2e\x3e\xff\xa6\xbf\xf1", 8, GRND_NONBLOCK) = 8
openat(AT_FDCWD, "/tmp/goto-gcc.2370.p671fN.out", O_RDWR|O_CREAT|O_EXCL, 0600) = 3
close(3) = 0
getpid() = 2370
openat(AT_FDCWD, "/tmp/goto-gcc.2370.2lzVHT.err", O_RDWR|O_CREAT|O_EXCL, 0600) = 3
close(3) = 0
openat(AT_FDCWD, "/tmp/goto-gcc.2370.MLxqk7.in", O_WRONLY|O_CREAT|O_TRUNC, 0666) = 3
write(3, "#if defined(__clang_major__)\ncla"..., 218) = 218
close(3) = 0
openat(AT_FDCWD, "/tmp/goto-gcc.2370.MLxqk7.in", O_RDONLY) = 3
openat(AT_FDCWD, "/tmp/goto-gcc.2370.p671fN.out", O_WRONLY|O_CREAT, 0600) = 4
openat(AT_FDCWD, "/tmp/goto-gcc.2370.2lzVHT.err", O_WRONLY|O_CREAT, 0600) = 5
rt_sigprocmask(SIG_SETMASK, [], [], 8) = 0
clone(child_stack=NULL, flags=CLONE_CHILD_CLEARTID|CLONE_CHILD_SETTID|SIGCHLD, child_tidptr=0x7f18166ca690) = 2371
rt_sigprocmask(SIG_SETMASK, [], NULL, 8) = 0
wait4(2371, [{WIFEXITED(s) && WEXITSTATUS(s) == 0}], 0, NULL) = 2371
--- SIGCHLD {si_signo=SIGCHLD, si_code=CLD_EXITED, si_pid=2371, si_uid=1000, si_status=0, si_utime=0, si_stime=0} ---
close(3) = 0
close(4) = 0
close(5) = 0
openat(AT_FDCWD, "/tmp/goto-gcc.2370.p671fN.out", O_RDONLY) = 3
read(3, "# 0 \"<stdin>\"\n# 0 \"<built-in>\"\n#"..., 8191) = 172
read(3, "", 8191) = 0
getpid() = 2370
openat(AT_FDCWD, "/tmp/goto-gcc.2370.yQJXjk.cpp", O_RDWR|O_CREAT|O_EXCL, 0600) = 4
close(4) = 0
getpid() = 2370
openat(AT_FDCWD, "/tmp/goto-gcc.2370.can4MZ.out", O_RDWR|O_CREAT|O_EXCL, 0600) = 4
close(4) = 0
getpid() = 2370
openat(AT_FDCWD, "/tmp/goto-gcc.2370.pATTYd.err", O_RDWR|O_CREAT|O_EXCL, 0600) = 4
close(4) = 0
openat(AT_FDCWD, "/tmp/goto-gcc.2370.yQJXjk.cpp", O_WRONLY|O_CREAT|O_TRUNC, 0666) = 4
write(4, "default_cxx_standard __cplusplus"..., 33) = 33
close(4) = 0
openat(AT_FDCWD, "/tmp/goto-gcc.2370.yQJXjk.cpp", O_RDONLY) = 4
openat(AT_FDCWD, "/tmp/goto-gcc.2370.can4MZ.out", O_WRONLY|O_CREAT, 0600) = 5
openat(AT_FDCWD, "/tmp/goto-gcc.2370.pATTYd.err", O_WRONLY|O_CREAT, 0600) = 6
rt_sigprocmask(SIG_SETMASK, [], [], 8) = 0
clone(child_stack=NULL, flags=CLONE_CHILD_CLEARTID|CLONE_CHILD_SETTID|SIGCHLD, child_tidptr=0x7f18166ca690) = 2373
rt_sigprocmask(SIG_SETMASK, [], NULL, 8) = 0
wait4(2373, [{WIFEXITED(s) && WEXITSTATUS(s) == 0}], 0, NULL) = 2373
--- SIGCHLD {si_signo=SIGCHLD, si_code=CLD_EXITED, si_pid=2373, si_uid=1000, si_status=0, si_utime=0, si_stime=0} ---
close(4) = 0
close(5) = 0
close(6) = 0
openat(AT_FDCWD, "/tmp/goto-gcc.2370.can4MZ.out", O_RDONLY) = 4
read(4, "# 0 \"<stdin>\"\n# 0 \"<built-in>\"\n#"..., 8191) = 157
read(4, "", 8191) = 0
close(4) = 0
unlink("/tmp/goto-gcc.2370.pATTYd.err") = 0
unlink("/tmp/goto-gcc.2370.can4MZ.out") = 0
unlink("/tmp/goto-gcc.2370.yQJXjk.cpp") = 0
close(3) = 0
unlink("/tmp/goto-gcc.2370.2lzVHT.err") = 0
unlink("/tmp/goto-gcc.2370.p671fN.out") = 0
unlink("/tmp/goto-gcc.2370.MLxqk7.in") = 0
getcwd("/home/mirage/Visualization-Tool-For-CBMC/src", 1024) = 45
mkdir("/tmp/goto-cc-UuxOvy", 0700) = 0
readlink("/tmp", 0x7ffed91fbf90, 1023) = -1 EINVAL (Invalid argument)
readlink("/tmp/goto-cc-UuxOvy", 0x7ffed91fbf90, 1023) = -1 EINVAL (Invalid argument)
futex(0x7f18169f9210, FUTEX_WAKE_PRIVATE, 2147483647) = 0
write(2, "realpath failed: Invalid argumen"..., 33realpath failed: Invalid argument) = 33
write(2, "\n", 1
) = 1
exit_group(70) = ?
+++ exited with 70 +++
Can anyone help me on this? Thanks in advance!