Merge remote-tracking branch 'origin/master' into koo/ex5

.gitignore

@@ -28,7 +28,7 @@ fixcalc.*.inp$
 /*.log$
 /*.mli$
 /bench/
-/*.out$
+**.out
 /old/
 /*.orig$
 /*.output$
@@ -46,4 +46,4 @@ cil/doc/header.html$
 cil/doc/index.html$
 cil/bin/CilConfig.pm$
 /mona.failure
-
+mona-1.4/

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "dependencies"]
+	path = dependencies
+	url = https://github.com/hipsleek/dependencies.git

.merlin

@@ -6,7 +6,7 @@ S cil/
 B _build/**/*
 
 # Dependencies
-PKG extlib batteries ocamlgraph camlp4 camlp4.lib xml-light
+PKG extlib fileutils batteries ocamlgraph ocamlformat camlp4 camlp4.lib xml-light
 
 # Extra flags
 FLG -debug locate,/tmp/merlin-debug

.ocamlformat

@@ -0,0 +1,5 @@
+version=0.14.2
+
+# to enable a whole directory, put "disable=false" in dir/.ocamlformat
+# to enable specific files put them in .ocamlformat-enable
+disable=true

.travis.yml

@@ -0,0 +1,25 @@
+os: linux
+dist: trusty
+language: ruby
+cache:
+  directories:
+    - ~/.opam
+env:
+  - HIPSLEEK_TESTS_START=0 HIPSLEEK_TESTS_END=4 PATH="$PATH:$TRAVIS_BUILD_DIR/dependencies:/usr/local/etc/reduce/bin" CACHE_NAME=hipsleek
+  - HIPSLEEK_TESTS_START=5 HIPSLEEK_TESTS_END=5 PATH="$PATH:$TRAVIS_BUILD_DIR/dependencies:/usr/local/etc/reduce/bin" CACHE_NAME=hipsleek
+  - HIPSLEEK_TESTS_START=6 HIPSLEEK_TESTS_END=6 PATH="$PATH:$TRAVIS_BUILD_DIR/dependencies:/usr/local/etc/reduce/bin" CACHE_NAME=hipsleek
+  - HIPSLEEK_TESTS_START=7 HIPSLEEK_TESTS_END=19 PATH="$PATH:$TRAVIS_BUILD_DIR/dependencies:/usr/local/etc/reduce/bin" CACHE_NAME=hipsleek
+  - HIPSLEEK_TESTS_START=20 HIPSLEEK_TESTS_END=39 PATH="$PATH:$TRAVIS_BUILD_DIR/dependencies:/usr/local/etc/reduce/bin" CACHE_NAME=hipsleek
+  - HIPSLEEK_TESTS_START=40 HIPSLEEK_TESTS_END=40 PATH="$PATH:$TRAVIS_BUILD_DIR/dependencies:/usr/local/etc/reduce/bin" CACHE_NAME=hipsleek
+  - HIPSLEEK_TESTS_START=41 HIPSLEEK_TESTS_END=41 PATH="$PATH:$TRAVIS_BUILD_DIR/dependencies:/usr/local/etc/reduce/bin" CACHE_NAME=hipsleek
+  - HIPSLEEK_TESTS_START=42 HIPSLEEK_TESTS_END=42 PATH="$PATH:$TRAVIS_BUILD_DIR/dependencies:/usr/local/etc/reduce/bin" CACHE_NAME=hipsleek
+  - HIPSLEEK_TESTS_START=43 HIPSLEEK_TESTS_END=43 PATH="$PATH:$TRAVIS_BUILD_DIR/dependencies:/usr/local/etc/reduce/bin" CACHE_NAME=hipsleek
+  - HIPSLEEK_TESTS_START=44 HIPSLEEK_TESTS_END=44 PATH="$PATH:$TRAVIS_BUILD_DIR/dependencies:/usr/local/etc/reduce/bin" CACHE_NAME=hipsleek
+  - HIPSLEEK_TESTS_START=45 HIPSLEEK_TESTS_END=50 PATH="$PATH:$TRAVIS_BUILD_DIR/dependencies:/usr/local/etc/reduce/bin" CACHE_NAME=hipsleek
+  - HIPSLEEK_TESTS_START=50 HIPSLEEK_TESTS_END=119 PATH="$PATH:$TRAVIS_BUILD_DIR/dependencies:/usr/local/etc/reduce/bin" CACHE_NAME=hipsleek
+before_install:
+  - ./.travis/before_install
+install:
+  - ./.travis/install
+script:
+  - ./.travis/script

.travis/before_install

@@ -0,0 +1,13 @@
+#!/bin/bash
+set -ev
+yes "" | sudo add-apt-repository ppa:avsm/ppa
+sudo apt-get update
+sudo apt-get -y install ed opam cpanminus
+ed dependencies/reduce/scripts/run.sh <<'EOF'
+10i
+exec $here/../cslbuild/x86_64-unknown-ubuntu12.04/csl/$ap $*
+exit 0
+.
+w
+q
+EOF

.travis/install

@@ -0,0 +1,11 @@
+#!/bin/bash
+set -ev
+yes "" | opam init --compiler=4.07.0
+eval $(opam env)
+sudo mkdir -p /usr/local/etc
+sudo cp -r dependencies/new_mona /usr/local
+sudo cp -r dependencies/reduce /usr/local/etc
+ln -s /usr/local/new_mona/bin/mona dependencies/mona_inter
+OPAMYES=true rake dependencies:install
+rake
+sudo cpanm File::NCopy Spreadsheet::WriteExcel Spreadsheet::ParseExcel

.travis/run-fast-tests.hip.0-4

@@ -0,0 +1,12 @@
+Starting sleek-hip tests:
+Starting hip tests:
+Checking eps.ss
+Checking append.ss
+Checking append-tail.ss
+Checking avl-bind.ss
+Checking avl.ss
+All test results were as expected.
+Total verification time: 620.17 second
+	Time spent in main process: 345.71 second
+	Time spent in child processes: 274.46 second
+	Number of false contexts: 23

.travis/run-fast-tests.hip.20-39

@@ -0,0 +1,27 @@
+Starting sleek-hip tests:
+Starting hip tests:
+Checking trees.ss
+Checking rb.ss
+Checking global1.ss
+Checking global2.ss
+Checking global3.ss
+Checking global4.ss
+Checking global5.ss
+Checking global-ll.ss
+Checking global-mutual-rec.ss
+Checking classic/classic1.ss
+Checking classic/classic1.ss (runs with extra options: --classic)
+Checking classic/classic1a.ss
+Checking classic/classic1a.ss (runs with extra options: --classic)
+Checking classic/classic2.ss
+Checking classic/classic2a.ss
+Checking classic/classic3.ss
+Checking classic/classic3a.ss
+Checking ../../modular_examples/dll-modular.ss (runs with extra options: --overeps)
+Checking ../../modular_examples/selection-modular.ss (runs with extra options: --overeps --lda)
+Checking ../../modular_examples/qsort-modular.ss (runs with extra options: --overeps --lda)
+All test results were as expected.
+Total verification time: 510.01 second
+	Time spent in main process: 407.62 second
+	Time spent in child processes: 102.39 second
+	Number of false contexts: 327

.travis/run-fast-tests.hip.40-40

@@ -0,0 +1,8 @@
+Starting sleek-hip tests:
+Starting hip tests:
+Checking vperm/ho_vperm_check.ss (runs with extra options: --ann-vp)
+All test results were as expected.
+Total verification time: 1.08 second
+	Time spent in main process: 1.00 second
+	Time spent in child processes: 0.07 second
+	Number of false contexts: 0

.travis/run-fast-tests.hip.41-41

@@ -0,0 +1,11 @@
+Starting sleek-hip tests:
+Starting hip tests:
+Checking vperm/task_decompose.ss (runs with extra options: --ann-vp)
+error at: vperm/task_decompose.ss inc
+Total number of errors: 1 in files:
+ error at: vperm/task_decompose.ss inc
+.
+Total verification time: 0.86 second
+	Time spent in main process: 0.80 second
+	Time spent in child processes: 0.06 second
+	Number of false contexts: 0

