blob: ffa909e93bff3f80218c48be9e7e90cd90d5b9b1 (
plain)
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
|
#!/usr/bin/env bash
set -ex
export COQBIN=$BIN
export PATH=$COQBIN:$PATH
cd misc
rm -f vio_checking{,bad}.{vo,vio}
coqc -vio vio_checking.v
coqc -vio vio_checking_bad.v
coqc -schedule-vio-checking 2 vio_checking.vio
if coqc -schedule-vio-checking 2 vio_checking_bad.vio; then
echo 'vio-checking on vio_checking_bad.vio should have failed!'
exit 1
fi
if coqc -schedule-vio-checking 2 vio_checking.vio vio_checking_bad.vio; then
echo 'vio-checking on vio_checking vio_checking_bad.vio should have failed!'
exit 1
fi
coqc -vio2vo vio_checking.vio
coqchk -silent vio_checking.vo
if coqc -vio2vo vio_checking_bad.vio; then
echo 'vio2vo on vio_checking_bad.vio should have failed!'
exit 1
fi
|
