Skip to content
This repository was archived by the owner on Oct 3, 2021. It is now read-only.

Commit 0a87f6c

Browse files
authored
Merge pull request #1180 from sosy-lab/java-format
Reformat Java sources and add CI for Java format
2 parents db15ea5 + 45a4141 commit 0a87f6c

File tree

670 files changed

+19952
-21006
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

670 files changed

+19952
-21006
lines changed

.gitlab-ci.yml

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -108,6 +108,15 @@ java:
108108
tags:
109109
- privileged
110110

111+
java-format:
112+
stage: checks
113+
image: openjdk:11
114+
script: "java/check-format.sh"
115+
cache:
116+
key: "$CI_JOB_NAME"
117+
paths:
118+
- "java/*.jar"
119+
111120
.build-docker:
112121
image:
113122
name: gcr.io/kaniko-project/executor:debug

.travis.yml

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -4,11 +4,12 @@ if: type = pull_request
44
language: c
55
env:
66
matrix:
7-
- NAME="Sanity checks" DOCKER_IMAGE=sanity-checks COMMAND="c/check.py"
8-
- NAME="Preprocessing consistency checks" DOCKER_IMAGE=preprocessing-consistency COMMAND="cd c; ./diff_ci.sh './compare.py --keep-going --skip-large --directory'"
9-
- NAME="gcc-5" DOCKER_IMAGE=gcc:5 COMMAND="gcc-5 -v --version; cd c; ./diff_ci.sh 'make -j2 CC=gcc-5 -C'"
10-
- NAME="clang-3.9" DOCKER_IMAGE=clang:3.9 COMMAND="clang-3.9 -v --version; cd c; ./diff_ci.sh 'make -j2 CC=clang-3.9 -C'"
11-
- NAME="java" DOCKER_IMAGE=java COMMAND="java/check-compile.sh"
7+
- NAME="Sanity checks" DOCKER_IMAGE=registry.gitlab.com/sosy-lab/software/sv-benchmarks/ci/sanity-checks COMMAND="c/check.py"
8+
- NAME="Preprocessing consistency checks" DOCKER_IMAGE=registry.gitlab.com/sosy-lab/software/sv-benchmarks/ci/preprocessing-consistency COMMAND="cd c; ./diff_ci.sh './compare.py --keep-going --skip-large --directory'"
9+
- NAME="gcc-5" DOCKER_IMAGE=registry.gitlab.com/sosy-lab/software/sv-benchmarks/ci/gcc:5 COMMAND="gcc-5 -v --version; cd c; ./diff_ci.sh 'make -j2 CC=gcc-5 -C'"
10+
- NAME="clang-3.9" DOCKER_IMAGE=registry.gitlab.com/sosy-lab/software/sv-benchmarks/ci/clang:3.9 COMMAND="clang-3.9 -v --version; cd c; ./diff_ci.sh 'make -j2 CC=clang-3.9 -C'"
11+
- NAME="java" DOCKER_IMAGE=registry.gitlab.com/sosy-lab/software/sv-benchmarks/ci/java COMMAND="java/check-compile.sh"
12+
- NAME="java-format" DOCKER_IMAGE=openjdk:11 COMMAND="java/check-format.sh"
1213

1314
# Hint to TravisCI that we want to use their container infrastructure
1415
sudo: required
@@ -20,7 +21,7 @@ git:
2021
depth: 3
2122

2223
before_install:
23-
- docker pull registry.gitlab.com/sosy-lab/software/sv-benchmarks/ci/${DOCKER_IMAGE}
24+
- docker pull ${DOCKER_IMAGE}
2425

2526
script:
26-
- docker run --privileged --tty --volume "$(pwd):$(pwd)" registry.gitlab.com/sosy-lab/software/sv-benchmarks/ci/${DOCKER_IMAGE} /bin/sh -c "cd $(pwd); ${COMMAND}"
27+
- docker run --privileged --tty --volume "$(pwd):$(pwd)" ${DOCKER_IMAGE} /bin/sh -c "cd $(pwd); ${COMMAND}"

java/MinePump/spec1-5_product1/Actions.java

Lines changed: 15 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -14,24 +14,25 @@ public class Actions {
1414
p = new MinePump(env);
1515
}
1616

17-
void waterRise() { env.waterRise(); }
17+
void waterRise() {
18+
env.waterRise();
19+
}
1820

19-
void methaneChange() { env.changeMethaneLevel(); }
21+
void methaneChange() {
22+
env.changeMethaneLevel();
23+
}
2024

2125
void stopSystem() {
22-
if (p.isSystemActive())
23-
p.stopSystem();
26+
if (p.isSystemActive()) p.stopSystem();
2427
}
2528

2629
void startSystem() {
27-
if (!p.isSystemActive())
28-
p.startSystem();
30+
if (!p.isSystemActive()) p.startSystem();
2931
}
3032

