# HG changeset patch # User anatofuz # Date 1568677703 -32400 # Node ID e49b52c098c7f7b26af94a9c4a640b8e19eeb4b5 # Parent 6ad6aeabe992315bb0cba0095bd22256631dd0f3 mounted the current directory diff -r 6ad6aeabe992 -r e49b52c098c7 Dockerfile --- a/Dockerfile Mon Sep 16 23:32:00 2019 +0900 +++ b/Dockerfile Tue Sep 17 08:48:23 2019 +0900 @@ -11,10 +11,7 @@ RUN git clone https://github.com/javapathfinder/jpf-core.git --single-branch java-8 RUN wget https://services.gradle.org/distributions/gradle-5.6.2-bin.zip && unzip -d bin/gradle gradle-5.6.2-bin.zip -RUN cd /java-8 && ../bin/gradle/gradle-5.6.2/bin/gradle buildJars && cd / - -COPY ./ThreadTest ./ThreadTest -RUN cd ThreadTest && ../bin/gradle/gradle-5.6.2/bin/gradle build +RUN cd /java-8 && ../bin/gradle/gradle-5.6.2/bin/gradle buildJars COPY ./entrypoint.sh ./entrypoint.sh ENTRYPOINT ["sh","entrypoint.sh"] diff -r 6ad6aeabe992 -r e49b52c098c7 README.md --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/README.md Tue Sep 17 08:48:23 2019 +0900 @@ -0,0 +1,53 @@ +# NAME + +Docker-JPF + +## SYNOPSIS + +``` +$ls +Dockerfile ThreadTest/ docker-compose.yml entrypoint.sh + +$docker-compose build # docker image build + +$docker-compose up # execute... +``` + +## WHAT's JPF? + +> An extensible software model checking framework for Java bytecode programs +> JPF is an extensible software analysis framework for Java bytecode. jpf-core is the basis for all JPF projects; you always need to install it. It contains the basic VM and model checking infrastructure, and can be used to check for concurrency defects like deadlocks, and unhandled exceptions like NullPointerExceptions and AssertionErrors. + +This Docker Image based on java-8 JavaPathFinder source code. +cf. https://github.com/javapathfinder/jpf-core/tree/java-8 + + +## BASIC USAGE + +1. First, Place the Gradle project you want to run in the same directory as this repository. + +``` +$ls +Dockerfile ThreadTest/ docker-compose.yml entrypoint.sh + ↑ This is target Gradle Project +``` + +2. Then edit `entrypoint.sh`. + +This DockerImage mounts the root repository directory to `/os_exercise`. +Therefore, please do `cd /os_exercise /hogeproject` first. + +Next, Please execute gradle build. +(Gradle is /bin/gradle/gradle-5.6.2/bin/gradle) + +Finally, write the command to be executed by jpf. +jpf is `/java-8/bin/jpf` + +3. `$docker-compose build` + +4. `$docker-compose up` + +## AUTHOR + +AnaTofuZ + diff -r 6ad6aeabe992 -r e49b52c098c7 docker-compose.yml --- a/docker-compose.yml Mon Sep 16 23:32:00 2019 +0900 +++ b/docker-compose.yml Tue Sep 17 08:48:23 2019 +0900 @@ -5,7 +5,7 @@ image: jpf-docker build: . volumes: - - ./ThreadTest:/app + - .:/os_exercise environment: USER: "${USER}" command: '/bin/bash' diff -r 6ad6aeabe992 -r e49b52c098c7 entrypoint.sh --- a/entrypoint.sh Mon Sep 16 23:32:00 2019 +0900 +++ b/entrypoint.sh Tue Sep 17 08:48:23 2019 +0900 @@ -1,11 +1,8 @@ #!/bin/sh -#ls ../java-8 -#cd ../java-8 -#./gradlew buildJars -cd /ThreadTest -ls build/classes/java/main/threadTest -#../java-8/bin/jpf +classpath=build/classes/java/main/threadTest.TestThread + export JPF_HOME=/java-8 -#../java-8/bin/jpf +classpath=. threadTest.TestThread -#../java-8/bin/jpf +classpath=. build/classes/java/main/threadTest.TestThread -../java-8/bin/jpf +classpath=build/classes/java/main threadTest.TestThread +cd /os_exercise/ThreadTest +/bin/gradle/gradle-5.6.2/bin/gradle build + +/java-8/bin/jpf +classpath=build/classes/java/main threadTest.TestThread +#/java-8/bin/jpf +classpath=build/classes/java/main jp.ac.uryukyu.ie.e1x57xx.Interleave