Commit 799925ec authored by Heiko Becker's avatar Heiko Becker
Browse files

Script that can run all tests

parent f295fc40
......@@ -25,25 +25,40 @@ mkdir -p ./hol/output
for file in "${arr[@]}"
do
echo $file
echo ""
./daisy $file --certificate=coq
echo ""
echo "Coq certificate"
time (./daisy $file --certificate=coq >/dev/null)
echo "HOL Certificate"
time (./daisy $file --certificate=hol >/dev/null)
done
#mv static_experiment.txt static_experiment_interval.txt
echo ""
echo "[Certificate Test]"
echo ""
cd coq
arrCoq=()
while IFS= read -r -d $'\0'; do
arrCoq+=("$REPLY")
done < <(find ./output/ -name "*.v" -print0)
for file in "${arrCoq[@]}"
do
echo $file
echo ""
time (coqc -R ./ Daisy $file)
done
# for file in "${arr[@]}"
# do
# echo $file
# ./daisy --noInitialErrors --rangeMethod=affine $file
# done
cd ../hol
# mv static_experiment.txt static_experiment_affine.txt
arrHOL=()
while IFS= read -r -d $'\0'; do
arrHOL+=("$REPLY")
done < <(find ./output/ -name "*.hl" -print0)
# for file in "${arr[@]}"
# do
# echo $file
# ./daisy --noInitialErrors --rangeMethod=smt $file
# done
for file in "${arrHOL[@]}"
do
echo $file
echo ""
time ((ocaml < $file) &>/dev/null)
done
# mv static_experiment.txt static_experiment_smt.txt
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment