Maj terminée. Pour consulter la release notes associée voici le lien :
https://about.gitlab.com/releases/2021/07/07/critical-security-release-gitlab-14-0-4-released/

Commit e98c76c5 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

programs: typing benchmarks

parent ce84499d
......@@ -6,6 +6,7 @@ export WHYLIB=../lib
pgm=$1
pgml=$2
pgml_options=
goods () {
for f in $1/*.why; do
......@@ -50,8 +51,9 @@ drivers () {
programs () {
for f in $1/*.mlw; do
echo -n " "$f"... "
if ! $pgml $f > /dev/null 2>&1; then
echo "$pgml $2 $f"
if ! $pgml $pgml_options $f > /dev/null 2>&1; then
echo
echo "$pgml $pgml_options $f"
echo "FAILED!"
exit 1
else
......@@ -60,6 +62,20 @@ programs () {
done
}
bad_programs () {
for f in $1/*.mlw; do
echo -n " "$f"... "
if $pgml $pgml_options $f > /dev/null 2>&1; then
echo
echo "$pgml $pgml_options $f"
echo "SHOULD FAIL!"
exit 1
else
echo "ok"
fi
done
}
# 1. Syntax
echo "=== Parsing good files ==="
goods bench/typing/bad --parse-only
......@@ -82,7 +98,19 @@ echo "=== Checking drivers ==="
drivers drivers
echo ""
echo "=== Type-checking programs ==="
echo "=== Parsing programs ==="
pgml_options=--parse-only
programs bench/programs/bad-typing
programs examples/programs
echo ""
echo "=== Type-checking bad programs ==="
pgml_options=--type-only
bad_programs bench/programs/bad-typing
echo ""
echo "=== Type-checking good programs ==="
pgml_options=--type-only
programs examples/programs
echo ""
......@@ -74,6 +74,7 @@ let type_file file =
let th = Env.find_theory env ["programs"] "Prelude" in
let uc = Theory.use_export uc th in
let _uc, _dl = Pgm_typing.file env uc p in
if !type_only then raise Exit;
()
let handle_file file =
......
......@@ -4,6 +4,8 @@ use import list.List
logic c : int
}
let id x = x
let test (n:int) =
let rec is_even (x:int) =
{true}
......
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