diff options
| author | Denis Gavrielov <de.gavrielov@gmail.com> | 2019-06-17 16:04:36 +0100 |
|---|---|---|
| committer | MartinNowack <martin.nowack@gmail.com> | 2019-07-25 09:43:04 +0100 |
| commit | f75a6941eee820ebdeae14cc10c24ecd5ec04579 (patch) | |
| tree | 588e018a51c26ae72d4592fa4889c586a4d752a2 /Dockerfile | |
| parent | df33de1a47eaff1b191d22f482af5d26162e6aa9 (diff) | |
| download | klee-f75a6941eee820ebdeae14cc10c24ecd5ec04579.tar.gz | |
Solve issues with running as a command on docker run
Now commands like `docker run klee/klee klee --version` are possible.
Diffstat (limited to 'Dockerfile')
| -rw-r--r-- | Dockerfile | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Dockerfile b/Dockerfile index 97708b53..11185076 100644 --- a/Dockerfile +++ b/Dockerfile @@ -44,6 +44,7 @@ RUN apt update && apt -y --no-install-recommends install sudo && \ cp /etc/sudoers /etc/sudoers.bak && \ echo 'klee ALL=(root) NOPASSWD: ALL' >> /etc/sudoers +ENV PATH="$PATH:/tmp/llvm-60-install_O_D_A/bin:/home/klee/klee_build/bin" ENV BASE=/tmp # Copy across source files needed for build # Set klee user to be owner @@ -54,7 +55,7 @@ WORKDIR /home/klee ENV LD_LIBRARY_PATH /home/klee/klee_build/lib/ # Add KLEE binary directory to PATH -RUN /bin/bash -c 'ln -s ${BASE}/klee_src /home/klee/ && ln -s ${BASE}/klee_build* /home/klee/klee_build && echo "export PATH=\"$PATH:$(cd /tmp/llvm-*install*/bin && pwd):/home/klee/klee_build/bin\"" >> /home/klee/.bashrc' +RUN /bin/bash -c 'ln -s ${BASE}/klee_src /home/klee/ && ln -s ${BASE}/klee_build* /home/klee/klee_build' # TODO Remove when STP is fixed RUN /bin/bash -c 'echo "export LD_LIBRARY_PATH=$(cd ${BASE}/metaSMT-*-deps/stp-git-basic/lib/ && pwd):$LD_LIBRARY_PATH" >> /home/klee/.bashrc' |