.travis/run-fast-tests.hip.42-42

@@ -0,0 +1,11 @@
+Starting sleek-hip tests:
+Starting hip tests:
+Checking parahip/cell.ss (runs with extra options: --en-para -tp parahip --en-lsmu-infer --en-thrd-and-conj)
+error at: parahip/cell.ss test
+Total number of errors: 1 in files:
+ error at: parahip/cell.ss test
+.
+Total verification time: 1196.81 second
+	Time spent in main process: 1.76 second
+	Time spent in child processes: 1195.06 second
+	Number of false contexts: 0

.travis/run-fast-tests.hip.43-43

@@ -0,0 +1,8 @@
+Starting sleek-hip tests:
+Starting hip tests:
+Checking parahip/cell-extreme-cases.ss (runs with extra options: --en-para -tp parahip --en-lsmu-infer --en-thrd-and-conj)
+All test results were as expected.
+Total verification time: 468.70 second
+	Time spent in main process: 1.02 second
+	Time spent in child processes: 467.68 second
+	Number of false contexts: 0

.travis/run-fast-tests.hip.44-44

@@ -0,0 +1,13 @@
+Starting sleek-hip tests:
+Starting hip tests:
+Checking parahip/ordered-locking.ss (runs with extra options: --en-para -tp parahip --en-lsmu-infer --en-thrd-and-conj)
+error at: parahip/ordered-locking.ss func
+error at: parahip/ordered-locking.ss main
+Total number of errors: 2 in files:
+ error at: parahip/ordered-locking.ss func
+error at: parahip/ordered-locking.ss main
+.
+Total verification time: 439.78 second
+	Time spent in main process: 0.83 second
+	Time spent in child processes: 438.96 second
+	Number of false contexts: 0

.travis/run-fast-tests.hip.45-50

@@ -0,0 +1,38 @@
+Starting sleek-hip tests:
+Starting hip tests:
+Checking parahip/unordered-locking.ss (runs with extra options: --en-para -tp parahip --en-lsmu-infer --en-thrd-and-conj)
+error at: parahip/unordered-locking.ss main
+Checking veribsync/hip-bperm1.ss (runs with extra options: --en-para -perm bperm -tp redlog)
+error at: veribsync/hip-bperm1.ss readCell
+error at: veribsync/hip-bperm1.ss updateCell
+Checking veribsync/barrier-static-consistency.ss (runs with extra options: --en-para -perm bperm -tp redlog)
+error at: veribsync/barrier-static-consistency.ss main_fail
+Checking veribsync/barrier-dynamic-exp3.ss (runs with extra options: --en-para -perm bperm -tp redlog)
+Checking veribsync/barrier-dynamic-exp4.ss (runs with extra options: --en-para -perm bperm -tp redlog)
+Checking conchip/mapreduce.ss (runs with extra options: -tp parahip --classic)
+error at: conchip/mapreduce.ss count_helper
+error at: conchip/mapreduce.ss countList
+error at: conchip/mapreduce.ss destroyList
+error at: conchip/mapreduce.ss main
+error at: conchip/mapreduce.ss mapper_helper
+error at: conchip/mapreduce.ss mapper
+error at: conchip/mapreduce.ss reducer1
+error at: conchip/mapreduce.ss reducer2
+Total number of errors: 12 in files:
+ error at: parahip/unordered-locking.ss main
+error at: veribsync/hip-bperm1.ss readCell
+error at: veribsync/hip-bperm1.ss updateCell
+error at: veribsync/barrier-static-consistency.ss main_fail
+error at: conchip/mapreduce.ss count_helper
+error at: conchip/mapreduce.ss countList
+error at: conchip/mapreduce.ss destroyList
+error at: conchip/mapreduce.ss main
+error at: conchip/mapreduce.ss mapper_helper
+error at: conchip/mapreduce.ss mapper
+error at: conchip/mapreduce.ss reducer1
+error at: conchip/mapreduce.ss reducer2
+.
+Total verification time: 457.06 second
+	Time spent in main process: 13.51 second
+	Time spent in child processes: 443.55 second
+	Number of false contexts: 1

.travis/run-fast-tests.hip.5-5

