forked from jwiesler/ips4o-verify
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathMakefile
58 lines (43 loc) · 2.66 KB
/
Makefile
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
KEY_JAR=tools/key-2.11.0-exe.jar
KEY_OVERFLOW_JAR=tools/key-2.11.0-o-exe.jar
CI_TOOL=tools/citool-1.4.0-mini.jar
checkCommand=java -Dlogback.configurationFile=./gradle/disablelogging.xml -Dkey.contractOrder="contract-order.txt" -cp "$(KEY_JAR):$(CI_TOOL)" de.uka.ilkd.key.CheckerKt --no-auto-mode --proof-path src/main/key
checkOverflowCommand=java -Dlogback.configurationFile=./gradle/disablelogging.xml -Dkey.contractOrder="contract-order.txt" -cp "$(KEY_OVERFLOW_JAR):$(CI_TOOL)" de.uka.ilkd.key.CheckerKt -v --no-auto-mode --proof-path src/main/key-overflow
default:
@echo Available targets:
@sed -n 's/^\([a-zA-Z_-]\+\):.*/ \1/p' Makefile
proofSettings:
mkdir -p $${HOME}/.key
cp proofIndependentSettings.props $${HOME}/.key
touch $${HOME}/.key/proof-settings.props
overflow-run: proofSettings
@echo Consider loading one of the following files:
@find -iname "project*.key"
java -Dkey.contractOrder="contract-order.txt" -jar $(KEY_OVERFLOW_JAR)
run: proofSettings
@echo Consider loading one of the following files:
@find -iname "project*.key"
java -Dkey.contractOrder="contract-order.txt" -jar $(KEY_JAR)
compile:
./gradlew compileJava
test:
./gradlew test
constr-src:
rm -rf src/main/java-constr
cp -r src/main/java src/main/java-constr
sed -i 's/no_state int bucketStart/int bucketStart/' src/main/java-constr/de/wiesler/BucketPointers.java
sed -i 's/no_state int bucketSize/int bucketSize/' src/main/java-constr/de/wiesler/BucketPointers.java
constr-overflow-src:
rm -rf src/main/java-constr-overflow
cp -r src/main/java src/main/java-constr-overflow
sed -i 's/no_state int bucketStart/int bucketStart/' src/main/java-constr-overflow/de/wiesler/BucketPointers.java
sed -i 's/no_state int bucketSize/int bucketSize/' src/main/java-constr-overflow/de/wiesler/BucketPointers.java
check: check-methods check-constructors check-overflow-methods check-overflow-constructors
check-methods: proofSettings
$(checkCommand) --forbid-contracts-file "contracts/ignore.txt" --forbid-contracts-file "contracts/constructors.txt" -s statistics-methods.json src/main/key/project.key
check-constructors: constr-src proofSettings
$(checkCommand) --contracts-file contracts/constructors.txt -s statistics-constructors.json src/main/key/project-constr.key
check-overflow-methods: proofSettings
$(checkOverflowCommand) --contracts-file "contracts/overflow.txt" --forbid-contracts-file "contracts/constructors.txt" -s statistics-overflow-methods.json src/main/key-overflow/project.key
check-overflow-constructors: constr-overflow-src proofSettings
$(checkOverflowCommand) --contracts-file "contracts/constructors.txt" -s statistics-overflow-constructors.json src/main/key-overflow/project-constr.key