Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit 67a84b35 authored by Benedikt Becker's avatar Benedikt Becker

Start testing mlw_printer

parent 12aa1ea6
......@@ -6,7 +6,7 @@ stages:
- deploy
variables:
BUILD_IMAGE: "$CI_REGISTRY_IMAGE:ci-master-2020-04-01"
BUILD_IMAGE: "$CI_REGISTRY_IMAGE:ci-master-2020-04-17"
SPHINX_IMAGE: "$CI_REGISTRY_IMAGE:ci-sphinx"
GIT_CLEAN_FLAGS: "-ffdxq"
......
......@@ -296,6 +296,20 @@ list_stuff () {
fi
}
test_mlw_printer () {
python3 -m sexpdata || return
bench_mlw_printer "bench/valid/booleans.mlw" || exit 1
bench_mlw_printer "bench/valid/complex_arg_1.mlw" || exit 1
bench_mlw_printer "bench/valid/complex_arg_2.mlw" || exit 1
bench_mlw_printer "bench/valid/division.mlw" || exit 1
bench_mlw_printer "bench/valid/exns.mlw" || exit 1
bench_mlw_printer "bench/valid/oldify.mlw" || exit 1
bench_mlw_printer "bench/valid/recfun.mlw" || exit 1
bench_mlw_printer "bench/valid/see.mlw" || exit 1
bench_mlw_printer "bench/valid/type_invariant.mlw" || exit 1
bench_mlw_printer "bench/valid/wpcalls.mlw" || exit 1
}
echo "=== Checking stdlib ==="
goods stdlib
goods stdlib/mach
......@@ -467,3 +481,6 @@ echo ""
echo "=== Checking realizations ==="
exec bench/check_realizations.sh
echo "=== Checking mlw_printer ==="
test_mlw_printer
#!/usr/bin/env python3
import sys
import sexpdata
from subprocess import Popen, PIPE
# Read a whyml file as a s-exp
def read(filename):
p = Popen(["bin/why3pp", "--output=sexp", filename], stdout=PIPE, encoding='utf8')
return sexpdata.loads(''.join(p.stdout.readlines()))
# Pretty-print a whyml file and read the result as a s-exp
def print_and_read(filename):
p = Popen(["bin/why3pp", "--output=mlw", filename], stdout=PIPE, encoding='utf8')
p1 = Popen(["bin/why3pp", "--output=sexp", "-"], stdin=p.stdout, stdout=PIPE, encoding='utf8')
return sexpdata.loads(''.join(p1.stdout.readlines()))
class NotEqual(Exception):
def __init__(self, path, sexp0, sexp1):
self.path = path
self.sexp0 = sexp0
self.sexp1 = sexp1
def is_location(sexp):
return (type(sexp) == list and
[type(x) for x in sexp] == [str, int, int, int])
def assert_equal(path, sexp0, sexp1):
if is_location(sexp0) and is_location(sexp1):
return # Don't bother with locations
elif sexp1 == sexpdata.Symbol("__todo__"):
return # And accept todos
elif type(sexp0) == list and type(sexp1) == list:
for i, (s0, s1) in enumerate(zip(sexp0, sexp1)):
return assert_equal(path+[i], s0, s1)
if len(sexp0) > len(sexp1):
raise NotEqual(path+[len(sexp1)], sexp0[len(sexp1)], None)
if len(sexp1) > len(sexp0):
raise NotEqual(path+[len(sexp0)], None, sexp1[len(sexp0)])
elif sexp0 == sexp1:
return
else:
raise NotEqual(path, sexp0, sexp1)
def trace(path, sexp, sexp1):
if path == []:
return [sexpdata.Symbol("EXPECTED"), sexp,
sexpdata.Symbol("FOUND"), sexp1]
elif type(sexp) == list:
return [trace(path[1:], sexp[i], sexp1)
if i == path[0] else sexp[i]
for i, x in enumerate(sexp)]
return sexp
def test(filename):
sexp0 = read(filename)
sexp1 = print_and_read(filename)
try:
assert_equal([], sexp0, sexp1)
print("OK:", filename)
return True
except NotEqual as e:
print("FAILED:", filename)
# sexpdata.dump(trace(e.path, sexp0, e.sexp1), sys.stdout)
return False
def main():
res = all(test(f) for f in sys.argv[1:])
exit(0 if res else 1)
if __name__ == "__main__":
main()
......@@ -8,7 +8,7 @@ USER root
ARG DEBIAN_FRONTEND=noninteractive
RUN apt-get update -yq && \
apt-get upgrade -yq --with-new-pkgs --auto-remove && \
apt-get install -yq --no-install-recommends wget libgmp-dev xvfb unzip build-essential autoconf ocaml-nox ca-certificates git xauth graphviz menhir libmenhir-ocaml-dev libzip-ocaml-dev liblablgtksourceview3-ocaml-dev libzarith-ocaml-dev && \
apt-get install -yq --no-install-recommends wget libgmp-dev xvfb unzip build-essential autoconf ocaml-nox ca-certificates git xauth graphviz menhir libmenhir-ocaml-dev libzip-ocaml-dev liblablgtksourceview3-ocaml-dev libzarith-ocaml-dev python3-sexpdata && \
apt-get clean
RUN wget --quiet https://github.com/ocaml/opam/releases/download/2.0.6/opam-2.0.6-x86_64-linux -O /usr/local/bin/opam && \
......
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