@@ -0,0 +1,8 @@
+Starting sleek-hip tests:
+Starting hip tests:
+Checking avl-orig-2.ss
+All test results were as expected.
+Total verification time: 1423.15 second
+	Time spent in main process: 389.58 second
+	Time spent in child processes: 1033.57 second
+	Number of false contexts: 0

.travis/run-fast-tests.hip.50-119

@@ -0,0 +1,52 @@
+Starting sleek-hip tests:
+Starting hip tests:
+Checking conchip/mapreduce.ss (runs with extra options: -tp parahip --classic)
+error at: conchip/mapreduce.ss count_helper
+error at: conchip/mapreduce.ss countList
+error at: conchip/mapreduce.ss destroyList
+error at: conchip/mapreduce.ss main
+error at: conchip/mapreduce.ss mapper_helper
+error at: conchip/mapreduce.ss mapper
+error at: conchip/mapreduce.ss reducer1
+error at: conchip/mapreduce.ss reducer2
+Checking conchip/multi-join2.ss (runs with extra options: -tp parahip  -perm fperm --classic)
+error at: conchip/multi-join2.ss main
+error at: conchip/multi-join2.ss thread1
+error at: conchip/multi-join2.ss thread2
+Checking conchip/latch-exp2.ss (runs with extra options: -tp parahip --classic)
+error at: conchip/latch-exp2.ss main
+error at: conchip/latch-exp2.ss thread1
+Checking conchip/deadpool.ss (runs with extra options: -tp parahip -perm fperm --classic)
+error at: conchip/deadpool.ss destroyDeadPool
+error at: conchip/deadpool.ss forkHelper
+error at: conchip/deadpool.ss forkThreads
+error at: conchip/deadpool.ss joinHelper
+error at: conchip/deadpool.ss joinThreads
+error at: conchip/deadpool.ss main
+error at: conchip/deadpool.ss thread
+Total number of errors: 20 in files:
+ error at: conchip/mapreduce.ss count_helper
+error at: conchip/mapreduce.ss countList
+error at: conchip/mapreduce.ss destroyList
+error at: conchip/mapreduce.ss main
+error at: conchip/mapreduce.ss mapper_helper
+error at: conchip/mapreduce.ss mapper
+error at: conchip/mapreduce.ss reducer1
+error at: conchip/mapreduce.ss reducer2
+error at: conchip/multi-join2.ss main
+error at: conchip/multi-join2.ss thread1
+error at: conchip/multi-join2.ss thread2
+error at: conchip/latch-exp2.ss main
+error at: conchip/latch-exp2.ss thread1
+error at: conchip/deadpool.ss destroyDeadPool
+error at: conchip/deadpool.ss forkHelper
+error at: conchip/deadpool.ss forkThreads
+error at: conchip/deadpool.ss joinHelper
+error at: conchip/deadpool.ss joinThreads
+error at: conchip/deadpool.ss main
+error at: conchip/deadpool.ss thread
+.
+Total verification time: 0.00 second
+	Time spent in main process: 0.00 second
+	Time spent in child processes: 0.00 second
+	Number of false contexts: 0

.travis/run-fast-tests.hip.6-6

@@ -0,0 +1,8 @@
+Starting sleek-hip tests:
+Starting hip tests:
+Checking avl-orig3.ss
+All test results were as expected.
+Total verification time: 1184.09 second
+	Time spent in main process: 410.61 second
+	Time spent in child processes: 773.48 second
+	Number of false contexts: 0

.travis/run-fast-tests.hip.7-19

@@ -0,0 +1,20 @@
+Starting sleek-hip tests:
+Starting hip tests:
+Checking bll.ss
+Checking bubble.ss
+Checking cll.ss
+Checking complete.ss
+Checking dll.ss
+Checking heaps.ss
+Checking insertion.ss
+Checking ll.ss
+Checking merge.ss
+Checking perfect.ss
+Checking qsort.ss
+Checking selection.ss
+Checking sll.ss
+All test results were as expected.
+Total verification time: 327.35 second
+	Time spent in main process: 145.93 second
+	Time spent in child processes: 181.42 second
+	Number of false contexts: 64

