javascript-semantics/verification/Makefile at es6 · https-github-com-goodman-ops/javascript-semantics · GitHub

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
59
60
61
62
63
64
65
66
67
SHELL=/bin/bash

.PHONY: all
all: build prove

.PHONY: build
build: clean
	kompile -d patterns/tree_string --no-prelude --backend java --main-module JS-VERIFIER --syntax-module JS-SYNTAX patterns/tree_string/js-verifier.k
	kompile -d patterns/tree_float  --no-prelude --backend java --main-module JS-VERIFIER --syntax-module JS-SYNTAX patterns/tree_float/js-verifier.k
	kompile -d patterns/list        --no-prelude --backend java --main-module JS-VERIFIER --syntax-module JS-SYNTAX patterns/list/js-verifier.k

.PHONY: list
list:
	@echo "List"
	krun -d patterns/list        --smt none          --prove list/head_spec.k          list/list.js
	krun -d patterns/list        --smt none          --prove list/tail_spec.k          list/list.js
	krun -d patterns/list        --smt none          --prove list/add_spec.k           list/list.js
	krun -d patterns/list        --smt none          --prove list/swap_spec.k          list/list.js
#	krun -d patterns/list        --smt none          --prove list/length_recursive_spec.k       list/list.js
#	krun -d patterns/list        --smt none          --prove list/length_iterative_spec.k       list/list.js
#	krun -d patterns/list        --smt none          --prove list/sum_recursive_spec.k          list/list.js
#	krun -d patterns/list        --smt none          --prove list/sum_iterative_spec.k          list/list.js
	krun -d patterns/list        --smt none          --prove list/reverse_spec.k       list/list.js
	krun -d patterns/list        --smt none          --prove list/append_spec.k        list/list.js
#	krun -d patterns/list        --smt none          --prove list/copy.k               list/list.js

.PHONY: list-smt
list-smt:
	@echo "List"
	krun -d patterns/list        --smt_prelude patterns/list/list.smt2          --prove list/head_spec.k          list/list.js
	krun -d patterns/list        --smt_prelude patterns/list/list.smt2          --prove list/tail_spec.k          list/list.js
	krun -d patterns/list        --smt_prelude patterns/list/list.smt2          --prove list/add_spec.k           list/list.js
	krun -d patterns/list        --smt_prelude patterns/list/list.smt2          --prove list/swap_spec.k          list/list.js
#	krun -d patterns/list        --smt_prelude patterns/list/list.smt2          --prove list/length_recursive_spec.k       list/list.js
#	krun -d patterns/list        --smt_prelude patterns/list/list.smt2          --prove list/length_iterative_spec.k       list/list.js
#	krun -d patterns/list        --smt_prelude patterns/list/list.smt2          --prove list/sum_recursive_spec.k          list/list.js
#	krun -d patterns/list        --smt_prelude patterns/list/list.smt2          --prove list/sum_iterative_spec.k          list/list.js
	krun -d patterns/list        --smt_prelude patterns/list/list.smt2          --prove list/reverse_spec.k       list/list.js
	krun -d patterns/list        --smt_prelude patterns/list/list.smt2          --prove list/append_spec.k        list/list.js
#	krun -d patterns/list        --smt_prelude patterns/list/list.smt2          --prove list/copy.k               list/list.js

.PHONY: prove
prove:
	@echo "List"
	krun -d patterns/list        --smt none                                     --prove list/reverse_spec.k       list/reverse.js
	krun -d patterns/list        --smt none                                     --prove list/append_spec.k        list/append.js
	@echo "BST String"
	krun -d patterns/tree_string --smt_prelude patterns/tree_string/string.smt2 --prove bst/string_find_spec.k    bst/find.js
	krun -d patterns/tree_string --smt_prelude patterns/tree_string/string.smt2 --prove bst/string_insert_spec.k  bst/insert.js
	krun -d patterns/tree_string --smt_prelude patterns/tree_string/string.smt2 --prove bst/string_delete_spec.k  bst/delete.js
	@echo "BST OOP String"
	krun -d patterns/tree_string --smt_prelude patterns/tree_string/string.smt2 --prove bst-oop/bst_find_spec.k   bst-oop/bst.js
	krun -d patterns/tree_string --smt_prelude patterns/tree_string/string.smt2 --prove bst-oop/bst_insert_spec.k bst-oop/bst.js
	@echo "BST Float"
	krun -d patterns/tree_float  --smt_prelude patterns/tree_float/float.smt2   --prove bst/float_find_spec.k     bst/find.js
	krun -d patterns/tree_float  --smt_prelude patterns/tree_float/float.smt2   --prove bst/float_insert_spec.k   bst/insert.js
	krun -d patterns/tree_float  --smt_prelude patterns/tree_float/float.smt2   --prove bst/float_delete_spec.k   bst/delete.js
	@echo "AVL String"
	krun -d patterns/tree_string --smt_prelude patterns/tree_string/string.smt2 --prove avl/avl_find_spec.k       avl/avl.js
	krun -d patterns/tree_string --smt_prelude patterns/tree_string/string.smt2 --prove avl/avl_insert_spec.k     avl/avl.js
	krun -d patterns/tree_string --smt_prelude patterns/tree_string/string.smt2 --prove avl/avl_delete_spec.k     avl/avl.js

.PHONY: clean
clean:
	rm -rf patterns/tree_string/js-verifier-kompiled
	rm -rf patterns/tree_float/js-verifier-kompiled
	rm -rf patterns/list/js-verifier-kompiled