-
Notifications
You must be signed in to change notification settings - Fork 8
/
run.sh
executable file
·20 lines (17 loc) · 854 Bytes
/
run.sh
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
INSTR_SEMANTICS="../../semantics/underTestInstructions/"
if [ -d "$INSTR_SEMANTICS" ]; then
rm -rf $INSTR_SEMANTICS/*
fi
mkdir -p $INSTR_SEMANTICS
echo "########################################################################"
echo "Copying the semantic definitions of instructions involved in the program"
echo "########################################################################"
cp -rp instruction_semantics/* $INSTR_SEMANTICS/
echo "################################################################"
echo "Compiling the semantics of instructions & execution environment"
echo "################################################################"
../../scripts/kompile.pl --backend java
echo "##################"
echo "Running the prover"
echo "##################"
time kprove test-spec.k --directory ../../semantics --smt_prelude ../basic.smt2