.travis/run-fast-tests.sleek.0-4

@@ -0,0 +1,12 @@
+Starting sleek tests:
+Checking sleek.slk
+Checking term.slk (runs with extra options: --efa-exc)
+Checking cll-d.slk
+Checking label-basic.slk (runs with extra options: --dis-eps)
+Checking label-dll.slk (runs with extra options: --dis-eps)
+Starting hip-sleek tests:
+All test results were as expected.
+Total verification time: 0.99 second
+	Time spent in main process: 0.85 second
+	Time spent in child processes: 0.14 second
+	Number of false contexts: 1

.travis/run-fast-tests.sleek.20-39

@@ -0,0 +1,27 @@
+Starting sleek tests:
+Checking sleek-err-exc-flow.slk (runs with extra options: --efa-exc)
+Checking lst-under2.slk (runs with extra options: --inv-test)
+Checking data-holes.slk
+Checking ll-under1a.slk (runs with extra options:  --inv-test --use-baga )
+Checking ll-under1b.slk (runs with extra options:  --inv-test --use-baga )
+Checking ll-under1c.slk (runs with extra options:  --inv-test --use-baga )
+Checking ll-under1d.slk (runs with extra options:  --inv-test --use-baga )
+Checking ll-under1e.slk (runs with extra options:  --inv-test --use-baga )
+Checking ll-under1f.slk (runs with extra options:  --inv-test --use-baga )
+Checking baga-test-eps.slk (runs with extra options: --eps)
+Checking baga-test.slk (runs with extra options: --use-baga)
+Checking baga-test-2.slk (runs with extra options: --dis-use-baga --dis-eps)
+Checking baga-test-2.slk (runs with extra options: --use-baga)
+Checking symb-diff.slk
+Checking xpure3nodes.slk
+Checking infer/app-inv.slk (runs with extra options: --inv --dis-eps)
+Checking infer/app-inv2.slk (runs with extra options: --inv --dis-eps)
+Checking infer/infer1.slk
+Checking infer/infer2.slk
+Checking infer/infer4.slk
+Starting hip-sleek tests:
+All test results were as expected.
+Total verification time: 5.80 second
+	Time spent in main process: 4.99 second
+	Time spent in child processes: 0.82 second
+	Number of false contexts: 42

.travis/run-fast-tests.sleek.40-40

@@ -0,0 +1,8 @@
+Starting sleek tests:
+Checking infer/infer5.slk
+Starting hip-sleek tests:
+All test results were as expected.
+Total verification time: 1.10 second
+	Time spent in main process: 0.32 second
+	Time spent in child processes: 0.78 second
+	Number of false contexts: 2

.travis/run-fast-tests.sleek.41-41

@@ -0,0 +1,8 @@
+Starting sleek tests:
+Checking infer/infer5a.slk
+Starting hip-sleek tests:
+All test results were as expected.
+Total verification time: 1.06 second
+	Time spent in main process: 0.45 second
+	Time spent in child processes: 0.61 second
+	Number of false contexts: 0

.travis/run-fast-tests.sleek.42-42

@@ -0,0 +1,8 @@
+Starting sleek tests:
+Checking infer/infer6.slk
+Starting hip-sleek tests:
+All test results were as expected.
+Total verification time: 0.15 second
+	Time spent in main process: 0.13 second
+	Time spent in child processes: 0.02 second
+	Number of false contexts: 0

.travis/run-fast-tests.sleek.43-43

@@ -0,0 +1,8 @@
+Starting sleek tests:
+Checking infer/infer7.slk
+Starting hip-sleek tests:
+All test results were as expected.
+Total verification time: 0.35 second
+	Time spent in main process: 0.31 second
+	Time spent in child processes: 0.04 second
+	Number of false contexts: 4

.travis/run-fast-tests.sleek.44-44

@@ -0,0 +1,8 @@
+Starting sleek tests:
+Checking infer/infer8.slk
+Starting hip-sleek tests:
+All test results were as expected.
+Total verification time: 0.86 second
+	Time spent in main process: 0.75 second
+	Time spent in child processes: 0.10 second
+	Number of false contexts: 5