Dockerfile failed to build due to git error

[HALOCORE]

When running the following commands,

git clone git@github.com:tracer-x/TracerX.git
cd TracerX
docker build .

Docker image failed to build. The error message is as, elow:

Besides, may I ask are there any prebuild docker images available? Thanks!

[rasoolmaghareh]

@HALOCORE This issues seems to be related to minisat versioning. TracerX relies on an older version of minisat.

We have added a binary version on test-comp platform. Please let me know if you can use that or if you would like a separate binary version?

[HALOCORE]

Yes, I can run the binary version. Thanks!

[HALOCORE]

Hi, the TracerX from test-comp always produce this error: 'stddef.h' file not found. I tried to run TracerX in (1) Ubuntu 20.04 with clang 10 installed (2) the latest KLEE container. Both failed. Don't know how to fix this.

BTW, may I ask is it possible to provide a docker container for running TracerX? I didn't find the container for test-comp 2021.

klee@a22af6fb2779:~$ /mnt/tracerx/bin/tracerx /mnt/data/xxx.c
In file included from /mnt/data/xxx.c:1:
/usr/include/stdio.h:33:10: fatal error: 'stddef.h' file not found
#include <stddef.h>
         ^
1 error generated.
/mnt/tracerx/bin/../include/klee-test-comp.c:82:23: warning: implicitly declaring library function 'calloc' with type 'void *(unsigned long, unsigned long)'
  char* obj = (char*) calloc(1, size); 
                      ^
/mnt/tracerx/bin/../include/klee-test-comp.c:82:23: note: please include the header <stdlib.h> or explicitly provide a declaration for 'calloc'
1 warning generated.
/mnt/tracerx/bin/../llvm-3.4.2/llvm-link: /tmp/tmpehfqo08q/xxx.c.bc: error: Could not open input file: No such file or directory
/mnt/tracerx/bin/../llvm-3.4.2/llvm-link: error loading file '/tmp/tmpehfqo08q/xxx.c.bc'
KLEE: ERROR: error loading program '/tmp/tmpehfqo08q/xxx.c.bc': No such file or directory
klee@a22af6fb2779:~$ 

[rasoolmaghareh]

Can you please share with me the instructions that you are running? I will try to run it on my side on a freshly installed Ubuntu20.04 and see if I can produce the error on my side. Most probably the issue comes from a missing header file. We have been developing TracerX on Ubuntu 16 & 18 and probably that is the cause of the issue on Ubuntu 20.

[HALOCORE]

Command: tracerx/bin/tracerx ./test.c

tracerx obtained from https://gitlab.com/sosy-lab/test-comp/archives-2021/

The following test.c file including stdlib.h has error:

#include<stdlib.h>
int main() {
  int a;
  klee_make_symbolic(&a, sizeof(a), "a");
  return a > 0;
}

In file included from ./test.c:1:
/usr/include/stdlib.h:31:10: fatal error: 'stddef.h' file not found
#include <stddef.h>
...

The following test.c file has warning on calloc but no error:

//#include<stdlib.h>
int main() {
  int a;
  klee_make_symbolic(&a, sizeof(a), "a");
  return a > 0;
}

..../tracerx/bin/../include/klee-test-comp.c:82:23: warning: implicitly declaring library function 'calloc' with type 'void *(unsigned long, unsigned long)'
  char* obj = (char*) calloc(1, size); 
                      ^
..../tracerx/bin/../include/klee-test-comp.c:82:23: note: please include the header <stdlib.h> or explicitly provide a declaration for 'calloc'
1 warning generated.
KLEE: output directory is "..../tracerx/bin/../test-suite"
Using Z3 solver backend
KLEE: Memory cap NOT exceeded!

KLEE: done: Total reduced symbolic execution tree nodes = 1
KLEE: done: Total number of visited basic blocks = 1
...

[HALOCORE]

May I ask are there any updates on this? Are there docker images available for the tracerx obtained from https://gitlab.com/sosy-lab/test-comp/archives-2021/ ?

[rasoolmaghareh]

@HALOCORE sorry for the delay. I am overseas currently and it seems that gitlab does not provide service to the country that I am visiting. I have tried many ways to access the link above (https://gitlab.com/sosy-lab/test-comp/archives-2021/) and none of them worked. I have asked a friend for help in this matter. I will respond shortly.

[rasoolmaghareh]

@HALOCORE I have not got back to you for a long time. Let me know if you are still interested in running TracerX.

[HALOCORE]

Hi, eventually I used the VM to run it. Thanks!