3133
void timeShift() {
3234

33-
if (p.isSystemActive())
34-
Specification5_1();
35+
if (p.isSystemActive()) Specification5_1();
3536

3637
p.timeShift();
3738

@@ -44,7 +45,9 @@ void timeShift() {
4445
}
4546
}
4647

47-
String getSystemState() { return p.toString(); }
48+
String getSystemState() {
49+
return p.toString();
50+
}
4851

4952
// Specification 1 methan is Critical and pumping leads to Error
5053
void Specification1() {
@@ -109,7 +112,9 @@ void Specification4() {
109112

110113
// Specification 5: The Pump is never switched on when the water is below the
111114
// highWater sensor.
112-
void Specification5_1() { switchedOnBeforeTS = p.isPumpRunning(); }
115+
void Specification5_1() {
116+
switchedOnBeforeTS = p.isPumpRunning();
117+
}
113118

114119
// Specification 5: The Pump is never switched on when the water is below the
115120
// highWater sensor.

java/MinePump/spec1-5_product1/Main.java

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,16 @@
1-
import MinePumpSystem.Environment;
2-
import MinePumpSystem.MinePump;
31
import org.sosy_lab.sv_benchmarks.Verifier;
42

53
public class Main {
64

75
private static int cleanupTimeShifts = 2;
86

9-
public static void main(String[] args) { randomSequenceOfActions(3); }
7+
public static void main(String[] args) {
8+
randomSequenceOfActions(3);
9+
}
1010

11-
public static boolean getBoolean() { return Verifier.nondetBoolean(); }
11+
public static boolean getBoolean() {
12+
return Verifier.nondetBoolean();
13+
}
1214

1315
public static void randomSequenceOfActions(int maxLength) {
1416
Actions a = new Actions();
@@ -21,8 +23,7 @@ public static void randomSequenceOfActions(int maxLength) {
2123
boolean action2 = getBoolean();
2224
boolean action3 = getBoolean();
2325
boolean action4 = false;
24-
if (!action3)
25-
action4 = getBoolean();
26+
if (!action3) action4 = getBoolean();
2627

2728
if (action1) {
2829
a.waterRise();

java/MinePump/spec1-5_product1/MinePumpSystem/Environment.java

Lines changed: 24 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,11 @@
22

33
public class Environment {
44

5-
public enum WaterLevelEnum { low, normal, high }
5+
public enum WaterLevelEnum {
6+
low,
7+
normal,
8+
high
9+
}
610

711
// private WaterLevelEnum waterLevel = WaterLevelEnum.normal;
812

@@ -12,37 +16,40 @@ public enum WaterLevelEnum { low, normal, high }
1216

1317
void lowerWaterLevel() {
1418
switch (waterLevel) {
15-
case high:
16-
waterLevel = WaterLevelEnum.normal;
17-
break;
18-
case normal:
19-
waterLevel = WaterLevelEnum.low;
20-
break;
19+
case high:
20+
waterLevel = WaterLevelEnum.normal;
21+
break;
22+
case normal:
23+
waterLevel = WaterLevelEnum.low;
24+
break;
2125
}
2226
}
2327

2428
public void waterRise() {
2529
switch (waterLevel) {
26-
case low:
27-
waterLevel = WaterLevelEnum.normal;
28-
break;
29-
case normal:
30-
waterLevel = WaterLevelEnum.high;
31-
break;
30+
case low:
31+
waterLevel = WaterLevelEnum.normal;
32+
break;
33+
case normal:
34+
waterLevel = WaterLevelEnum.high;
35+
break;
3236
}
3337
}
3438

3539
public void changeMethaneLevel() {
3640
methaneLevelCritical = !methaneLevelCritical;
3741
}
3842

39-
public boolean isMethaneLevelCritical() { return methaneLevelCritical; }
43+
public boolean isMethaneLevelCritical() {
44+
return methaneLevelCritical;
45+
}
4046

4147
@Override
4248
public String toString() {
43-
return "Env(Water:" + waterLevel + ",Meth:" +
44-
(methaneLevelCritical ? "CRIT" : "OK") + ")";
49+
return "Env(Water:" + waterLevel + ",Meth:" + (methaneLevelCritical ? "CRIT" : "OK") + ")";
4550
}
4651

47-
public WaterLevelEnum getWaterLevel() { return waterLevel; }
52+
public WaterLevelEnum getWaterLevel() {
53+
return waterLevel;
54+
}
4855
}
Lines changed: 26 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,5 @@
11
package MinePumpSystem;
22

3-
import MinePumpSystem.Environment;
4-
53
public class MinePump {
64

75
boolean pumpRunning = false;
@@ -16,29 +14,41 @@ public MinePump(Environment env) {
1614
}
1715

1816
public void timeShift() {
19-
if (pumpRunning)
20-
env.lowerWaterLevel();
21-
if (systemActive)
22-
processEnvironment();
17+
if (pumpRunning) env.lowerWaterLevel();
18+
if (systemActive) processEnvironment();
2319
}
2420

2521
void processEnvironment() {}
2622

27-
void activatePump() { pumpRunning = true; }
23+
void activatePump() {
24+
pumpRunning = true;
25+
}
2826

29-
public boolean isPumpRunning() { return pumpRunning; }
27+
public boolean isPumpRunning() {
28+
return pumpRunning;
29+
}
3030

31-
void deactivatePump() { pumpRunning = false; }
31+
void deactivatePump() {
32+
pumpRunning = false;
33+
}
3234

33-
boolean isMethaneAlarm() { return env.isMethaneLevelCritical(); }
35+
boolean isMethaneAlarm() {
36+
return env.isMethaneLevelCritical();
37+
}
3438

3539
@Override
3640
public String toString() {
37-
return "Pump(System:" + (systemActive ? "On" : "Off") + ",Pump:" +
38-
(pumpRunning ? "On" : "Off") + ") " + env.toString();
41+
return "Pump(System:"
42+
+ (systemActive ? "On" : "Off")
43+
+ ",Pump:"
44+
+ (pumpRunning ? "On" : "Off")
45+
+ ") "
46+
+ env.toString();
3947
}
4048

41-
public Environment getEnv() { return env; }
49+
public Environment getEnv() {
50+
return env;
51+
}
4252

4353
public void stopSystem() {
4454
// feature not present
@@ -48,5 +58,7 @@ public void startSystem() {
4858
// feature not present
4959
}
5060

51-
public boolean isSystemActive() { return systemActive; }
61+
public boolean isSystemActive() {
62+
return systemActive;
63+
}
5264
}

java/MinePump/spec1-5_product10/Actions.java

Lines changed: 15 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -14,24 +14,25 @@ public class Actions {
1414
p = new MinePump(env);
1515
}
1616

17-
void waterRise() { env.waterRise(); }
17+
void waterRise() {
18+
env.waterRise();
19+
}
1820

19-
void methaneChange() { env.changeMethaneLevel(); }
21+
void methaneChange() {
22+
env.changeMethaneLevel();
23+
}
2024

2125
void stopSystem() {
22-
if (p.isSystemActive())
23-
p.stopSystem();
26+
if (p.isSystemActive()) p.stopSystem();
2427
}
2528

2629
void startSystem() {
27-
if (!p.isSystemActive())
28-
p.startSystem();
30+
if (!p.isSystemActive()) p.startSystem();
2931
}
3032

3133
void timeShift() {
3234

33-
if (p.isSystemActive())
34-
Specification5_1();
35+
if (p.isSystemActive()) Specification5_1();
3536

3637
p.timeShift();
3738

@@ -44,7 +45,9 @@ void timeShift() {
4445
}
4546
}
4647

47-
String getSystemState() { return p.toString(); }
48+
String getSystemState() {
49+
return p.toString();
50+
}
4851

4952
// Specification 1 methan is Critical and pumping leads to Error
5053
void Specification1() {
@@ -109,7 +112,9 @@ void Specification4() {
109112

110113
// Specification 5: The Pump is never switched on when the water is below the
111114
// highWater sensor.
112-
void Specification5_1() { switchedOnBeforeTS = p.isPumpRunning(); }
115+
void Specification5_1() {
116+
switchedOnBeforeTS = p.isPumpRunning();
117+
}
113118

114119
// Specification 5: The Pump is never switched on when the water is below the
115120
// highWater sensor.

java/MinePump/spec1-5_product10/Main.java

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,16 @@
1-
import MinePumpSystem.Environment;
2-
import MinePumpSystem.MinePump;
31
import org.sosy_lab.sv_benchmarks.Verifier;
42

53
public class Main {
64

75
private static int cleanupTimeShifts = 2;
86

9-
public static void main(String[] args) { randomSequenceOfActions(3); }
7+
public static void main(String[] args) {
8+
randomSequenceOfActions(3);
9+
}
1010

11-
public static boolean getBoolean() { return Verifier.nondetBoolean(); }
11+
public static boolean getBoolean() {
12+
return Verifier.nondetBoolean();
13+
}
1214

1315
public static void randomSequenceOfActions(int maxLength) {
1416
Actions a = new Actions();
@@ -21,8 +23,7 @@ public static void randomSequenceOfActions(int maxLength) {
2123
boolean action2 = getBoolean();
2224
boolean action3 = getBoolean();
2325
boolean action4 = false;
24-
if (!action3)
25-
action4 = getBoolean();
26+
if (!action3) action4 = getBoolean();
2627

2728
if (action1) {
2829
a.waterRise();

0 commit comments

Comments
 (0)