Add travis and dockerfile #34
Conversation
|
|
||
| ## install required pacakges | ||
| USER root | ||
|
|
There was a problem hiding this comment.
apt remove --purge cmake
snap install cmake --classic
Add above lines here to update cmake to the latest one
verify-c-common.Dockerfile
Outdated
| WORKDIR /home/usea | ||
| RUN git clone https://github.com/yvizel/verify-c-common.git | ||
|
|
||
| ## clone trusty repository (takes a long time) |
verify-c-common.Dockerfile
Outdated
| RUN git clone https://github.com/awslabs/aws-c-common.git | ||
|
|
||
| WORKDIR /home/usea/verify-c-common/aws-c-common | ||
| RUN mkdir build && cd build && cmake -DCMAKE_EXPORT_COMPILE_COMMANDS=1 ../ |
There was a problem hiding this comment.
change cmake to
cmake -DCMAKE_EXPORT_COMPILE_COMMANDS=1 -DCMAKE_INSTALL_PREFIX=$(pwd)/run ../ -GNinja
verify-c-common.Dockerfile
Outdated
| RUN mkdir build && cd build && cmake -DCMAKE_EXPORT_COMPILE_COMMANDS=1 ../ | ||
|
|
||
| WORKDIR /home/usea/verify-c-common | ||
| RUN ln -sf aws-c-common/build/compile_commands.json . |
There was a problem hiding this comment.
remove above RUN. it is no longer necessary.
There was a problem hiding this comment.
are you referring to line 19 or 22?
|
|
||
| WORKDIR /home/usea/verify-c-common/aws-c-common | ||
| RUN mkdir build && cd build && cmake -DCMAKE_EXPORT_COMPILE_COMMANDS=1 ../ | ||
|
|
There was a problem hiding this comment.
need to build aws-c-common by adding to the above line
cmake --build . --target install
| - env: BUILD_TYPE=RelWithDebInfo | ||
| script: | ||
| - docker build -t verify-c-common -f verify-c-common.Dockerfile . | ||
| - docker run -t verify-c-common /bin/bash -c "cd build && ninja test" |
There was a problem hiding this comment.
once everything is working, (but maybe even now?), need to do runs with different options.
Currently, we have the following combinations:
- normal : which is what is run above
- cex : with --cex switch
- vacuity: with --vac switch
- normal with yices: --horn-bmc-solver=smt-y2
- cex with yices: --horn-bmc-solver=smt-y2
Some of these might time out, so we will need to exclude tests that time out. This can be done using ctest command and its flags.
As this gets complicated, it is best to package this in a script and then call the script from the docker container.
There was a problem hiding this comment.
to do this, would I just add ctest --cex (or whatever flag) in the travis file or would I need to change the cmake instructions in the dockerfile?
No description provided.