Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add travis and dockerfile #34

Open
wants to merge 6 commits into
base: master
Choose a base branch
from
Open

Add travis and dockerfile #34

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
ba17686
Add travis
emmyni Nov 5, 2020
e848a56
Update travis
emmyni Nov 8, 2020
14c8a19
Update dockerfile
emmyni Nov 10, 2020
c8f42c0
changes
emmyni Nov 10, 2020
986667f
Update
emmyni Nov 10, 2020
adcf73c
Add -y
emmyni Nov 10, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
25 changes: 25 additions & 0 deletions .travis.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
language: cpp
dist: trusty
os: linux
cache: apt
branches:
only:
- master2
matrix:
include:
- 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"
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

services:
- docker

install: true

notifications:
slack: seahornteam:NAUqZmZHFFviPH4ktQbJXgKu
email:
recipients:
- [email protected]
on_success: always
on_failure: always
29 changes: 29 additions & 0 deletions verify-c-common.Dockerfile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@

FROM seahorn/seahorn-llvm10:nightly

ENV SEAHORN=/home/usea/seahorn/bin/sea PATH="$PATH:/home/usea/seahorn/bin:/home/usea/bin"

## install required pacakges
USER root

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more. 

apt remove --purge cmake
snap install cmake --classic

Add above lines here to update cmake to the latest one

RUN apt remove -y --purge cmake
RUN snap install -y cmake --classic

## clone verify-c-common repository
USER usea
WORKDIR /home/usea
RUN git clone https://github.com/yvizel/verify-c-common.git

## clone verify-c-common repository
WORKDIR /home/usea/verify-c-common
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 -DCMAKE_INSTALL_PREFIX=$(pwd)/run ../ -GNinja && cmake --build . --target install

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

need to build aws-c-common by adding to the above line

cmake --build . --target install

WORKDIR /home/usea/verify-c-common

RUN mkdir build && cd build && cmake -DSEA_LINK=llvm-link-10 -DCMAKE_C_COMPILER=clang-10 -DCMAKE_CXX_COMPILER=clang++-10 -DSEAHORN_ROOT=/home/usea/seahorn ../ -GNinja && ninja

## set default user and wait for someone to login and start running verification tasks
USER usea