From 52b326d009545af9dbf44ec54e7ce9d610414517 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Mon, 8 Jun 2015 18:14:53 -0700 Subject: Add the beginning of a new testing infrastructure runTests.py reads lit-style annotations, so we will be able to retain lit compatibility. This new framework adds: * Precise timings * Proper support for interrupting using Ctrl+C * Much better reporting (including tracking of error codes, and merging of successive reports for performance tracking) * No dependency on lit, OutputCheck, or Diff * Pretty colors! --- Test/runTests.py | 457 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 457 insertions(+) create mode 100644 Test/runTests.py (limited to 'Test/runTests.py') diff --git a/Test/runTests.py b/Test/runTests.py new file mode 100644 index 00000000..bf4b0d9d --- /dev/null +++ b/Test/runTests.py @@ -0,0 +1,457 @@ +import os +import re +import sys +import csv +import shlex +import shutil +import argparse +import operator +import platform +from enum import Enum +from time import time, strftime +from multiprocessing import Pool +from collections import defaultdict +from subprocess import Popen, call, PIPE, TimeoutExpired + +# C:/Python34/python.exe runTests.py --compiler "c:/MSR/dafny/Binaries/Dafny.exe /useBaseNameForFileName /compile:1 /nologo" --difftool "C:\Program Files (x86)\Meld\Meld.exe" -j4 -f "/dprelude preludes\AlmostAllTriggers.bpl" dafny0\SeqFromArray.dfy + +# c:/Python34/python.exe runTests.py --compare ../TestStable/results/SequenceAxioms/2015-06-06-00-54-52--PrettyPrinted.report.csv ../TestStable/results/SequenceAxioms/*.csv + +ANSI = False +try: + import colorama + colorama.init() + ANSI = True +except ImportError: + try: + import tendo.ansiterm + ANSI = True + except ImportError: + pass + +VERBOSITY = None +KILLED = False + +ALWAYS_EXCLUDED = ["Output", "snapshots", "sandbox"] + + +class Debug(Enum): + ERROR = (-1, '\033[91m') + REPORT = (0, '\033[0m') + INFO = (1, '\033[0m') + DEBUG = (2, '\033[0m') + TRACE = (3, '\033[0m') + + def __init__(self, index, color): + self.index = index + self.color = color + +def wrap_color(string, color): + if ANSI: + return color + string + '\033[0m' + else: + return string + +def debug(level, *args, **kwargs): + kwargs["file"] = sys.stderr + kwargs["flush"] = True + + headers = kwargs.pop("headers", []) + if isinstance(headers, Enum): + headers = [headers] + + if level and level.index <= VERBOSITY: + if level: + headers = [level] + headers + headers = tuple("[" + wrap_color("{: ^8}".format(h.name), h.color) + "]" for h in headers) + print(*(headers + args), **kwargs) + +class TestStatus(Enum): + PENDING = (0, '\033[0m') + PASSED = (1, '\033[92m') + FAILED = (2, '\033[91m') + UNKNOWN = (3, '\033[91m') + TIMEOUT = (4, '\033[91m') + + def __init__(self, index, color): + self.index = index + self.color = color + +class Test: + COLUMNS = ["name", "status", "start", "end", "duration", "returncodes", "suite_time", "njobs", "proc_info", "source_path", "temp_directory", "cmds", "expected", "output"] + + def __init__(self, name, source_path, cmds, timeout): + self.name = name + self.source_path = source_path + self.expect_path = Test.source_to_expect_path(self.source_path) + self.source_directory, self.fname = os.path.split(self.source_path) + self.temp_directory = os.path.join(self.source_directory, "Output") + self.temp_output_path = os.path.join(self.temp_directory, self.fname + ".tmp") + + self.output = None + self.expected = Test.read_normalize(self.expect_path) + + self.cmds = cmds + self.timeout = timeout + self.cmds = [cmd.replace("%s", self.source_path) for cmd in self.cmds] + self.cmds = [cmd.replace("%t", self.temp_output_path) for cmd in self.cmds] + + self.status = TestStatus.PENDING + self.proc_info = platform.processor() + + self.time, self.suite_time = None, None + self.njobs, self.returncodes = None, [] + + @staticmethod + def source_to_expect_path(source): + return source + ".expect" + + @staticmethod + def read_normalize(path): + with open(path, mode="rb") as reader: + return reader.read().replace(b'\r\n', b'\n').replace(b'\r', b'\n') + + @staticmethod + def build_report(tests, name): + time = strftime("%Y-%m-%d-%H-%M-%S") + if name: + directory, fname = os.path.split(name) + name = os.path.join(directory, time + "--" + fname) + else: + name = time + + with open(name + ".csv", mode='w', newline='') as writer: + csv_writer = csv.DictWriter(writer, Test.COLUMNS, dialect='excel') + csv_writer.writeheader() # TODO enable later + for test in tests: + test.serialize(csv_writer) + + @staticmethod + def load_report(path): + results = [] + with open(path) as csvfile: + for row in csv.DictReader(csvfile): #, fieldnames=Test.COLUMNS): + results.append(Test.deserialize(row)) + return results + + @staticmethod + def summarize(results): + debug(None, "") + debug(Debug.INFO, "** Testing complete ({} tests) **".format(len(results))) + + if results: + debug(Debug.REPORT, "Testing took {:.2f}s on {} threads".format(results[0].suite_time, results[0].njobs)) + + grouped = defaultdict(list) + for t in results: + grouped[t.status].append(t) + + for status, ts in sorted(grouped.items(), key=lambda x: x[0].index): + if ts: + debug(Debug.REPORT, "{}/{} -- {}".format(len(ts), len(results), ", ".join(t.name for t in ts)), headers=status) + + def run(self): + debug(Debug.DEBUG, "Starting {}".format(self.name)) + os.makedirs(self.temp_directory, exist_ok = True) + # os.chdir(self.source_directory) + + stdout, stderr = b'', b'' + self.start = time() + + try: + for cmd in self.cmds: + debug(Debug.DEBUG, "> {}".format(cmd)) + try: + #, timeout = 60*60) + proc = Popen(cmd, stdin=PIPE, stdout=PIPE, stderr=PIPE, shell=True) + _stdout, _stderr = proc.communicate(timeout=self.timeout) + stdout, stderr = stdout + _stdout, stderr + _stderr + self.returncodes.append(proc.returncode) + except FileNotFoundError: + debug(Debug.ERROR, "Program '{}' not found".format(cmd)) + self.status = TestStatus.UNKNOWN + return + except TimeoutExpired: + self.status = TestStatus.TIMEOUT + self.end = self.start + self.timeout + self.duration = self.timeout + return + + self.end = time() + self.duration = self.end - self.start + + stdout, stderr = stdout.strip(), stderr.strip() + if stdout != b"" or stderr != b"": + debug(Debug.TRACE, "Writing the output of {} to {}".format(self.name, self.temp_output_path)) + with open(self.temp_output_path, mode='ab') as writer: + writer.write(stdout + stderr) + if stderr != b"": + debug(Debug.TRACE, stderr) + + self.update_status() + except TimeoutExpired: + self.status = TestStatus.TIMEOUT + except KeyboardInterrupt: + raise + + def update_status(self): + self.output = Test.read_normalize(self.temp_output_path) + self.status = TestStatus.PASSED if self.expected == self.output else TestStatus.FAILED + + def report(self, tid): + debug(Debug.INFO, "{} ({})".format(self.name, tid), headers=self.status) + + @staticmethod + def write_bytes(base_directory, relative_path, extension, contents): + with open(os.path.join(base_directory, relative_path + extension), mode='wb') as writer: + writer.write(contents) + + def serialize(self, csv_writer): + csv_writer.writerow({col: getattr(self, col) for col in Test.COLUMNS}) + + @classmethod + def deserialize(cls, row): + test = cls.__new__(cls) + for col, val in row.items(): + setattr(test, col, val) + test.duration = float(test.duration) + test.status = next(x for x in TestStatus if str(x) == test.status) + return test + +def setup_parser(): + parser = argparse.ArgumentParser(description='Run the Dafny test suite.') + + parser.add_argument('paths', type=str, action='store', nargs='+', + help='Input files or folders. Folders are searched for .dfy files.') + + parser.add_argument('--compiler', type=str, action='store', default='Dafny.exe', + help='Command to use for %dafny.') + + parser.add_argument('--more-flags', '-f', type=str, action='store', default='', + help='Command used to run the tests.') + + parser.add_argument('--njobs', '-j', action='store', type=int, default=None, + help='Number of test workers.') + + parser.add_argument('--exclude', action='append', type=str, default=[], + help='Excluded directories. {} are automatically added.'.format(ALWAYS_EXCLUDED)) + + parser.add_argument('--verbosity', action='store', type=int, default=1, + help='Set verbosity level. 0: Minimal; 1: Some info; 2: More info.') + + parser.add_argument('--report', '-r', action='store', type=str, default=None, + help='Give an explicit name to the report file. Defaults to the current date and time.') + + parser.add_argument('--timeout', action='store', type=float, default=15*60.0, + help='Prover timeout') + + parser.add_argument('--compare', action='store_true', + help="Compare two previously generated reports.") + + parser.add_argument('--diff', '-d', action='store_const', const=True, default=False, + help="Don't run tests; show differences for one file.") + + parser.add_argument('--open', '-o', action='store_const', const=True, default=False, + help="Don't run tests; open one file.") + + parser.add_argument('--accept', '-a', action='store_const', const=True, default=False, + help="Used in conjuction with --diff, accept the new output.") + + parser.add_argument('--difftool', action='store', type=str, default="diff", + help='Diff command line.') + return parser + + +def run_one(test_args): + global KILLED + global VERBOSITY + + test, args = test_args + VERBOSITY = args.verbosity + + try: + if not KILLED: + test.run() + except KeyboardInterrupt: + # There's no reliable way to handle this cleanly on Windows: if one + # of the worker dies, it gets respawned. The reliable solution is to + # ignore further work once you receive a kill signal + KILLED = True + except Exception as e: + debug(Debug.ERROR, "For file {}".format(test.name), e) + test.status = TestStatus.UNKNOWN + return test + +def read_one_test(name, fname, compiler_cmd, timeout): + source_path = os.path.realpath(fname) + with open(source_path, mode='r') as reader: + cmds = [] + for line in reader: + line = line.strip() + match = re.match("^// *RUN: *(?!%diff)([^ ].*)$", line) + if match: + cmds.append(match.groups()[0].replace("%dafny", compiler_cmd)) + else: + break + if cmds: + if os.path.exists(Test.source_to_expect_path(source_path)): + return [Test(name, source_path, cmds, timeout)] + else: + debug(Debug.DEBUG, "Test file {} has no .expect".format(fname)) + else: + debug(Debug.INFO, "Test file {} has no RUN specification".format(fname)) + + return [] + + +def find_one(name, fname, compiler_cmd, timeout): + name, ext = os.path.splitext(fname) + if ext == ".dfy": + if os.path.exists(fname): + debug(Debug.TRACE, "Found test file: {}".format(fname)) + yield from read_one_test(name, fname, compiler_cmd, timeout) + else: + debug(Debug.ERROR, "Test file {} not found".format(fname)) + else: + debug(Debug.TRACE, "Ignoring {}".format(fname)) + + +def find_tests(paths, compiler_cmd, excluded, timeout): + for path in paths: + if os.path.isdir(path): + debug(Debug.TRACE, "Searching for tests in {}".format(path)) + for base, dirnames, fnames in os.walk(path): + dirnames[:] = [d for d in dirnames if d not in excluded] + for fname in fnames: + yield from find_one(fname, os.path.join(base, fname), compiler_cmd, timeout) + else: + yield from find_one(path, path, compiler_cmd, timeout) + + +def run_tests(args): + compiler_cmd = shlex.split(args.compiler) + compiler_bin = compiler_cmd[0] + + if not os.path.exists(compiler_cmd[0]): + debug(Debug.ERROR, "Compiler not found: {}".format(compiler_bin)) + return + + tests = list(find_tests(args.paths, args.compiler + ' ' + args.more_flags, + args.exclude + ALWAYS_EXCLUDED, args.timeout)) + tests.sort(key=operator.attrgetter("name")) + + args.njobs = args.njobs or os.cpu_count() or 1 + debug(Debug.INFO, "** Running {} tests on {} testing threads, timeout is {:.2f} **".format(len(tests), args.njobs, args.timeout)) + try: + pool = Pool(args.njobs) #, init_tester) + + start = time() + results = [] + for tid, test in enumerate(pool.imap_unordered(run_one, [(t, args) for t in tests], 1)): + test.report(tid + 1) + results.append(test) + pool.close() + pool.join() + suite_time = time() - start + + for t in results: + t.njobs = args.njobs + t.suite_time = suite_time + + Test.summarize(results) + Test.build_report(results, args.report) + except KeyboardInterrupt: + pool.terminate() + pool.join() + debug(Debug.ERROR, "Testing interrupted") + + +def diff(paths, accept, difftool): + if len(paths) > 1: + debug(Debug.ERROR, "Please specify a single path") + elif not os.path.exists(paths[0]): + debug(Debug.ERROR, "Not found: {}".format(paths[0])) + else: + test = Test(None, paths[0], [], None) + if accept: + shutil.copy(test.temp_output_path, test.expect_path) + else: + call([difftool, test.expect_path, test.temp_output_path]) + +def compare_results(globs): + from glob import glob + paths = [path for g in globs for path in glob(g)] + reports = {path: Test.load_report(path) for path in paths} + resultsets = {path: {test.name: (test.status, test.duration) for test in report} + for path, report in reports.items()} + + all_tests = set(name for resultset in resultsets.values() for name in resultset.keys()) + + reference = resultsets[paths[0]] + for path, resultset in resultsets.items(): + resultset["$$TOTAL$$"] = None, sum(v[1] for v in resultset.values() if v[1] and v[0] != TestStatus.TIMEOUT) + + print(all_tests) + with open("compare.csv", mode='w', newline='') as writer: + csv_writer = csv.writer(writer, dialect='excel') + csv_writer.writerow(["Name"] + [os.path.split(path)[1].lstrip("0123456789-") for path in paths]) + + for name in sorted(all_tests) + ["$$TOTAL$$"]: + ref_status, ref_duration = reference[name] + + row = [] + row.append(name) + row.append(ref_duration) + for path in paths[1:]: + test_status, test_duration = resultsets[path][name] + if test_status == ref_status: + result = "{:.2%}".format((test_duration - ref_duration) / ref_duration) + else: + result = test_status.name + "?!" + row.append(result) + + csv_writer.writerow(row) + + +# def compare_results(globs): +# from glob import glob +# baseline = dict() +# results = defaultdict(dict) +# paths = [p for g in globs for p in glob(g)] + +# for path in paths: +# report = Test.load_report(path) +# for test in report: # FIXME add return codes (once we have them) +# if test.duration: +# bl = baseline.setdefault(test.name, float(test.duration)) +# result = "timeout" if test.status == TestStatus.TIMEOUT else (float(test.duration) - bl) / bl +# else: +# result = "???" +# results[test.name][path] = result, test.duration, test.status.name + +# with open("compare.csv", mode='w', newline='') as writer: +# csv_writer = csv.writer(writer, dialect='excel') +# csv_writer.writerow(["Name"] + [os.path.split(path)[1].lstrip("0123456789-") for path in paths]) +# for name, tresults in sorted(results.items()): +# res = [tresults.get(path) for path in paths] +# csv_writer.writerow([name] + [r[0] for r in res]) +# csv_writer.writerow([name + "*"] + [r[1:] for r in res]) + + +def main(): + global VERBOSITY + parser = setup_parser() + args = parser.parse_args() + VERBOSITY = args.verbosity + + if args.diff: + diff(args.paths, args.accept, args.difftool) + elif args.open: + os.startfile(args.paths[0]) + elif args.compare: + compare_results(args.paths) + else: + run_tests(args) + +if __name__ == '__main__': + main() -- cgit v1.2.3 From b9ed0285592f5f0d12d02b3d9155dfe46903b6c5 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Wed, 10 Jun 2015 16:29:50 -0700 Subject: Small improvements to runTests.py --- Test/runTests.bat | 2 +- Test/runTests.py | 33 ++++++++++++++++++++------------- 2 files changed, 21 insertions(+), 14 deletions(-) (limited to 'Test/runTests.py') diff --git a/Test/runTests.bat b/Test/runTests.bat index 4eeed06b..ced3bd27 100644 --- a/Test/runTests.bat +++ b/Test/runTests.bat @@ -1,2 +1,2 @@ @REM runTests.bat -f "/dprelude PRELUDE_FILE" -r REPORT_NAME INPUT_FILES -C:/Python34/python.exe runTests.py --compiler "c:/MSR/dafny/Binaries/Dafny.exe /useBaseNameForFileName /compile:1 /nologo" --difftool "C:\Program Files (x86)\Meld\Meld.exe" -j4 %* +C:/Python34/python.exe runTests.py --flags "/useBaseNameForFileName /compile:1 /nologo" --difftool "C:/Program Files (x86)/Meld/Meld.exe" %* diff --git a/Test/runTests.py b/Test/runTests.py index bf4b0d9d..1d16440e 100644 --- a/Test/runTests.py +++ b/Test/runTests.py @@ -137,11 +137,9 @@ class Test: @staticmethod def summarize(results): debug(None, "") - debug(Debug.INFO, "** Testing complete ({} tests) **".format(len(results))) + debug(Debug.INFO, "** Testing complete ({} tests) **".format(len(results))) if results: - debug(Debug.REPORT, "Testing took {:.2f}s on {} threads".format(results[0].suite_time, results[0].njobs)) - grouped = defaultdict(list) for t in results: grouped[t.status].append(t) @@ -149,6 +147,7 @@ class Test: for status, ts in sorted(grouped.items(), key=lambda x: x[0].index): if ts: debug(Debug.REPORT, "{}/{} -- {}".format(len(ts), len(results), ", ".join(t.name for t in ts)), headers=status) + debug(Debug.REPORT, "Testing took {:.2f}s on {} threads".format(results[0].suite_time, results[0].njobs)) def run(self): debug(Debug.DEBUG, "Starting {}".format(self.name)) @@ -224,11 +223,11 @@ def setup_parser(): parser.add_argument('paths', type=str, action='store', nargs='+', help='Input files or folders. Folders are searched for .dfy files.') - parser.add_argument('--compiler', type=str, action='store', default='Dafny.exe', - help='Command to use for %dafny.') + parser.add_argument('--compiler', type=str, action='store', default=None, + help='Dafny executable.') - parser.add_argument('--more-flags', '-f', type=str, action='store', default='', - help='Command used to run the tests.') + parser.add_argument('--flags', '-f', type=str, action='append', default=[], + help='Arguments to pass to dafny. Multiple --flags are concatenated.') parser.add_argument('--njobs', '-j', action='store', type=int, default=None, help='Number of test workers.') @@ -248,6 +247,9 @@ def setup_parser(): parser.add_argument('--compare', action='store_true', help="Compare two previously generated reports.") + parser.add_argument('--time-failures', action='store_true', + help="When comparing, include timings of failures.") + parser.add_argument('--diff', '-d', action='store_const', const=True, default=False, help="Don't run tests; show differences for one file.") @@ -336,14 +338,19 @@ def run_tests(args): debug(Debug.ERROR, "Compiler not found: {}".format(compiler_bin)) return - tests = list(find_tests(args.paths, args.compiler + ' ' + args.more_flags, + if args.compiler is None: + base_directory = os.path.dirname(os.path.realpath(__file__)) + compiler = os.path.normpath(os.path.join(base_directory, "../Binaries/Dafny.exe")) + + tests = list(find_tests(args.paths, compiler + ' ' + " ".join(args.flags), args.exclude + ALWAYS_EXCLUDED, args.timeout)) tests.sort(key=operator.attrgetter("name")) args.njobs = args.njobs or os.cpu_count() or 1 - debug(Debug.INFO, "** Running {} tests on {} testing threads, timeout is {:.2f} **".format(len(tests), args.njobs, args.timeout)) + debug(Debug.INFO, "** Running {} tests on {} testing threads, timeout is {:.2f}, started at {}**".format(len(tests), args.njobs, args.timeout, strftime("%H:%M:%S"))) + try: - pool = Pool(args.njobs) #, init_tester) + pool = Pool(args.njobs) start = time() results = [] @@ -378,7 +385,7 @@ def diff(paths, accept, difftool): else: call([difftool, test.expect_path, test.temp_output_path]) -def compare_results(globs): +def compare_results(globs, time_failures): from glob import glob paths = [path for g in globs for path in glob(g)] reports = {path: Test.load_report(path) for path in paths} @@ -404,7 +411,7 @@ def compare_results(globs): row.append(ref_duration) for path in paths[1:]: test_status, test_duration = resultsets[path][name] - if test_status == ref_status: + if test_status == ref_status or (test_status == TestStatus.FAILED and time_failures): result = "{:.2%}".format((test_duration - ref_duration) / ref_duration) else: result = test_status.name + "?!" @@ -449,7 +456,7 @@ def main(): elif args.open: os.startfile(args.paths[0]) elif args.compare: - compare_results(args.paths) + compare_results(args.paths, args.time_failures) else: run_tests(args) -- cgit v1.2.3 From b0b1f8782080528a0ebcaa2bd0fc0c8641b2efdd Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 11 Jun 2015 19:59:16 -0700 Subject: A few more improvements to runTests.py --- Test/runTests.py | 112 ++++++++++++++++++++++++++++--------------------------- 1 file changed, 58 insertions(+), 54 deletions(-) (limited to 'Test/runTests.py') diff --git a/Test/runTests.py b/Test/runTests.py index 1d16440e..5b2050a7 100644 --- a/Test/runTests.py +++ b/Test/runTests.py @@ -80,7 +80,7 @@ class TestStatus(Enum): class Test: COLUMNS = ["name", "status", "start", "end", "duration", "returncodes", "suite_time", "njobs", "proc_info", "source_path", "temp_directory", "cmds", "expected", "output"] - def __init__(self, name, source_path, cmds, timeout): + def __init__(self, name, source_path, cmds, timeout, compiler_id): self.name = name self.source_path = source_path self.expect_path = Test.source_to_expect_path(self.source_path) @@ -93,6 +93,7 @@ class Test: self.cmds = cmds self.timeout = timeout + self.compiler_id = compiler_id self.cmds = [cmd.replace("%s", self.source_path) for cmd in self.cmds] self.cmds = [cmd.replace("%t", self.temp_output_path) for cmd in self.cmds] @@ -146,7 +147,7 @@ class Test: for status, ts in sorted(grouped.items(), key=lambda x: x[0].index): if ts: - debug(Debug.REPORT, "{}/{} -- {}".format(len(ts), len(results), ", ".join(t.name for t in ts)), headers=status) + debug(Debug.REPORT, "{}/{} -- {}".format(len(ts), len(results), " ".join(t.name for t in ts)), headers=status) debug(Debug.REPORT, "Testing took {:.2f}s on {} threads".format(results[0].suite_time, results[0].njobs)) def run(self): @@ -197,8 +198,8 @@ class Test: self.output = Test.read_normalize(self.temp_output_path) self.status = TestStatus.PASSED if self.expected == self.output else TestStatus.FAILED - def report(self, tid): - debug(Debug.INFO, "{} ({})".format(self.name, tid), headers=self.status) + def report(self, tid, total): + debug(Debug.INFO, "[{}] [{:.2f}s] {} ({} of {})".format(self.compiler_id, self.duration, self.name, tid, total), headers=self.status) @staticmethod def write_bytes(base_directory, relative_path, extension, contents): @@ -223,7 +224,7 @@ def setup_parser(): parser.add_argument('paths', type=str, action='store', nargs='+', help='Input files or folders. Folders are searched for .dfy files.') - parser.add_argument('--compiler', type=str, action='store', default=None, + parser.add_argument('--compiler', type=str, action='append', default=[], help='Dafny executable.') parser.add_argument('--flags', '-f', type=str, action='append', default=[], @@ -247,8 +248,8 @@ def setup_parser(): parser.add_argument('--compare', action='store_true', help="Compare two previously generated reports.") - parser.add_argument('--time-failures', action='store_true', - help="When comparing, include timings of failures.") + parser.add_argument('--time-all', action='store_true', + help="When comparing, include all timings.") parser.add_argument('--diff', '-d', action='store_const', const=True, default=False, help="Don't run tests; show differences for one file.") @@ -284,65 +285,63 @@ def run_one(test_args): test.status = TestStatus.UNKNOWN return test -def read_one_test(name, fname, compiler_cmd, timeout): - source_path = os.path.realpath(fname) - with open(source_path, mode='r') as reader: - cmds = [] - for line in reader: - line = line.strip() - match = re.match("^// *RUN: *(?!%diff)([^ ].*)$", line) - if match: - cmds.append(match.groups()[0].replace("%dafny", compiler_cmd)) +def read_one_test(name, fname, compiler_cmds, timeout): + for cid, compiler_cmd in enumerate(compiler_cmds): + source_path = os.path.realpath(fname) + with open(source_path, mode='r') as reader: + cmds = [] + for line in reader: + line = line.strip() + match = re.match("^// *RUN: *(?!%diff)([^ ].*)$", line) + if match: + cmds.append(match.groups()[0].replace("%dafny", compiler_cmd)) + else: + break + if cmds: + if os.path.exists(Test.source_to_expect_path(source_path)): + yield Test(name, source_path, cmds, timeout, cid) else: - break - if cmds: - if os.path.exists(Test.source_to_expect_path(source_path)): - return [Test(name, source_path, cmds, timeout)] + debug(Debug.DEBUG, "Test file {} has no .expect".format(fname)) else: - debug(Debug.DEBUG, "Test file {} has no .expect".format(fname)) - else: - debug(Debug.INFO, "Test file {} has no RUN specification".format(fname)) - - return [] + debug(Debug.INFO, "Test file {} has no RUN specification".format(fname)) -def find_one(name, fname, compiler_cmd, timeout): +def find_one(name, fname, compiler_cmds, timeout): name, ext = os.path.splitext(fname) if ext == ".dfy": if os.path.exists(fname): debug(Debug.TRACE, "Found test file: {}".format(fname)) - yield from read_one_test(name, fname, compiler_cmd, timeout) + yield from read_one_test(name, fname, compiler_cmds, timeout) else: debug(Debug.ERROR, "Test file {} not found".format(fname)) else: debug(Debug.TRACE, "Ignoring {}".format(fname)) -def find_tests(paths, compiler_cmd, excluded, timeout): +def find_tests(paths, compiler_cmds, excluded, timeout): for path in paths: if os.path.isdir(path): debug(Debug.TRACE, "Searching for tests in {}".format(path)) for base, dirnames, fnames in os.walk(path): dirnames[:] = [d for d in dirnames if d not in excluded] for fname in fnames: - yield from find_one(fname, os.path.join(base, fname), compiler_cmd, timeout) + yield from find_one(fname, os.path.join(base, fname), compiler_cmds, timeout) else: - yield from find_one(path, path, compiler_cmd, timeout) + yield from find_one(path, path, compiler_cmds, timeout) def run_tests(args): - compiler_cmd = shlex.split(args.compiler) - compiler_bin = compiler_cmd[0] - - if not os.path.exists(compiler_cmd[0]): - debug(Debug.ERROR, "Compiler not found: {}".format(compiler_bin)) - return - - if args.compiler is None: + if args.compiler is []: base_directory = os.path.dirname(os.path.realpath(__file__)) - compiler = os.path.normpath(os.path.join(base_directory, "../Binaries/Dafny.exe")) + args.compiler = [os.path.normpath(os.path.join(base_directory, "../Binaries/Dafny.exe"))] - tests = list(find_tests(args.paths, compiler + ' ' + " ".join(args.flags), + for compiler in args.compiler: + if not os.path.exists(compiler): + debug(Debug.ERROR, "Compiler not found: {}".format(compiler)) + return + + tests = list(find_tests(args.paths, [compiler + ' ' + " ".join(args.flags) + for compiler in args.compiler], args.exclude + ALWAYS_EXCLUDED, args.timeout)) tests.sort(key=operator.attrgetter("name")) @@ -355,7 +354,7 @@ def run_tests(args): start = time() results = [] for tid, test in enumerate(pool.imap_unordered(run_one, [(t, args) for t in tests], 1)): - test.report(tid + 1) + test.report(tid + 1, len(tests)) results.append(test) pool.close() pool.join() @@ -374,18 +373,22 @@ def run_tests(args): def diff(paths, accept, difftool): - if len(paths) > 1: - debug(Debug.ERROR, "Please specify a single path") - elif not os.path.exists(paths[0]): - debug(Debug.ERROR, "Not found: {}".format(paths[0])) - else: - test = Test(None, paths[0], [], None) - if accept: - shutil.copy(test.temp_output_path, test.expect_path) + for path in paths: + if not path.endswith(".dfy"): + path += ".dfy" + + if not os.path.exists(path): + debug(Debug.ERROR, "Not found: {}".format(path)) else: - call([difftool, test.expect_path, test.temp_output_path]) + test = Test(None, path, [], None) + if not accept: + call([difftool, test.expect_path, test.temp_output_path]) + + if accept or input("Accept this change? (y/N)") == "y": + debug(Debug.INFO, path, "Accepted") + shutil.copy(test.temp_output_path, test.expect_path) -def compare_results(globs, time_failures): +def compare_results(globs, time_all): from glob import glob paths = [path for g in globs for path in glob(g)] reports = {path: Test.load_report(path) for path in paths} @@ -410,8 +413,9 @@ def compare_results(globs, time_failures): row.append(name) row.append(ref_duration) for path in paths[1:]: - test_status, test_duration = resultsets[path][name] - if test_status == ref_status or (test_status == TestStatus.FAILED and time_failures): + res = resultsets[path].get(name) + test_status, test_duration = res if res else (TestStatus.UNKNOWN, None) + if res is not None and (test_status == ref_status or time_all): result = "{:.2%}".format((test_duration - ref_duration) / ref_duration) else: result = test_status.name + "?!" @@ -456,7 +460,7 @@ def main(): elif args.open: os.startfile(args.paths[0]) elif args.compare: - compare_results(args.paths, args.time_failures) + compare_results(args.paths, args.time_all) else: run_tests(args) -- cgit v1.2.3 From e3df1e20893c90700d3f9a23902ff5220e79994d Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 11 Jun 2015 20:15:13 -0700 Subject: Add missing default parameter in runTests.py --- Test/runTests.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Test/runTests.py') diff --git a/Test/runTests.py b/Test/runTests.py index 5b2050a7..df233a94 100644 --- a/Test/runTests.py +++ b/Test/runTests.py @@ -80,7 +80,7 @@ class TestStatus(Enum): class Test: COLUMNS = ["name", "status", "start", "end", "duration", "returncodes", "suite_time", "njobs", "proc_info", "source_path", "temp_directory", "cmds", "expected", "output"] - def __init__(self, name, source_path, cmds, timeout, compiler_id): + def __init__(self, name, source_path, cmds, timeout, compiler_id = 0): self.name = name self.source_path = source_path self.expect_path = Test.source_to_expect_path(self.source_path) -- cgit v1.2.3 From 1b64a68eaa9013047ca3af9910f2fbc264e6f3ac Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 12 Jun 2015 11:44:14 -0700 Subject: Small fix in runTests.py --- Test/runTests.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'Test/runTests.py') diff --git a/Test/runTests.py b/Test/runTests.py index df233a94..044cf260 100644 --- a/Test/runTests.py +++ b/Test/runTests.py @@ -331,7 +331,7 @@ def find_tests(paths, compiler_cmds, excluded, timeout): def run_tests(args): - if args.compiler is []: + if args.compiler == []: base_directory = os.path.dirname(os.path.realpath(__file__)) args.compiler = [os.path.normpath(os.path.join(base_directory, "../Binaries/Dafny.exe"))] @@ -401,7 +401,6 @@ def compare_results(globs, time_all): for path, resultset in resultsets.items(): resultset["$$TOTAL$$"] = None, sum(v[1] for v in resultset.values() if v[1] and v[0] != TestStatus.TIMEOUT) - print(all_tests) with open("compare.csv", mode='w', newline='') as writer: csv_writer = csv.writer(writer, dialect='excel') csv_writer.writerow(["Name"] + [os.path.split(path)[1].lstrip("0123456789-") for path in paths]) -- cgit v1.2.3 From 80ca1f0f28afa5f4b132ac0d64efa5d877f0d590 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 17 Jul 2015 13:48:42 -0700 Subject: Clean up runTests after 2015/07/17 meeting --- Test/runTests.py | 137 +++++++++++++++++++++++++++---------------------------- 1 file changed, 68 insertions(+), 69 deletions(-) (limited to 'Test/runTests.py') diff --git a/Test/runTests.py b/Test/runTests.py index 044cf260..efabdc73 100644 --- a/Test/runTests.py +++ b/Test/runTests.py @@ -2,7 +2,6 @@ import os import re import sys import csv -import shlex import shutil import argparse import operator @@ -17,10 +16,15 @@ from subprocess import Popen, call, PIPE, TimeoutExpired # c:/Python34/python.exe runTests.py --compare ../TestStable/results/SequenceAxioms/2015-06-06-00-54-52--PrettyPrinted.report.csv ../TestStable/results/SequenceAxioms/*.csv +VERBOSITY = None +KILLED = False ANSI = False + try: import colorama - colorama.init() + no_native_ansi = os.name == 'nt' and os.environ.get("TERM") in [None, "cygwin"] + tty = all(hasattr(stream, 'isatty') and stream.isatty() for stream in (sys.stdout, sys.stderr)) + colorama.init(strip=no_native_ansi, convert=no_native_ansi and tty) ANSI = True except ImportError: try: @@ -29,25 +33,28 @@ except ImportError: except ImportError: pass -VERBOSITY = None -KILLED = False - -ALWAYS_EXCLUDED = ["Output", "snapshots", "sandbox"] - +class Defaults: + ALWAYS_EXCLUDED = ["Output", "snapshots", "sandbox", "desktop"] + DAFNY_BIN = os.path.realpath(os.path.join(os.path.dirname(__file__), "../Binaries/Dafny.exe")) + COMPILER = [DAFNY_BIN] + FLAGS = ["/useBaseNameForFileName", "/compile:1", "/nologo", "/timeLimit:120"] class Debug(Enum): ERROR = (-1, '\033[91m') - REPORT = (0, '\033[0m') - INFO = (1, '\033[0m') + REPORT = (0, '\033[0m', True) + INFO = (1, '\033[0m', True) DEBUG = (2, '\033[0m') TRACE = (3, '\033[0m') - def __init__(self, index, color): + def __init__(self, index, color, elide=False): self.index = index self.color = color + self.elide = elide -def wrap_color(string, color): - if ANSI: +def wrap_color(string, color, silent=False): + if silent: + return " " * len(string) + elif ANSI: return color + string + '\033[0m' else: return string @@ -60,10 +67,14 @@ def debug(level, *args, **kwargs): if isinstance(headers, Enum): headers = [headers] + silentheaders = kwargs.pop("silentheaders", False) + if level and level.index <= VERBOSITY: if level: - headers = [level] + headers - headers = tuple("[" + wrap_color("{: ^8}".format(h.name), h.color) + "]" for h in headers) + headers = [level] + headers + + headers = tuple(wrap_color("{: <8}".format("[" + h.name + "]"), h.color, silent = silentheaders) + for h in headers if not h.elide) print(*(headers + args), **kwargs) class TestStatus(Enum): @@ -76,13 +87,15 @@ class TestStatus(Enum): def __init__(self, index, color): self.index = index self.color = color + self.elide = False class Test: COLUMNS = ["name", "status", "start", "end", "duration", "returncodes", "suite_time", "njobs", "proc_info", "source_path", "temp_directory", "cmds", "expected", "output"] def __init__(self, name, source_path, cmds, timeout, compiler_id = 0): self.name = name - self.source_path = source_path + self.dfy = None if self.name is None else (self.name + ".dfy") + self.source_path = Test.uncygdrive(source_path) self.expect_path = Test.source_to_expect_path(self.source_path) self.source_directory, self.fname = os.path.split(self.source_path) self.temp_directory = os.path.join(self.source_directory, "Output") @@ -107,6 +120,10 @@ class Test: def source_to_expect_path(source): return source + ".expect" + @staticmethod + def uncygdrive(path): + return re.sub("^/cygdrive/([a-zA-Z])/", r"\1:/", path) + @staticmethod def read_normalize(path): with open(path, mode="rb") as reader: @@ -137,22 +154,26 @@ class Test: @staticmethod def summarize(results): - debug(None, "") + debug(Debug.INFO, "\nTesting complete ({} test(s))".format(len(results))) - debug(Debug.INFO, "** Testing complete ({} tests) **".format(len(results))) if results: grouped = defaultdict(list) - for t in results: - grouped[t.status].append(t) + for test in results: + grouped[test.status].append(test) + + for status, tests in sorted(grouped.items(), key=lambda x: x[0].index): + if tests: + debug(Debug.REPORT, "{} of {}".format(len(tests), len(results)), headers=status) + if status != TestStatus.PASSED: + for test in tests: + debug(Debug.REPORT, "* " + test.dfy, headers=status, silentheaders=True) + + debug(Debug.REPORT, "Testing took {:.2f}s on {} thread(s)".format(results[0].suite_time, results[0].njobs)) - for status, ts in sorted(grouped.items(), key=lambda x: x[0].index): - if ts: - debug(Debug.REPORT, "{}/{} -- {}".format(len(ts), len(results), " ".join(t.name for t in ts)), headers=status) - debug(Debug.REPORT, "Testing took {:.2f}s on {} threads".format(results[0].suite_time, results[0].njobs)) def run(self): - debug(Debug.DEBUG, "Starting {}".format(self.name)) - os.makedirs(self.temp_directory, exist_ok = True) + debug(Debug.DEBUG, "Starting {}".format(self.dfy)) + os.makedirs(self.temp_directory, exist_ok=True) # os.chdir(self.source_directory) stdout, stderr = b'', b'' @@ -162,7 +183,6 @@ class Test: for cmd in self.cmds: debug(Debug.DEBUG, "> {}".format(cmd)) try: - #, timeout = 60*60) proc = Popen(cmd, stdin=PIPE, stdout=PIPE, stderr=PIPE, shell=True) _stdout, _stderr = proc.communicate(timeout=self.timeout) stdout, stderr = stdout + _stdout, stderr + _stderr @@ -182,7 +202,7 @@ class Test: stdout, stderr = stdout.strip(), stderr.strip() if stdout != b"" or stderr != b"": - debug(Debug.TRACE, "Writing the output of {} to {}".format(self.name, self.temp_output_path)) + debug(Debug.TRACE, "Writing the output of {} to {}".format(self.dfy, self.temp_output_path)) with open(self.temp_output_path, mode='ab') as writer: writer.write(stdout + stderr) if stderr != b"": @@ -199,7 +219,7 @@ class Test: self.status = TestStatus.PASSED if self.expected == self.output else TestStatus.FAILED def report(self, tid, total): - debug(Debug.INFO, "[{}] [{:.2f}s] {} ({} of {})".format(self.compiler_id, self.duration, self.name, tid, total), headers=self.status) + debug(Debug.INFO, "[{:5.2f}s] {} ({} of {})".format(self.duration, self.dfy, tid, total), headers=self.status) @staticmethod def write_bytes(base_directory, relative_path, extension, contents): @@ -224,17 +244,20 @@ def setup_parser(): parser.add_argument('paths', type=str, action='store', nargs='+', help='Input files or folders. Folders are searched for .dfy files.') - parser.add_argument('--compiler', type=str, action='append', default=[], - help='Dafny executable.') + parser.add_argument('--compiler', type=str, action='append', default=None, + help='Dafny executable. Default: {}'.format(Defaults.DAFNY_BIN)) + + parser.add_argument('--base-flags', type=str, action='append', default=None, + help='Arguments to pass to dafny. Multiple --flags are concatenated. Default: {}'.format(Defaults.FLAGS)) parser.add_argument('--flags', '-f', type=str, action='append', default=[], - help='Arguments to pass to dafny. Multiple --flags are concatenated.') + help='Additional arguments to pass to dafny. Useful to override some of the defaults found in --base-flags.') parser.add_argument('--njobs', '-j', action='store', type=int, default=None, help='Number of test workers.') parser.add_argument('--exclude', action='append', type=str, default=[], - help='Excluded directories. {} are automatically added.'.format(ALWAYS_EXCLUDED)) + help='Excluded directories. {} are automatically added.'.format(Defaults.ALWAYS_EXCLUDED)) parser.add_argument('--verbosity', action='store', type=int, default=1, help='Set verbosity level. 0: Minimal; 1: Some info; 2: More info.') @@ -261,7 +284,8 @@ def setup_parser(): help="Used in conjuction with --diff, accept the new output.") parser.add_argument('--difftool', action='store', type=str, default="diff", - help='Diff command line.') + help='Diff program. Default: diff.') + return parser @@ -281,7 +305,7 @@ def run_one(test_args): # ignore further work once you receive a kill signal KILLED = True except Exception as e: - debug(Debug.ERROR, "For file {}".format(test.name), e) + debug(Debug.ERROR, "[{}] {}".format(test.dfy, e)) test.status = TestStatus.UNKNOWN return test @@ -331,22 +355,23 @@ def find_tests(paths, compiler_cmds, excluded, timeout): def run_tests(args): - if args.compiler == []: - base_directory = os.path.dirname(os.path.realpath(__file__)) - args.compiler = [os.path.normpath(os.path.join(base_directory, "../Binaries/Dafny.exe"))] + if args.compiler is None: + args.compiler = Defaults.COMPILER + if args.base_flags is None: + args.base_flags = Defaults.FLAGS for compiler in args.compiler: if not os.path.exists(compiler): debug(Debug.ERROR, "Compiler not found: {}".format(compiler)) return - tests = list(find_tests(args.paths, [compiler + ' ' + " ".join(args.flags) + tests = list(find_tests(args.paths, [compiler + ' ' + " ".join(args.base_flags + args.flags) for compiler in args.compiler], - args.exclude + ALWAYS_EXCLUDED, args.timeout)) + args.exclude + Defaults.ALWAYS_EXCLUDED, args.timeout)) tests.sort(key=operator.attrgetter("name")) - args.njobs = args.njobs or os.cpu_count() or 1 - debug(Debug.INFO, "** Running {} tests on {} testing threads, timeout is {:.2f}, started at {}**".format(len(tests), args.njobs, args.timeout, strftime("%H:%M:%S"))) + args.njobs = min(args.njobs or os.cpu_count() or 1, len(tests)) + debug(Debug.INFO, "\nRunning {} test(s) on {} testing thread(s), timeout is {:.2f}s, started at {}".format(len(tests), args.njobs, args.timeout, strftime("%H:%M:%S"))) try: pool = Pool(args.njobs) @@ -384,7 +409,7 @@ def diff(paths, accept, difftool): if not accept: call([difftool, test.expect_path, test.temp_output_path]) - if accept or input("Accept this change? (y/N)") == "y": + if accept or input("Accept this change? (y/N) ") == "y": debug(Debug.INFO, path, "Accepted") shutil.copy(test.temp_output_path, test.expect_path) @@ -392,7 +417,7 @@ def compare_results(globs, time_all): from glob import glob paths = [path for g in globs for path in glob(g)] reports = {path: Test.load_report(path) for path in paths} - resultsets = {path: {test.name: (test.status, test.duration) for test in report} + resultsets = {path: {test.dfy: (test.status, test.duration) for test in report} for path, report in reports.items()} all_tests = set(name for resultset in resultsets.values() for name in resultset.keys()) @@ -422,32 +447,6 @@ def compare_results(globs, time_all): csv_writer.writerow(row) - -# def compare_results(globs): -# from glob import glob -# baseline = dict() -# results = defaultdict(dict) -# paths = [p for g in globs for p in glob(g)] - -# for path in paths: -# report = Test.load_report(path) -# for test in report: # FIXME add return codes (once we have them) -# if test.duration: -# bl = baseline.setdefault(test.name, float(test.duration)) -# result = "timeout" if test.status == TestStatus.TIMEOUT else (float(test.duration) - bl) / bl -# else: -# result = "???" -# results[test.name][path] = result, test.duration, test.status.name - -# with open("compare.csv", mode='w', newline='') as writer: -# csv_writer = csv.writer(writer, dialect='excel') -# csv_writer.writerow(["Name"] + [os.path.split(path)[1].lstrip("0123456789-") for path in paths]) -# for name, tresults in sorted(results.items()): -# res = [tresults.get(path) for path in paths] -# csv_writer.writerow([name] + [r[0] for r in res]) -# csv_writer.writerow([name + "*"] + [r[1:] for r in res]) - - def main(): global VERBOSITY parser = setup_parser() -- cgit v1.2.3 From 1f53d595ff0e4282ac51a68b124e94cd1af951ec Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Mon, 20 Jul 2015 09:48:50 -0700 Subject: Add missing .expect file + a small fix in runTests.py --- Test/dafny0/IndexIntoUpdate.dfy.expect | 6 ++++++ Test/runTests.py | 2 +- 2 files changed, 7 insertions(+), 1 deletion(-) create mode 100644 Test/dafny0/IndexIntoUpdate.dfy.expect (limited to 'Test/runTests.py') diff --git a/Test/dafny0/IndexIntoUpdate.dfy.expect b/Test/dafny0/IndexIntoUpdate.dfy.expect new file mode 100644 index 00000000..3423a20b --- /dev/null +++ b/Test/dafny0/IndexIntoUpdate.dfy.expect @@ -0,0 +1,6 @@ +IndexIntoUpdate.dfy(7,19): Error: assertion violation +Execution trace: + (0,0): anon0 + (0,0): anon3_Then + +Dafny program verifier finished with 1 verified, 1 error diff --git a/Test/runTests.py b/Test/runTests.py index efabdc73..b8d8e6f4 100644 --- a/Test/runTests.py +++ b/Test/runTests.py @@ -370,7 +370,7 @@ def run_tests(args): args.exclude + Defaults.ALWAYS_EXCLUDED, args.timeout)) tests.sort(key=operator.attrgetter("name")) - args.njobs = min(args.njobs or os.cpu_count() or 1, len(tests)) + args.njobs = max(1, min(args.njobs or os.cpu_count() or 1, len(tests))) debug(Debug.INFO, "\nRunning {} test(s) on {} testing thread(s), timeout is {:.2f}s, started at {}".format(len(tests), args.njobs, args.timeout, strftime("%H:%M:%S"))) try: -- cgit v1.2.3 From 82cd6194369a376e51a6b525e577f7cc8852ebef Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Mon, 20 Jul 2015 13:00:10 -0700 Subject: Split snapshot tests into separate files and add support for %S in runTests.py --- Test/dafny0/snapshots/Inputs/Snapshots0.v0.dfy | 8 + Test/dafny0/snapshots/Inputs/Snapshots0.v1.dfy | 8 + Test/dafny0/snapshots/Inputs/Snapshots1.v0.dfy | 13 ++ Test/dafny0/snapshots/Inputs/Snapshots1.v1.dfy | 13 ++ Test/dafny0/snapshots/Inputs/Snapshots2.v0.dfy | 19 +++ Test/dafny0/snapshots/Inputs/Snapshots2.v1.dfy | 19 +++ Test/dafny0/snapshots/Inputs/Snapshots3.v0.dfy | 11 ++ Test/dafny0/snapshots/Inputs/Snapshots3.v1.dfy | 11 ++ Test/dafny0/snapshots/Inputs/Snapshots4.v0.dfy | 11 ++ Test/dafny0/snapshots/Inputs/Snapshots4.v1.dfy | 12 ++ Test/dafny0/snapshots/Inputs/Snapshots5.v0.dfy | 26 +++ Test/dafny0/snapshots/Inputs/Snapshots5.v1.dfy | 27 +++ Test/dafny0/snapshots/Inputs/Snapshots6.v0.dfy | 23 +++ Test/dafny0/snapshots/Inputs/Snapshots6.v1.dfy | 23 +++ Test/dafny0/snapshots/Inputs/Snapshots7.v0.dfy | 22 +++ Test/dafny0/snapshots/Inputs/Snapshots7.v1.dfy | 22 +++ Test/dafny0/snapshots/Snapshots0.run.dfy | 2 + Test/dafny0/snapshots/Snapshots0.run.dfy.expect | 25 +++ Test/dafny0/snapshots/Snapshots0.v0.dfy | 8 - Test/dafny0/snapshots/Snapshots0.v1.dfy | 8 - Test/dafny0/snapshots/Snapshots1.run.dfy | 2 + Test/dafny0/snapshots/Snapshots1.run.dfy.expect | 21 +++ Test/dafny0/snapshots/Snapshots1.v0.dfy | 13 -- Test/dafny0/snapshots/Snapshots1.v1.dfy | 13 -- Test/dafny0/snapshots/Snapshots2.run.dfy | 2 + Test/dafny0/snapshots/Snapshots2.run.dfy.expect | 41 +++++ Test/dafny0/snapshots/Snapshots2.v0.dfy | 19 --- Test/dafny0/snapshots/Snapshots2.v1.dfy | 19 --- Test/dafny0/snapshots/Snapshots3.run.dfy | 2 + Test/dafny0/snapshots/Snapshots3.run.dfy.expect | 18 ++ Test/dafny0/snapshots/Snapshots3.v0.dfy | 11 -- Test/dafny0/snapshots/Snapshots3.v1.dfy | 11 -- Test/dafny0/snapshots/Snapshots4.run.dfy | 2 + Test/dafny0/snapshots/Snapshots4.run.dfy.expect | 20 +++ Test/dafny0/snapshots/Snapshots4.v0.dfy | 11 -- Test/dafny0/snapshots/Snapshots4.v1.dfy | 12 -- Test/dafny0/snapshots/Snapshots5.run.dfy | 2 + Test/dafny0/snapshots/Snapshots5.run.dfy.expect | 26 +++ Test/dafny0/snapshots/Snapshots5.v0.dfy | 26 --- Test/dafny0/snapshots/Snapshots5.v1.dfy | 27 --- Test/dafny0/snapshots/Snapshots6.run.dfy | 2 + Test/dafny0/snapshots/Snapshots6.run.dfy.expect | 11 ++ Test/dafny0/snapshots/Snapshots6.v0.dfy | 23 --- Test/dafny0/snapshots/Snapshots6.v1.dfy | 23 --- Test/dafny0/snapshots/Snapshots7.run.dfy | 2 + Test/dafny0/snapshots/Snapshots7.run.dfy.expect | 31 ++++ Test/dafny0/snapshots/Snapshots7.v0.dfy | 22 --- Test/dafny0/snapshots/Snapshots7.v1.dfy | 22 --- Test/dafny0/snapshots/lit.local.cfg | 5 - Test/dafny0/snapshots/runtest.snapshot | 2 - Test/dafny0/snapshots/runtest.snapshot.expect | 209 ------------------------ Test/lit.site.cfg | 2 +- Test/runTests.py | 4 +- 53 files changed, 481 insertions(+), 486 deletions(-) create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots0.v0.dfy create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots0.v1.dfy create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots1.v0.dfy create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots1.v1.dfy create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots2.v0.dfy create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots2.v1.dfy create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots3.v0.dfy create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots3.v1.dfy create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots4.v0.dfy create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots4.v1.dfy create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots5.v0.dfy create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots5.v1.dfy create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots6.v0.dfy create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots6.v1.dfy create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots7.v0.dfy create mode 100644 Test/dafny0/snapshots/Inputs/Snapshots7.v1.dfy create mode 100644 Test/dafny0/snapshots/Snapshots0.run.dfy create mode 100644 Test/dafny0/snapshots/Snapshots0.run.dfy.expect delete mode 100644 Test/dafny0/snapshots/Snapshots0.v0.dfy delete mode 100644 Test/dafny0/snapshots/Snapshots0.v1.dfy create mode 100644 Test/dafny0/snapshots/Snapshots1.run.dfy create mode 100644 Test/dafny0/snapshots/Snapshots1.run.dfy.expect delete mode 100644 Test/dafny0/snapshots/Snapshots1.v0.dfy delete mode 100644 Test/dafny0/snapshots/Snapshots1.v1.dfy create mode 100644 Test/dafny0/snapshots/Snapshots2.run.dfy create mode 100644 Test/dafny0/snapshots/Snapshots2.run.dfy.expect delete mode 100644 Test/dafny0/snapshots/Snapshots2.v0.dfy delete mode 100644 Test/dafny0/snapshots/Snapshots2.v1.dfy create mode 100644 Test/dafny0/snapshots/Snapshots3.run.dfy create mode 100644 Test/dafny0/snapshots/Snapshots3.run.dfy.expect delete mode 100644 Test/dafny0/snapshots/Snapshots3.v0.dfy delete mode 100644 Test/dafny0/snapshots/Snapshots3.v1.dfy create mode 100644 Test/dafny0/snapshots/Snapshots4.run.dfy create mode 100644 Test/dafny0/snapshots/Snapshots4.run.dfy.expect delete mode 100644 Test/dafny0/snapshots/Snapshots4.v0.dfy delete mode 100644 Test/dafny0/snapshots/Snapshots4.v1.dfy create mode 100644 Test/dafny0/snapshots/Snapshots5.run.dfy create mode 100644 Test/dafny0/snapshots/Snapshots5.run.dfy.expect delete mode 100644 Test/dafny0/snapshots/Snapshots5.v0.dfy delete mode 100644 Test/dafny0/snapshots/Snapshots5.v1.dfy create mode 100644 Test/dafny0/snapshots/Snapshots6.run.dfy create mode 100644 Test/dafny0/snapshots/Snapshots6.run.dfy.expect delete mode 100644 Test/dafny0/snapshots/Snapshots6.v0.dfy delete mode 100644 Test/dafny0/snapshots/Snapshots6.v1.dfy create mode 100644 Test/dafny0/snapshots/Snapshots7.run.dfy create mode 100644 Test/dafny0/snapshots/Snapshots7.run.dfy.expect delete mode 100644 Test/dafny0/snapshots/Snapshots7.v0.dfy delete mode 100644 Test/dafny0/snapshots/Snapshots7.v1.dfy delete mode 100644 Test/dafny0/snapshots/lit.local.cfg delete mode 100644 Test/dafny0/snapshots/runtest.snapshot delete mode 100644 Test/dafny0/snapshots/runtest.snapshot.expect (limited to 'Test/runTests.py') diff --git a/Test/dafny0/snapshots/Inputs/Snapshots0.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots0.v0.dfy new file mode 100644 index 00000000..73db9f9c --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots0.v0.dfy @@ -0,0 +1,8 @@ +method foo() +{ + bar(); + assert false; +} + +method bar() + ensures false; diff --git a/Test/dafny0/snapshots/Inputs/Snapshots0.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots0.v1.dfy new file mode 100644 index 00000000..db9fc01a --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots0.v1.dfy @@ -0,0 +1,8 @@ +method foo() +{ + bar(); + assert false; // error +} + +method bar() + ensures true; diff --git a/Test/dafny0/snapshots/Inputs/Snapshots1.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots1.v0.dfy new file mode 100644 index 00000000..34d066c3 --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots1.v0.dfy @@ -0,0 +1,13 @@ +method M() +{ + N(); + assert false; +} + +method N() + ensures P(); + +predicate P() +{ + false +} diff --git a/Test/dafny0/snapshots/Inputs/Snapshots1.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots1.v1.dfy new file mode 100644 index 00000000..184ac65d --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots1.v1.dfy @@ -0,0 +1,13 @@ +method M() +{ + N(); + assert false; // error +} + +method N() + ensures P(); + +predicate P() +{ + true +} diff --git a/Test/dafny0/snapshots/Inputs/Snapshots2.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots2.v0.dfy new file mode 100644 index 00000000..727e177d --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots2.v0.dfy @@ -0,0 +1,19 @@ +method M() +{ + N(); + assert false; +} + +method N() + ensures P(); + +predicate P() + ensures P() == Q(); + +predicate Q() + ensures Q() == R(); + +predicate R() +{ + false +} diff --git a/Test/dafny0/snapshots/Inputs/Snapshots2.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots2.v1.dfy new file mode 100644 index 00000000..02a91b52 --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots2.v1.dfy @@ -0,0 +1,19 @@ +method M() +{ + N(); + assert false; // error +} + +method N() + ensures P(); + +predicate P() + ensures P() == Q(); + +predicate Q() + ensures Q() == R(); + +predicate R() +{ + true +} diff --git a/Test/dafny0/snapshots/Inputs/Snapshots3.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots3.v0.dfy new file mode 100644 index 00000000..72607412 --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots3.v0.dfy @@ -0,0 +1,11 @@ +method M() +{ + if (*) + { + + } + else + { + assert 0 != 0; // error + } +} diff --git a/Test/dafny0/snapshots/Inputs/Snapshots3.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots3.v1.dfy new file mode 100644 index 00000000..3b186318 --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots3.v1.dfy @@ -0,0 +1,11 @@ +method M() +{ + if (*) + { + assert true; + } + else + { + assert 0 != 0; // error + } +} diff --git a/Test/dafny0/snapshots/Inputs/Snapshots4.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots4.v0.dfy new file mode 100644 index 00000000..beaadfeb --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots4.v0.dfy @@ -0,0 +1,11 @@ +method M() +{ + if (*) + { + + } + else + { + assert 0 == 0; + } +} diff --git a/Test/dafny0/snapshots/Inputs/Snapshots4.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots4.v1.dfy new file mode 100644 index 00000000..cf9ae753 --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots4.v1.dfy @@ -0,0 +1,12 @@ +method M() +{ + if (*) + { + assert 1 != 1; // error + } + else + { + assert 0 == 0; + assert 2 != 2; // error + } +} diff --git a/Test/dafny0/snapshots/Inputs/Snapshots5.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots5.v0.dfy new file mode 100644 index 00000000..b81c1a2b --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots5.v0.dfy @@ -0,0 +1,26 @@ +method M() +{ + N(); + if (*) + { + + } + else + { + assert (forall b: bool :: b || !b) || 0 != 0; + } + N(); + assert (forall b: bool :: b || !b) || 3 != 3; + if (*) + { + + } + else + { + assert (forall b: bool :: b || !b) || 1 != 1; + } +} + + +method N() + ensures (forall b: bool :: b || !b) || 2 != 2; diff --git a/Test/dafny0/snapshots/Inputs/Snapshots5.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots5.v1.dfy new file mode 100644 index 00000000..05dbced0 --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots5.v1.dfy @@ -0,0 +1,27 @@ +method M() +{ + N(); + if (*) + { + + } + else + { + assert (forall b: bool :: b || !b) || 0 != 0; + } + N(); + assert (forall b: bool :: b || !b) || 3 != 3; + if (*) + { + + } + else + { + assert (exists b: bool :: b || !b) || 4 != 4; + } + assert (exists b: bool :: b || !b) || 5 != 5; +} + + +method N() + ensures (forall b: bool :: b || !b) || 2 != 2; diff --git a/Test/dafny0/snapshots/Inputs/Snapshots6.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots6.v0.dfy new file mode 100644 index 00000000..c3742f4b --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots6.v0.dfy @@ -0,0 +1,23 @@ +module M0 +{ + class C + { + method Foo() + { + assume false; + } + } +} + + +module M1 refines M0 +{ + class C + { + method Foo() + { + ...; + assert false; + } + } +} diff --git a/Test/dafny0/snapshots/Inputs/Snapshots6.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots6.v1.dfy new file mode 100644 index 00000000..aeb520cb --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots6.v1.dfy @@ -0,0 +1,23 @@ +module M0 +{ + class C + { + method Foo() + { + assume true; + } + } +} + + +module M1 refines M0 +{ + class C + { + method Foo() + { + ...; + assert false; + } + } +} diff --git a/Test/dafny0/snapshots/Inputs/Snapshots7.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots7.v0.dfy new file mode 100644 index 00000000..27c7da5f --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots7.v0.dfy @@ -0,0 +1,22 @@ +module M0 +{ + class C + { + method Foo() + requires false; + { + } + } +} + + +module M1 refines M0 +{ + class C + { + method Foo... + { + assert false; + } + } +} diff --git a/Test/dafny0/snapshots/Inputs/Snapshots7.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots7.v1.dfy new file mode 100644 index 00000000..b45dfe78 --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots7.v1.dfy @@ -0,0 +1,22 @@ +module M0 +{ + class C + { + method Foo() + requires true; + { + } + } +} + + +module M1 refines M0 +{ + class C + { + method Foo... + { + assert false; + } + } +} diff --git a/Test/dafny0/snapshots/Snapshots0.run.dfy b/Test/dafny0/snapshots/Snapshots0.run.dfy new file mode 100644 index 00000000..cb96468e --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots0.run.dfy @@ -0,0 +1,2 @@ +// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots0.dfy > "%t" +// RUN: %diff "%s.expect" "%t" diff --git a/Test/dafny0/snapshots/Snapshots0.run.dfy.expect b/Test/dafny0/snapshots/Snapshots0.run.dfy.expect new file mode 100644 index 00000000..96c280d9 --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots0.run.dfy.expect @@ -0,0 +1,25 @@ +Processing command (at Snapshots0.v0.dfy(3,6)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); + >>> DoNothingToAssert +Processing command (at Snapshots0.v0.dfy(4,10)) assert Lit(false); + >>> DoNothingToAssert + +Dafny program verifier finished with 3 verified, 0 errors +Processing implementation CheckWellformed$$_module.__default.bar (at Snapshots0.v1.dfy(7,8)): + >>> added axiom: ##extracted_function##1() == (0 == $ModuleContextHeight && 0 == $FunctionContextHeight) + >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##1(); +Processing call to procedure IntraModuleCall$$_module.__default.bar in implementation Impl$$_module.__default.foo (at Snapshots0.v1.dfy(3,6)): + >>> added axiom: (forall call0old#AT#$Heap: Heap, $Heap: Heap :: {:weight 30} { ##extracted_function##2(call0old#AT#$Heap, $Heap) } ##extracted_function##2(call0old#AT#$Heap, $Heap) == (true && Lit(false) && (forall $o: ref, $f: Field alpha :: { read($Heap, $o, $f) } $o != null && read(call0old#AT#$Heap, $o, alloc) ==> read($Heap, $o, $f) == read(call0old#AT#$Heap, $o, $f)) && $HeapSucc(call0old#AT#$Heap, $Heap))) + >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call0old#AT#$Heap, $Heap); +Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##1(); + >>> AssumeNegationOfAssumptionVariable +Processing command (at Snapshots0.v1.dfy(3,6)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); + >>> MarkAsFullyVerified +Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##2(call0old#AT#$Heap, $Heap); + >>> AssumeNegationOfAssumptionVariable +Processing command (at Snapshots0.v1.dfy(4,10)) assert Lit(false); + >>> MarkAsPartiallyVerified +Snapshots0.v1.dfy(4,10): Error: assertion violation +Execution trace: + (0,0): anon0 + +Dafny program verifier finished with 2 verified, 1 error diff --git a/Test/dafny0/snapshots/Snapshots0.v0.dfy b/Test/dafny0/snapshots/Snapshots0.v0.dfy deleted file mode 100644 index 73db9f9c..00000000 --- a/Test/dafny0/snapshots/Snapshots0.v0.dfy +++ /dev/null @@ -1,8 +0,0 @@ -method foo() -{ - bar(); - assert false; -} - -method bar() - ensures false; diff --git a/Test/dafny0/snapshots/Snapshots0.v1.dfy b/Test/dafny0/snapshots/Snapshots0.v1.dfy deleted file mode 100644 index db9fc01a..00000000 --- a/Test/dafny0/snapshots/Snapshots0.v1.dfy +++ /dev/null @@ -1,8 +0,0 @@ -method foo() -{ - bar(); - assert false; // error -} - -method bar() - ensures true; diff --git a/Test/dafny0/snapshots/Snapshots1.run.dfy b/Test/dafny0/snapshots/Snapshots1.run.dfy new file mode 100644 index 00000000..7c277b3e --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots1.run.dfy @@ -0,0 +1,2 @@ +// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots1.dfy > "%t" +// RUN: %diff "%s.expect" "%t" diff --git a/Test/dafny0/snapshots/Snapshots1.run.dfy.expect b/Test/dafny0/snapshots/Snapshots1.run.dfy.expect new file mode 100644 index 00000000..878f9905 --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots1.run.dfy.expect @@ -0,0 +1,21 @@ +Processing command (at Snapshots1.v0.dfy(3,4)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); + >>> DoNothingToAssert +Processing command (at Snapshots1.v0.dfy(4,10)) assert Lit(false); + >>> DoNothingToAssert +Processing command (at Snapshots1.v0.dfy(12,3)) assert true; + >>> DoNothingToAssert + +Dafny program verifier finished with 4 verified, 0 errors +Processing call to procedure IntraModuleCall$$_module.__default.N in implementation Impl$$_module.__default.M (at Snapshots1.v1.dfy(3,4)): + >>> added after: a##cached##0 := a##cached##0 && false; +Processing command (at Snapshots1.v1.dfy(12,3)) assert true; + >>> MarkAsFullyVerified +Processing command (at Snapshots1.v1.dfy(3,4)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); + >>> MarkAsFullyVerified +Processing command (at Snapshots1.v1.dfy(4,10)) assert Lit(false); + >>> DoNothingToAssert +Snapshots1.v1.dfy(4,10): Error: assertion violation +Execution trace: + (0,0): anon0 + +Dafny program verifier finished with 3 verified, 1 error diff --git a/Test/dafny0/snapshots/Snapshots1.v0.dfy b/Test/dafny0/snapshots/Snapshots1.v0.dfy deleted file mode 100644 index 34d066c3..00000000 --- a/Test/dafny0/snapshots/Snapshots1.v0.dfy +++ /dev/null @@ -1,13 +0,0 @@ -method M() -{ - N(); - assert false; -} - -method N() - ensures P(); - -predicate P() -{ - false -} diff --git a/Test/dafny0/snapshots/Snapshots1.v1.dfy b/Test/dafny0/snapshots/Snapshots1.v1.dfy deleted file mode 100644 index 184ac65d..00000000 --- a/Test/dafny0/snapshots/Snapshots1.v1.dfy +++ /dev/null @@ -1,13 +0,0 @@ -method M() -{ - N(); - assert false; // error -} - -method N() - ensures P(); - -predicate P() -{ - true -} diff --git a/Test/dafny0/snapshots/Snapshots2.run.dfy b/Test/dafny0/snapshots/Snapshots2.run.dfy new file mode 100644 index 00000000..889a8153 --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots2.run.dfy @@ -0,0 +1,2 @@ +// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots2.dfy > "%t" +// RUN: %diff "%s.expect" "%t" diff --git a/Test/dafny0/snapshots/Snapshots2.run.dfy.expect b/Test/dafny0/snapshots/Snapshots2.run.dfy.expect new file mode 100644 index 00000000..a6a9bc4c --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots2.run.dfy.expect @@ -0,0 +1,41 @@ +Processing command (at Snapshots2.v0.dfy(3,4)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); + >>> DoNothingToAssert +Processing command (at Snapshots2.v0.dfy(4,10)) assert Lit(false); + >>> DoNothingToAssert +Processing command (at Snapshots2.v0.dfy(11,11)) assert true; + >>> DoNothingToAssert +Processing command (at Snapshots2.v0.dfy(11,15)) assert _module.__default.P($LS($LS($LZ)), $Heap) <==> _module.__default.Q($LS($LS($LZ)), $Heap); + >>> DoNothingToAssert +Processing command (at Snapshots2.v0.dfy(14,11)) assert true; + >>> DoNothingToAssert +Processing command (at Snapshots2.v0.dfy(14,15)) assert _module.__default.Q($LS($LS($LZ)), $Heap) <==> Lit(_module.__default.R($Heap)); + >>> DoNothingToAssert +Processing command (at Snapshots2.v0.dfy(18,3)) assert true; + >>> DoNothingToAssert + +Dafny program verifier finished with 6 verified, 0 errors +Processing call to procedure IntraModuleCall$$_module.__default.N in implementation Impl$$_module.__default.M (at Snapshots2.v1.dfy(3,4)): + >>> added after: a##cached##0 := a##cached##0 && false; +Processing implementation CheckWellformed$$_module.__default.P (at Snapshots2.v1.dfy(10,11)): + >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false; +Processing implementation CheckWellformed$$_module.__default.Q (at Snapshots2.v1.dfy(13,11)): + >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false; +Processing command (at Snapshots2.v1.dfy(18,3)) assert true; + >>> MarkAsFullyVerified +Processing command (at Snapshots2.v1.dfy(3,4)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); + >>> MarkAsFullyVerified +Processing command (at Snapshots2.v1.dfy(4,10)) assert Lit(false); + >>> DoNothingToAssert +Snapshots2.v1.dfy(4,10): Error: assertion violation +Execution trace: + (0,0): anon0 +Processing command (at Snapshots2.v1.dfy(11,11)) assert true; + >>> DoNothingToAssert +Processing command (at Snapshots2.v1.dfy(11,15)) assert _module.__default.P($LS($LS($LZ)), $Heap) <==> _module.__default.Q($LS($LS($LZ)), $Heap); + >>> DoNothingToAssert +Processing command (at Snapshots2.v1.dfy(14,11)) assert true; + >>> DoNothingToAssert +Processing command (at Snapshots2.v1.dfy(14,15)) assert _module.__default.Q($LS($LS($LZ)), $Heap) <==> Lit(_module.__default.R($Heap)); + >>> DoNothingToAssert + +Dafny program verifier finished with 5 verified, 1 error diff --git a/Test/dafny0/snapshots/Snapshots2.v0.dfy b/Test/dafny0/snapshots/Snapshots2.v0.dfy deleted file mode 100644 index 727e177d..00000000 --- a/Test/dafny0/snapshots/Snapshots2.v0.dfy +++ /dev/null @@ -1,19 +0,0 @@ -method M() -{ - N(); - assert false; -} - -method N() - ensures P(); - -predicate P() - ensures P() == Q(); - -predicate Q() - ensures Q() == R(); - -predicate R() -{ - false -} diff --git a/Test/dafny0/snapshots/Snapshots2.v1.dfy b/Test/dafny0/snapshots/Snapshots2.v1.dfy deleted file mode 100644 index 02a91b52..00000000 --- a/Test/dafny0/snapshots/Snapshots2.v1.dfy +++ /dev/null @@ -1,19 +0,0 @@ -method M() -{ - N(); - assert false; // error -} - -method N() - ensures P(); - -predicate P() - ensures P() == Q(); - -predicate Q() - ensures Q() == R(); - -predicate R() -{ - true -} diff --git a/Test/dafny0/snapshots/Snapshots3.run.dfy b/Test/dafny0/snapshots/Snapshots3.run.dfy new file mode 100644 index 00000000..3df182d6 --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots3.run.dfy @@ -0,0 +1,2 @@ +// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots3.dfy > "%t" +// RUN: %diff "%s.expect" "%t" diff --git a/Test/dafny0/snapshots/Snapshots3.run.dfy.expect b/Test/dafny0/snapshots/Snapshots3.run.dfy.expect new file mode 100644 index 00000000..07e2d063 --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots3.run.dfy.expect @@ -0,0 +1,18 @@ +Processing command (at Snapshots3.v0.dfy(9,14)) assert Lit(0 != 0); + >>> DoNothingToAssert +Snapshots3.v0.dfy(9,14): Error: assertion violation +Execution trace: + (0,0): anon0 + (0,0): anon3_Else + +Dafny program verifier finished with 1 verified, 1 error +Processing command (at Snapshots3.v1.dfy(5,12)) assert Lit(true); + >>> DoNothingToAssert +Processing command (at Snapshots3.v1.dfy(9,14)) assert Lit(0 != 0); + >>> RecycleError +Snapshots3.v0.dfy(9,14): Error: assertion violation +Execution trace: + (0,0): anon0 + (0,0): anon3_Else + +Dafny program verifier finished with 1 verified, 1 error diff --git a/Test/dafny0/snapshots/Snapshots3.v0.dfy b/Test/dafny0/snapshots/Snapshots3.v0.dfy deleted file mode 100644 index 72607412..00000000 --- a/Test/dafny0/snapshots/Snapshots3.v0.dfy +++ /dev/null @@ -1,11 +0,0 @@ -method M() -{ - if (*) - { - - } - else - { - assert 0 != 0; // error - } -} diff --git a/Test/dafny0/snapshots/Snapshots3.v1.dfy b/Test/dafny0/snapshots/Snapshots3.v1.dfy deleted file mode 100644 index 3b186318..00000000 --- a/Test/dafny0/snapshots/Snapshots3.v1.dfy +++ /dev/null @@ -1,11 +0,0 @@ -method M() -{ - if (*) - { - assert true; - } - else - { - assert 0 != 0; // error - } -} diff --git a/Test/dafny0/snapshots/Snapshots4.run.dfy b/Test/dafny0/snapshots/Snapshots4.run.dfy new file mode 100644 index 00000000..fd6bef41 --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots4.run.dfy @@ -0,0 +1,2 @@ +// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots4.dfy > "%t" +// RUN: %diff "%s.expect" "%t" diff --git a/Test/dafny0/snapshots/Snapshots4.run.dfy.expect b/Test/dafny0/snapshots/Snapshots4.run.dfy.expect new file mode 100644 index 00000000..fdc97775 --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots4.run.dfy.expect @@ -0,0 +1,20 @@ +Processing command (at Snapshots4.v0.dfy(9,14)) assert LitInt(0) == LitInt(0); + >>> DoNothingToAssert + +Dafny program verifier finished with 2 verified, 0 errors +Processing command (at Snapshots4.v1.dfy(5,14)) assert Lit(1 != 1); + >>> DoNothingToAssert +Processing command (at Snapshots4.v1.dfy(9,14)) assert LitInt(0) == LitInt(0); + >>> MarkAsFullyVerified +Processing command (at Snapshots4.v1.dfy(10,14)) assert Lit(2 != 2); + >>> DoNothingToAssert +Snapshots4.v1.dfy(5,14): Error: assertion violation +Execution trace: + (0,0): anon0 + (0,0): anon3_Then +Snapshots4.v1.dfy(10,14): Error: assertion violation +Execution trace: + (0,0): anon0 + (0,0): anon3_Else + +Dafny program verifier finished with 1 verified, 2 errors diff --git a/Test/dafny0/snapshots/Snapshots4.v0.dfy b/Test/dafny0/snapshots/Snapshots4.v0.dfy deleted file mode 100644 index beaadfeb..00000000 --- a/Test/dafny0/snapshots/Snapshots4.v0.dfy +++ /dev/null @@ -1,11 +0,0 @@ -method M() -{ - if (*) - { - - } - else - { - assert 0 == 0; - } -} diff --git a/Test/dafny0/snapshots/Snapshots4.v1.dfy b/Test/dafny0/snapshots/Snapshots4.v1.dfy deleted file mode 100644 index cf9ae753..00000000 --- a/Test/dafny0/snapshots/Snapshots4.v1.dfy +++ /dev/null @@ -1,12 +0,0 @@ -method M() -{ - if (*) - { - assert 1 != 1; // error - } - else - { - assert 0 == 0; - assert 2 != 2; // error - } -} diff --git a/Test/dafny0/snapshots/Snapshots5.run.dfy b/Test/dafny0/snapshots/Snapshots5.run.dfy new file mode 100644 index 00000000..4f26aac4 --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots5.run.dfy @@ -0,0 +1,2 @@ +// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots5.dfy > "%t" +// RUN: %diff "%s.expect" "%t" diff --git a/Test/dafny0/snapshots/Snapshots5.run.dfy.expect b/Test/dafny0/snapshots/Snapshots5.run.dfy.expect new file mode 100644 index 00000000..2ad73416 --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots5.run.dfy.expect @@ -0,0 +1,26 @@ +Processing command (at Snapshots5.v0.dfy(3,4)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); + >>> DoNothingToAssert +Processing command (at Snapshots5.v0.dfy(10,40)) assert (forall b#1: bool :: true ==> b#1 || !b#1) || 0 != 0; + >>> DoNothingToAssert +Processing command (at Snapshots5.v0.dfy(12,4)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); + >>> DoNothingToAssert +Processing command (at Snapshots5.v0.dfy(13,38)) assert (forall b#3: bool :: true ==> b#3 || !b#3) || 3 != 3; + >>> DoNothingToAssert +Processing command (at Snapshots5.v0.dfy(20,40)) assert (forall b#5: bool :: true ==> b#5 || !b#5) || 1 != 1; + >>> DoNothingToAssert + +Dafny program verifier finished with 3 verified, 0 errors +Processing command (at Snapshots5.v1.dfy(3,4)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); + >>> MarkAsFullyVerified +Processing command (at Snapshots5.v1.dfy(10,40)) assert (forall b#1: bool :: true ==> b#1 || !b#1) || 0 != 0; + >>> MarkAsFullyVerified +Processing command (at Snapshots5.v1.dfy(12,4)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); + >>> MarkAsFullyVerified +Processing command (at Snapshots5.v1.dfy(13,38)) assert (forall b#3: bool :: true ==> b#3 || !b#3) || 3 != 3; + >>> MarkAsFullyVerified +Processing command (at Snapshots5.v1.dfy(20,40)) assert (exists b#5: bool :: b#5 || !b#5) || 4 != 4; + >>> DoNothingToAssert +Processing command (at Snapshots5.v1.dfy(22,38)) assert (exists b#7: bool :: b#7 || !b#7) || 5 != 5; + >>> DoNothingToAssert + +Dafny program verifier finished with 3 verified, 0 errors diff --git a/Test/dafny0/snapshots/Snapshots5.v0.dfy b/Test/dafny0/snapshots/Snapshots5.v0.dfy deleted file mode 100644 index b81c1a2b..00000000 --- a/Test/dafny0/snapshots/Snapshots5.v0.dfy +++ /dev/null @@ -1,26 +0,0 @@ -method M() -{ - N(); - if (*) - { - - } - else - { - assert (forall b: bool :: b || !b) || 0 != 0; - } - N(); - assert (forall b: bool :: b || !b) || 3 != 3; - if (*) - { - - } - else - { - assert (forall b: bool :: b || !b) || 1 != 1; - } -} - - -method N() - ensures (forall b: bool :: b || !b) || 2 != 2; diff --git a/Test/dafny0/snapshots/Snapshots5.v1.dfy b/Test/dafny0/snapshots/Snapshots5.v1.dfy deleted file mode 100644 index 05dbced0..00000000 --- a/Test/dafny0/snapshots/Snapshots5.v1.dfy +++ /dev/null @@ -1,27 +0,0 @@ -method M() -{ - N(); - if (*) - { - - } - else - { - assert (forall b: bool :: b || !b) || 0 != 0; - } - N(); - assert (forall b: bool :: b || !b) || 3 != 3; - if (*) - { - - } - else - { - assert (exists b: bool :: b || !b) || 4 != 4; - } - assert (exists b: bool :: b || !b) || 5 != 5; -} - - -method N() - ensures (forall b: bool :: b || !b) || 2 != 2; diff --git a/Test/dafny0/snapshots/Snapshots6.run.dfy b/Test/dafny0/snapshots/Snapshots6.run.dfy new file mode 100644 index 00000000..157fc5b7 --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots6.run.dfy @@ -0,0 +1,2 @@ +// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots6.dfy > "%t" +// RUN: %diff "%s.expect" "%t" diff --git a/Test/dafny0/snapshots/Snapshots6.run.dfy.expect b/Test/dafny0/snapshots/Snapshots6.run.dfy.expect new file mode 100644 index 00000000..af440327 --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots6.run.dfy.expect @@ -0,0 +1,11 @@ +Processing command (at Snapshots6.v0.dfy(20,14)) assert Lit(false); + >>> DoNothingToAssert + +Dafny program verifier finished with 4 verified, 0 errors +Processing command (at Snapshots6.v1.dfy(20,14)) assert Lit(false); + >>> DoNothingToAssert +Snapshots6.v1.dfy(20,14): Error: assertion violation +Execution trace: + (0,0): anon0 + +Dafny program verifier finished with 3 verified, 1 error diff --git a/Test/dafny0/snapshots/Snapshots6.v0.dfy b/Test/dafny0/snapshots/Snapshots6.v0.dfy deleted file mode 100644 index c3742f4b..00000000 --- a/Test/dafny0/snapshots/Snapshots6.v0.dfy +++ /dev/null @@ -1,23 +0,0 @@ -module M0 -{ - class C - { - method Foo() - { - assume false; - } - } -} - - -module M1 refines M0 -{ - class C - { - method Foo() - { - ...; - assert false; - } - } -} diff --git a/Test/dafny0/snapshots/Snapshots6.v1.dfy b/Test/dafny0/snapshots/Snapshots6.v1.dfy deleted file mode 100644 index aeb520cb..00000000 --- a/Test/dafny0/snapshots/Snapshots6.v1.dfy +++ /dev/null @@ -1,23 +0,0 @@ -module M0 -{ - class C - { - method Foo() - { - assume true; - } - } -} - - -module M1 refines M0 -{ - class C - { - method Foo() - { - ...; - assert false; - } - } -} diff --git a/Test/dafny0/snapshots/Snapshots7.run.dfy b/Test/dafny0/snapshots/Snapshots7.run.dfy new file mode 100644 index 00000000..b192f090 --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots7.run.dfy @@ -0,0 +1,2 @@ +// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots7.dfy > "%t" +// RUN: %diff "%s.expect" "%t" diff --git a/Test/dafny0/snapshots/Snapshots7.run.dfy.expect b/Test/dafny0/snapshots/Snapshots7.run.dfy.expect new file mode 100644 index 00000000..7c073a9a --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots7.run.dfy.expect @@ -0,0 +1,31 @@ +Processing command (at Snapshots7.v0.dfy(19,14)) assert Lit(false); + >>> DoNothingToAssert + +Dafny program verifier finished with 4 verified, 0 errors +Processing implementation CheckWellformed$$_0_M0.C.Foo (at Snapshots7.v1.dfy(5,12)): + >>> added axiom: ##extracted_function##1() == (0 == $ModuleContextHeight && 0 == $FunctionContextHeight) + >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##1(); +Processing implementation Impl$$_0_M0.C.Foo (at Snapshots7.v1.dfy(5,12)): + >>> added axiom: ##extracted_function##2() == (0 == $ModuleContextHeight && 0 == $FunctionContextHeight && Lit(false)) + >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##2(); +Processing implementation CheckWellformed$$_1_M1.C.Foo (at Snapshots7.v1.dfy[M1](5,12)): + >>> added axiom: ##extracted_function##3() == (1 == $ModuleContextHeight && 0 == $FunctionContextHeight) + >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##3(); +Processing implementation Impl$$_1_M1.C.Foo (at Snapshots7.v1.dfy[M1](5,12)): + >>> added axiom: ##extracted_function##4() == (1 == $ModuleContextHeight && 0 == $FunctionContextHeight && Lit(false)) + >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##4(); +Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##1(); + >>> AssumeNegationOfAssumptionVariable +Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##2(); + >>> AssumeNegationOfAssumptionVariable +Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##3(); + >>> AssumeNegationOfAssumptionVariable +Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##4(); + >>> AssumeNegationOfAssumptionVariable +Processing command (at Snapshots7.v1.dfy(19,14)) assert Lit(false); + >>> MarkAsPartiallyVerified +Snapshots7.v1.dfy(19,14): Error: assertion violation +Execution trace: + (0,0): anon0 + +Dafny program verifier finished with 3 verified, 1 error diff --git a/Test/dafny0/snapshots/Snapshots7.v0.dfy b/Test/dafny0/snapshots/Snapshots7.v0.dfy deleted file mode 100644 index 27c7da5f..00000000 --- a/Test/dafny0/snapshots/Snapshots7.v0.dfy +++ /dev/null @@ -1,22 +0,0 @@ -module M0 -{ - class C - { - method Foo() - requires false; - { - } - } -} - - -module M1 refines M0 -{ - class C - { - method Foo... - { - assert false; - } - } -} diff --git a/Test/dafny0/snapshots/Snapshots7.v1.dfy b/Test/dafny0/snapshots/Snapshots7.v1.dfy deleted file mode 100644 index b45dfe78..00000000 --- a/Test/dafny0/snapshots/Snapshots7.v1.dfy +++ /dev/null @@ -1,22 +0,0 @@ -module M0 -{ - class C - { - method Foo() - requires true; - { - } - } -} - - -module M1 refines M0 -{ - class C - { - method Foo... - { - assert false; - } - } -} diff --git a/Test/dafny0/snapshots/lit.local.cfg b/Test/dafny0/snapshots/lit.local.cfg deleted file mode 100644 index 07cb869f..00000000 --- a/Test/dafny0/snapshots/lit.local.cfg +++ /dev/null @@ -1,5 +0,0 @@ -# This test is unusual in that we don't use the .bpl files -# directly on the command line. So instead we'll invoke -# files in this directory with extension '.snapshot'. There -# will only be one for now -config.suffixes = ['.snapshot'] diff --git a/Test/dafny0/snapshots/runtest.snapshot b/Test/dafny0/snapshots/runtest.snapshot deleted file mode 100644 index 62ccabb3..00000000 --- a/Test/dafny0/snapshots/runtest.snapshot +++ /dev/null @@ -1,2 +0,0 @@ -// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 /verifySeparately Snapshots0.dfy Snapshots1.dfy Snapshots2.dfy Snapshots3.dfy Snapshots4.dfy Snapshots5.dfy Snapshots6.dfy Snapshots7.dfy > "%t" -// RUN: %diff "%s.expect" "%t" diff --git a/Test/dafny0/snapshots/runtest.snapshot.expect b/Test/dafny0/snapshots/runtest.snapshot.expect deleted file mode 100644 index f1050f62..00000000 --- a/Test/dafny0/snapshots/runtest.snapshot.expect +++ /dev/null @@ -1,209 +0,0 @@ - --------------------- Snapshots0.dfy -------------------- -Processing command (at Snapshots0.v0.dfy(3,6)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); - >>> DoNothingToAssert -Processing command (at Snapshots0.v0.dfy(4,10)) assert Lit(false); - >>> DoNothingToAssert - -Dafny program verifier finished with 3 verified, 0 errors -Processing implementation CheckWellformed$$_module.__default.bar (at Snapshots0.v1.dfy(7,8)): - >>> added axiom: ##extracted_function##1() == (0 == $ModuleContextHeight && 0 == $FunctionContextHeight) - >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##1(); -Processing call to procedure IntraModuleCall$$_module.__default.bar in implementation Impl$$_module.__default.foo (at Snapshots0.v1.dfy(3,6)): - >>> added axiom: (forall call0old#AT#$Heap: Heap, $Heap: Heap :: {:weight 30} { ##extracted_function##2(call0old#AT#$Heap, $Heap) } ##extracted_function##2(call0old#AT#$Heap, $Heap) == (true && Lit(false) && (forall $o: ref, $f: Field alpha :: { read($Heap, $o, $f) } $o != null && read(call0old#AT#$Heap, $o, alloc) ==> read($Heap, $o, $f) == read(call0old#AT#$Heap, $o, $f)) && $HeapSucc(call0old#AT#$Heap, $Heap))) - >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call0old#AT#$Heap, $Heap); -Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##1(); - >>> AssumeNegationOfAssumptionVariable -Processing command (at Snapshots0.v1.dfy(3,6)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); - >>> MarkAsFullyVerified -Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##2(call0old#AT#$Heap, $Heap); - >>> AssumeNegationOfAssumptionVariable -Processing command (at Snapshots0.v1.dfy(4,10)) assert Lit(false); - >>> MarkAsPartiallyVerified -Snapshots0.v1.dfy(4,10): Error: assertion violation -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 2 verified, 1 error - --------------------- Snapshots1.dfy -------------------- -Processing command (at Snapshots1.v0.dfy(3,4)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); - >>> DoNothingToAssert -Processing command (at Snapshots1.v0.dfy(4,10)) assert Lit(false); - >>> DoNothingToAssert -Processing command (at Snapshots1.v0.dfy(12,3)) assert true; - >>> DoNothingToAssert - -Dafny program verifier finished with 4 verified, 0 errors -Processing call to procedure IntraModuleCall$$_module.__default.N in implementation Impl$$_module.__default.M (at Snapshots1.v1.dfy(3,4)): - >>> added after: a##cached##0 := a##cached##0 && false; -Processing command (at Snapshots1.v1.dfy(12,3)) assert true; - >>> MarkAsFullyVerified -Processing command (at Snapshots1.v1.dfy(3,4)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); - >>> MarkAsFullyVerified -Processing command (at Snapshots1.v1.dfy(4,10)) assert Lit(false); - >>> DoNothingToAssert -Snapshots1.v1.dfy(4,10): Error: assertion violation -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 3 verified, 1 error - --------------------- Snapshots2.dfy -------------------- -Processing command (at Snapshots2.v0.dfy(3,4)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); - >>> DoNothingToAssert -Processing command (at Snapshots2.v0.dfy(4,10)) assert Lit(false); - >>> DoNothingToAssert -Processing command (at Snapshots2.v0.dfy(11,11)) assert true; - >>> DoNothingToAssert -Processing command (at Snapshots2.v0.dfy(11,15)) assert _module.__default.P($LS($LS($LZ)), $Heap) <==> _module.__default.Q($LS($LS($LZ)), $Heap); - >>> DoNothingToAssert -Processing command (at Snapshots2.v0.dfy(14,11)) assert true; - >>> DoNothingToAssert -Processing command (at Snapshots2.v0.dfy(14,15)) assert _module.__default.Q($LS($LS($LZ)), $Heap) <==> Lit(_module.__default.R($Heap)); - >>> DoNothingToAssert -Processing command (at Snapshots2.v0.dfy(18,3)) assert true; - >>> DoNothingToAssert - -Dafny program verifier finished with 6 verified, 0 errors -Processing call to procedure IntraModuleCall$$_module.__default.N in implementation Impl$$_module.__default.M (at Snapshots2.v1.dfy(3,4)): - >>> added after: a##cached##0 := a##cached##0 && false; -Processing implementation CheckWellformed$$_module.__default.P (at Snapshots2.v1.dfy(10,11)): - >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false; -Processing implementation CheckWellformed$$_module.__default.Q (at Snapshots2.v1.dfy(13,11)): - >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false; -Processing command (at Snapshots2.v1.dfy(18,3)) assert true; - >>> MarkAsFullyVerified -Processing command (at Snapshots2.v1.dfy(3,4)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); - >>> MarkAsFullyVerified -Processing command (at Snapshots2.v1.dfy(4,10)) assert Lit(false); - >>> DoNothingToAssert -Snapshots2.v1.dfy(4,10): Error: assertion violation -Execution trace: - (0,0): anon0 -Processing command (at Snapshots2.v1.dfy(11,11)) assert true; - >>> DoNothingToAssert -Processing command (at Snapshots2.v1.dfy(11,15)) assert _module.__default.P($LS($LS($LZ)), $Heap) <==> _module.__default.Q($LS($LS($LZ)), $Heap); - >>> DoNothingToAssert -Processing command (at Snapshots2.v1.dfy(14,11)) assert true; - >>> DoNothingToAssert -Processing command (at Snapshots2.v1.dfy(14,15)) assert _module.__default.Q($LS($LS($LZ)), $Heap) <==> Lit(_module.__default.R($Heap)); - >>> DoNothingToAssert - -Dafny program verifier finished with 5 verified, 1 error - --------------------- Snapshots3.dfy -------------------- -Processing command (at Snapshots3.v0.dfy(9,14)) assert Lit(0 != 0); - >>> DoNothingToAssert -Snapshots3.v0.dfy(9,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Else - -Dafny program verifier finished with 1 verified, 1 error -Processing command (at Snapshots3.v1.dfy(5,12)) assert Lit(true); - >>> DoNothingToAssert -Processing command (at Snapshots3.v1.dfy(9,14)) assert Lit(0 != 0); - >>> RecycleError -Snapshots3.v0.dfy(9,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Else - -Dafny program verifier finished with 1 verified, 1 error - --------------------- Snapshots4.dfy -------------------- -Processing command (at Snapshots4.v0.dfy(9,14)) assert LitInt(0) == LitInt(0); - >>> DoNothingToAssert - -Dafny program verifier finished with 2 verified, 0 errors -Processing command (at Snapshots4.v1.dfy(5,14)) assert Lit(1 != 1); - >>> DoNothingToAssert -Processing command (at Snapshots4.v1.dfy(9,14)) assert LitInt(0) == LitInt(0); - >>> MarkAsFullyVerified -Processing command (at Snapshots4.v1.dfy(10,14)) assert Lit(2 != 2); - >>> DoNothingToAssert -Snapshots4.v1.dfy(5,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -Snapshots4.v1.dfy(10,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Else - -Dafny program verifier finished with 1 verified, 2 errors - --------------------- Snapshots5.dfy -------------------- -Processing command (at Snapshots5.v0.dfy(3,4)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); - >>> DoNothingToAssert -Processing command (at Snapshots5.v0.dfy(10,40)) assert (forall b#1: bool :: true ==> b#1 || !b#1) || 0 != 0; - >>> DoNothingToAssert -Processing command (at Snapshots5.v0.dfy(12,4)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); - >>> DoNothingToAssert -Processing command (at Snapshots5.v0.dfy(13,38)) assert (forall b#3: bool :: true ==> b#3 || !b#3) || 3 != 3; - >>> DoNothingToAssert -Processing command (at Snapshots5.v0.dfy(20,40)) assert (forall b#5: bool :: true ==> b#5 || !b#5) || 1 != 1; - >>> DoNothingToAssert - -Dafny program verifier finished with 3 verified, 0 errors -Processing command (at Snapshots5.v1.dfy(3,4)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); - >>> MarkAsFullyVerified -Processing command (at Snapshots5.v1.dfy(10,40)) assert (forall b#1: bool :: true ==> b#1 || !b#1) || 0 != 0; - >>> MarkAsFullyVerified -Processing command (at Snapshots5.v1.dfy(12,4)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); - >>> MarkAsFullyVerified -Processing command (at Snapshots5.v1.dfy(13,38)) assert (forall b#3: bool :: true ==> b#3 || !b#3) || 3 != 3; - >>> MarkAsFullyVerified -Processing command (at Snapshots5.v1.dfy(20,40)) assert (exists b#5: bool :: b#5 || !b#5) || 4 != 4; - >>> DoNothingToAssert -Processing command (at Snapshots5.v1.dfy(22,38)) assert (exists b#7: bool :: b#7 || !b#7) || 5 != 5; - >>> DoNothingToAssert - -Dafny program verifier finished with 3 verified, 0 errors - --------------------- Snapshots6.dfy -------------------- -Processing command (at Snapshots6.v0.dfy(20,14)) assert Lit(false); - >>> DoNothingToAssert - -Dafny program verifier finished with 4 verified, 0 errors -Processing command (at Snapshots6.v1.dfy(20,14)) assert Lit(false); - >>> DoNothingToAssert -Snapshots6.v1.dfy(20,14): Error: assertion violation -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 3 verified, 1 error - --------------------- Snapshots7.dfy -------------------- -Processing command (at Snapshots7.v0.dfy(19,14)) assert Lit(false); - >>> DoNothingToAssert - -Dafny program verifier finished with 4 verified, 0 errors -Processing implementation CheckWellformed$$_0_M0.C.Foo (at Snapshots7.v1.dfy(5,12)): - >>> added axiom: ##extracted_function##1() == (0 == $ModuleContextHeight && 0 == $FunctionContextHeight) - >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##1(); -Processing implementation Impl$$_0_M0.C.Foo (at Snapshots7.v1.dfy(5,12)): - >>> added axiom: ##extracted_function##2() == (0 == $ModuleContextHeight && 0 == $FunctionContextHeight && Lit(false)) - >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##2(); -Processing implementation CheckWellformed$$_1_M1.C.Foo (at Snapshots7.v1.dfy[M1](5,12)): - >>> added axiom: ##extracted_function##3() == (1 == $ModuleContextHeight && 0 == $FunctionContextHeight) - >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##3(); -Processing implementation Impl$$_1_M1.C.Foo (at Snapshots7.v1.dfy[M1](5,12)): - >>> added axiom: ##extracted_function##4() == (1 == $ModuleContextHeight && 0 == $FunctionContextHeight && Lit(false)) - >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##4(); -Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##1(); - >>> AssumeNegationOfAssumptionVariable -Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##2(); - >>> AssumeNegationOfAssumptionVariable -Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##3(); - >>> AssumeNegationOfAssumptionVariable -Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##4(); - >>> AssumeNegationOfAssumptionVariable -Processing command (at Snapshots7.v1.dfy(19,14)) assert Lit(false); - >>> MarkAsPartiallyVerified -Snapshots7.v1.dfy(19,14): Error: assertion violation -Execution trace: - (0,0): anon0 - -Dafny program verifier finished with 3 verified, 1 error diff --git a/Test/lit.site.cfg b/Test/lit.site.cfg index 1fe593f4..a960bdbc 100644 --- a/Test/lit.site.cfg +++ b/Test/lit.site.cfg @@ -22,7 +22,7 @@ config.suffixes = ['.dfy'] # excludes: A list of directories to exclude from the testsuite. The 'Inputs' # subdirectories contain auxiliary inputs for various tests in their parent # directories. -config.excludes = [] +config.excludes = ['Inputs'] # test_source_root: The root path where tests are located. config.test_source_root = os.path.dirname(os.path.abspath(__file__)) diff --git a/Test/runTests.py b/Test/runTests.py index b8d8e6f4..d2bb61c9 100644 --- a/Test/runTests.py +++ b/Test/runTests.py @@ -34,7 +34,7 @@ except ImportError: pass class Defaults: - ALWAYS_EXCLUDED = ["Output", "snapshots", "sandbox", "desktop"] + ALWAYS_EXCLUDED = ["Inputs", "Output", "sandbox", "desktop"] DAFNY_BIN = os.path.realpath(os.path.join(os.path.dirname(__file__), "../Binaries/Dafny.exe")) COMPILER = [DAFNY_BIN] FLAGS = ["/useBaseNameForFileName", "/compile:1", "/nologo", "/timeLimit:120"] @@ -108,7 +108,9 @@ class Test: self.timeout = timeout self.compiler_id = compiler_id self.cmds = [cmd.replace("%s", self.source_path) for cmd in self.cmds] + self.cmds = [cmd.replace("%S", self.source_directory) for cmd in self.cmds] self.cmds = [cmd.replace("%t", self.temp_output_path) for cmd in self.cmds] + self.cmds = [cmd.replace("%T", self.temp_directory) for cmd in self.cmds] self.status = TestStatus.PENDING self.proc_info = platform.processor() -- cgit v1.2.3 From 10876f2eb49891b6d58280b7d6d9121424e20727 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Mon, 20 Jul 2015 15:50:20 -0700 Subject: runTests.py: Improve reports (show oldest thread) and fix colors on cygwin The color fix is only partial. It's rather tricky to support all combinations of cygwin/cmd and posix/nt Python. At the moment things work well everywhere with native Python. --- Test/runTests.py | 106 ++++++++++++++++++++++++++++++++++++------------------- 1 file changed, 69 insertions(+), 37 deletions(-) (limited to 'Test/runTests.py') diff --git a/Test/runTests.py b/Test/runTests.py index d2bb61c9..f32b0e8d 100644 --- a/Test/runTests.py +++ b/Test/runTests.py @@ -8,8 +8,8 @@ import operator import platform from enum import Enum from time import time, strftime -from multiprocessing import Pool from collections import defaultdict +from multiprocessing import Pool, Manager from subprocess import Popen, call, PIPE, TimeoutExpired # C:/Python34/python.exe runTests.py --compiler "c:/MSR/dafny/Binaries/Dafny.exe /useBaseNameForFileName /compile:1 /nologo" --difftool "C:\Program Files (x86)\Meld\Meld.exe" -j4 -f "/dprelude preludes\AlmostAllTriggers.bpl" dafny0\SeqFromArray.dfy @@ -39,12 +39,21 @@ class Defaults: COMPILER = [DAFNY_BIN] FLAGS = ["/useBaseNameForFileName", "/compile:1", "/nologo", "/timeLimit:120"] +class Colors: + RED = '\033[91m' + GREEN = '\033[92m' + YELLOW = '\033[93m' + BRIGHT = '\033[1m' + DIM = '\033[2m' + RESET = '\033[0m' + class Debug(Enum): - ERROR = (-1, '\033[91m') - REPORT = (0, '\033[0m', True) - INFO = (1, '\033[0m', True) - DEBUG = (2, '\033[0m') - TRACE = (3, '\033[0m') + ERROR = (-1, Colors.RED) + WARNING = (-1, Colors.YELLOW) + REPORT = (0, Colors.RESET, True) + INFO = (1, Colors.RESET, True) + DEBUG = (2, Colors.RESET) + TRACE = (3, Colors.RESET) def __init__(self, index, color, elide=False): self.index = index @@ -55,7 +64,7 @@ def wrap_color(string, color, silent=False): if silent: return " " * len(string) elif ANSI: - return color + string + '\033[0m' + return color + string + Colors.RESET else: return string @@ -78,11 +87,11 @@ def debug(level, *args, **kwargs): print(*(headers + args), **kwargs) class TestStatus(Enum): - PENDING = (0, '\033[0m') - PASSED = (1, '\033[92m') - FAILED = (2, '\033[91m') - UNKNOWN = (3, '\033[91m') - TIMEOUT = (4, '\033[91m') + PENDING = (0, Colors.RESET) + PASSED = (1, Colors.GREEN) + FAILED = (2, Colors.RED) + UNKNOWN = (3, Colors.RED) + TIMEOUT = (4, Colors.RED) def __init__(self, index, color): self.index = index @@ -117,6 +126,7 @@ class Test: self.time, self.suite_time = None, None self.njobs, self.returncodes = None, [] + self.start, self.end, self.duration = None, None, None @staticmethod def source_to_expect_path(source): @@ -142,7 +152,7 @@ class Test: with open(name + ".csv", mode='w', newline='') as writer: csv_writer = csv.DictWriter(writer, Test.COLUMNS, dialect='excel') - csv_writer.writeheader() # TODO enable later + csv_writer.writeheader() for test in tests: test.serialize(csv_writer) @@ -220,8 +230,17 @@ class Test: self.output = Test.read_normalize(self.temp_output_path) self.status = TestStatus.PASSED if self.expected == self.output else TestStatus.FAILED - def report(self, tid, total): - debug(Debug.INFO, "[{:5.2f}s] {} ({} of {})".format(self.duration, self.dfy, tid, total), headers=self.status) + def report(self, tid, running, alltests): + running = [alltests[rid].fname for rid in running] + # running = ", ".join(running if len(running) <= 2 else (running[:2] + ["..."])) + if running: + running = "; oldest thread: {}".format(wrap_color(running[0], Colors.DIM)) + + fstring = "[{:5.2f}s] {} ({} of {}{})" + message = fstring.format(self.duration, wrap_color(self.dfy, Colors.BRIGHT), + tid, len(alltests), running) + + debug(Debug.INFO, message, headers=self.status) @staticmethod def write_bytes(base_directory, relative_path, extension, contents): @@ -290,27 +309,31 @@ def setup_parser(): return parser - -def run_one(test_args): +def run_one_internal(test, test_id, args, running): global KILLED global VERBOSITY - - test, args = test_args VERBOSITY = args.verbosity - try: - if not KILLED: + if not KILLED: + try: + running.append(test_id) test.run() - except KeyboardInterrupt: - # There's no reliable way to handle this cleanly on Windows: if one - # of the worker dies, it gets respawned. The reliable solution is to - # ignore further work once you receive a kill signal - KILLED = True - except Exception as e: - debug(Debug.ERROR, "[{}] {}".format(test.dfy, e)) - test.status = TestStatus.UNKNOWN + except KeyboardInterrupt: + # There's no reliable way to handle this cleanly on Windows: if one + # of the worker dies, it gets respawned. The reliable solution is to + # ignore further work once you receive a kill signal + KILLED = True + except Exception as e: + debug(Debug.ERROR, "[{}] {}".format(test.dfy, e)) + test.status = TestStatus.UNKNOWN + finally: + running.remove(test_id) + return test +def run_one(args): + return run_one_internal(*args) + def read_one_test(name, fname, compiler_cmds, timeout): for cid, compiler_cmd in enumerate(compiler_cmds): source_path = os.path.realpath(fname) @@ -378,13 +401,16 @@ def run_tests(args): try: pool = Pool(args.njobs) - start = time() results = [] - for tid, test in enumerate(pool.imap_unordered(run_one, [(t, args) for t in tests], 1)): - test.report(tid + 1, len(tests)) - results.append(test) - pool.close() - pool.join() + start = time() + with Manager() as manager: + running = manager.list() + payloads = [(t, tid, args, running) for (tid, t) in enumerate(tests)] + for tid, test in enumerate(pool.imap_unordered(run_one, payloads, 1)): + test.report(tid + 1, running, tests) + results.append(test) + pool.close() + pool.join() suite_time = time() - start for t in results: @@ -394,8 +420,11 @@ def run_tests(args): Test.summarize(results) Test.build_report(results, args.report) except KeyboardInterrupt: - pool.terminate() - pool.join() + try: + pool.terminate() + pool.join() + except (FileNotFoundError, EOFError, ConnectionAbortedError): + pass debug(Debug.ERROR, "Testing interrupted") @@ -455,6 +484,9 @@ def main(): args = parser.parse_args() VERBOSITY = args.verbosity + if os.name != 'nt' and os.environ.get("TERM") == "cygwin": + debug(Debug.WARNING, "If you run into issues, try using Windows' Python instead of Cygwin's") + if args.diff: diff(args.paths, args.accept, args.difftool) elif args.open: -- cgit v1.2.3 From 4fc4d641bb9f90538cd4bde0ad83012bc8622236 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Tue, 21 Jul 2015 13:14:16 -0700 Subject: Small fix in runTests.py --- Test/runTests.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'Test/runTests.py') diff --git a/Test/runTests.py b/Test/runTests.py index f32b0e8d..02a6f039 100644 --- a/Test/runTests.py +++ b/Test/runTests.py @@ -233,8 +233,7 @@ class Test: def report(self, tid, running, alltests): running = [alltests[rid].fname for rid in running] # running = ", ".join(running if len(running) <= 2 else (running[:2] + ["..."])) - if running: - running = "; oldest thread: {}".format(wrap_color(running[0], Colors.DIM)) + running = "; oldest thread: {}".format(wrap_color(running[0], Colors.DIM)) if running else "" fstring = "[{:5.2f}s] {} ({} of {}{})" message = fstring.format(self.duration, wrap_color(self.dfy, Colors.BRIGHT), -- cgit v1.2.3 From c2092abbb945b55c87976d6d57ec2f728306af89 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 23 Jul 2015 11:59:33 -0700 Subject: Let runTests.py generate expect files That is, missing expect files now raise a warning, not an error. --- Test/runTests.bat | 2 +- Test/runTests.py | 39 ++++++++++++++++++++++----------------- 2 files changed, 23 insertions(+), 18 deletions(-) (limited to 'Test/runTests.py') diff --git a/Test/runTests.bat b/Test/runTests.bat index ced3bd27..4856faf8 100644 --- a/Test/runTests.bat +++ b/Test/runTests.bat @@ -1,2 +1,2 @@ @REM runTests.bat -f "/dprelude PRELUDE_FILE" -r REPORT_NAME INPUT_FILES -C:/Python34/python.exe runTests.py --flags "/useBaseNameForFileName /compile:1 /nologo" --difftool "C:/Program Files (x86)/Meld/Meld.exe" %* +C:/Python34/python.exe runTests.py --difftool "C:/Program Files (x86)/Meld/Meld.exe" %* diff --git a/Test/runTests.py b/Test/runTests.py index 02a6f039..34a9c4de 100644 --- a/Test/runTests.py +++ b/Test/runTests.py @@ -138,8 +138,12 @@ class Test: @staticmethod def read_normalize(path): - with open(path, mode="rb") as reader: - return reader.read().replace(b'\r\n', b'\n').replace(b'\r', b'\n') + try: + with open(path, mode="rb") as reader: + return reader.read().replace(b'\r\n', b'\n').replace(b'\r', b'\n') + except FileNotFoundError: + debug(Debug.WARNING, "{} not found".format(path)) + return "" @staticmethod def build_report(tests, name): @@ -232,12 +236,12 @@ class Test: def report(self, tid, running, alltests): running = [alltests[rid].fname for rid in running] - # running = ", ".join(running if len(running) <= 2 else (running[:2] + ["..."])) - running = "; oldest thread: {}".format(wrap_color(running[0], Colors.DIM)) if running else "" + running = "; oldest thread: {}".format(running[0]) if running else "" - fstring = "[{:5.2f}s] {} ({} of {}{})" + fstring = "[{:5.2f}s] {} ({}{})" + progress = "{} of {}".format(tid, len(alltests)) message = fstring.format(self.duration, wrap_color(self.dfy, Colors.BRIGHT), - tid, len(alltests), running) + wrap_color(progress, Colors.BRIGHT), running) debug(Debug.INFO, message, headers=self.status) @@ -295,14 +299,14 @@ def setup_parser(): help="When comparing, include all timings.") parser.add_argument('--diff', '-d', action='store_const', const=True, default=False, - help="Don't run tests; show differences for one file.") + help="Don't run tests; show differences between outputs and .expect files, optionally overwritting .expect files.") + + parser.add_argument('--accept', '-a', action='store_const', const=True, default=False, + help="Don't run tests; copy outputs to .expect files.") parser.add_argument('--open', '-o', action='store_const', const=True, default=False, help="Don't run tests; open one file.") - parser.add_argument('--accept', '-a', action='store_const', const=True, default=False, - help="Used in conjuction with --diff, accept the new output.") - parser.add_argument('--difftool', action='store', type=str, default="diff", help='Diff program. Default: diff.') @@ -346,10 +350,7 @@ def read_one_test(name, fname, compiler_cmds, timeout): else: break if cmds: - if os.path.exists(Test.source_to_expect_path(source_path)): - yield Test(name, source_path, cmds, timeout, cid) - else: - debug(Debug.DEBUG, "Test file {} has no .expect".format(fname)) + yield Test(name, source_path, cmds, timeout, cid) else: debug(Debug.INFO, "Test file {} has no RUN specification".format(fname)) @@ -436,12 +437,16 @@ def diff(paths, accept, difftool): debug(Debug.ERROR, "Not found: {}".format(path)) else: test = Test(None, path, [], None) + if not accept: call([difftool, test.expect_path, test.temp_output_path]) + accept = input("Accept this change? (y/N) ") == "y" - if accept or input("Accept this change? (y/N) ") == "y": - debug(Debug.INFO, path, "Accepted") + if accept: + debug(Debug.INFO, path, "accepted.") shutil.copy(test.temp_output_path, test.expect_path) + else: + debug(Debug.INFO, path, "not accepted.") def compare_results(globs, time_all): from glob import glob @@ -486,7 +491,7 @@ def main(): if os.name != 'nt' and os.environ.get("TERM") == "cygwin": debug(Debug.WARNING, "If you run into issues, try using Windows' Python instead of Cygwin's") - if args.diff: + if args.diff or args.accept: diff(args.paths, args.accept, args.difftool) elif args.open: os.startfile(args.paths[0]) -- cgit v1.2.3 From 259a1283e5636fc99a454ea414dc71008f71a571 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 23 Jul 2015 15:03:21 -0700 Subject: Bump up the time limit in runTests.py and save a bit of space in output --- Test/runTests.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'Test/runTests.py') diff --git a/Test/runTests.py b/Test/runTests.py index 34a9c4de..62ab205b 100644 --- a/Test/runTests.py +++ b/Test/runTests.py @@ -12,7 +12,7 @@ from collections import defaultdict from multiprocessing import Pool, Manager from subprocess import Popen, call, PIPE, TimeoutExpired -# C:/Python34/python.exe runTests.py --compiler "c:/MSR/dafny/Binaries/Dafny.exe /useBaseNameForFileName /compile:1 /nologo" --difftool "C:\Program Files (x86)\Meld\Meld.exe" -j4 -f "/dprelude preludes\AlmostAllTriggers.bpl" dafny0\SeqFromArray.dfy +# C:/Python34/python.exe runTests.py --compiler "c:/MSR/dafny/Binaries/Dafny.exe" --flags "/useBaseNameForFileName /compile:1 /nologo" --difftool "C:\Program Files (x86)\Meld\Meld.exe" -j4 --flags "/dprelude preludes\AlmostAllTriggers.bpl" dafny0\SeqFromArray.dfy # c:/Python34/python.exe runTests.py --compare ../TestStable/results/SequenceAxioms/2015-06-06-00-54-52--PrettyPrinted.report.csv ../TestStable/results/SequenceAxioms/*.csv @@ -37,7 +37,7 @@ class Defaults: ALWAYS_EXCLUDED = ["Inputs", "Output", "sandbox", "desktop"] DAFNY_BIN = os.path.realpath(os.path.join(os.path.dirname(__file__), "../Binaries/Dafny.exe")) COMPILER = [DAFNY_BIN] - FLAGS = ["/useBaseNameForFileName", "/compile:1", "/nologo", "/timeLimit:120"] + FLAGS = ["/useBaseNameForFileName", "/compile:1", "/nologo", "/timeLimit:300"] class Colors: RED = '\033[91m' @@ -236,10 +236,10 @@ class Test: def report(self, tid, running, alltests): running = [alltests[rid].fname for rid in running] - running = "; oldest thread: {}".format(running[0]) if running else "" + running = "; oldest: {}".format(running[0]) if running else "" fstring = "[{:5.2f}s] {} ({}{})" - progress = "{} of {}".format(tid, len(alltests)) + progress = "{}/{}".format(tid, len(alltests)) message = fstring.format(self.duration, wrap_color(self.dfy, Colors.BRIGHT), wrap_color(progress, Colors.BRIGHT), running) -- cgit v1.2.3 From 1258fd132d80cfdba5e59cfd76c517a091269d2d Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Tue, 28 Jul 2015 17:56:40 -0700 Subject: Save failing tests to failing.lst, making it easy to re-run them --- Test/runTests.py | 36 +++++++++++++++++++++++++++--------- 1 file changed, 27 insertions(+), 9 deletions(-) (limited to 'Test/runTests.py') diff --git a/Test/runTests.py b/Test/runTests.py index 62ab205b..f9443426 100644 --- a/Test/runTests.py +++ b/Test/runTests.py @@ -184,6 +184,15 @@ class Test: for test in tests: debug(Debug.REPORT, "* " + test.dfy, headers=status, silentheaders=True) + debug(Debug.REPORT) + + failing = [t for t in results if t.status != TestStatus.PASSED] + if failing: + with open("failing.lst", mode='w') as writer: + for t in failing: + writer.write("{}\t{}\n".format(t.name, t.source_path)) + debug(Debug.REPORT, "Some tests failed: use [runTests.py failing.lst] to rerun the failing tests") + debug(Debug.REPORT, "Testing took {:.2f}s on {} thread(s)".format(results[0].suite_time, results[0].njobs)) @@ -265,8 +274,8 @@ class Test: def setup_parser(): parser = argparse.ArgumentParser(description='Run the Dafny test suite.') - parser.add_argument('paths', type=str, action='store', nargs='+', - help='Input files or folders. Folders are searched for .dfy files.') + parser.add_argument('path', type=str, action='store', nargs='+', + help='Input files or folders. Folders are searched for .dfy files. Lists of files can also be specified by passing a .lst file (for an example of such a file, look at failing.lst after running failing tests.') parser.add_argument('--compiler', type=str, action='append', default=None, help='Dafny executable. Default: {}'.format(Defaults.DAFNY_BIN)) @@ -286,6 +295,9 @@ def setup_parser(): parser.add_argument('--verbosity', action='store', type=int, default=1, help='Set verbosity level. 0: Minimal; 1: Some info; 2: More info.') + parser.add_argument('-v', action='store_const', default=1, dest="verbosity", const=2, + help='Short for --verbosity 2.') + parser.add_argument('--report', '-r', action='store', type=str, default=None, help='Give an explicit name to the report file. Defaults to the current date and time.') @@ -298,13 +310,13 @@ def setup_parser(): parser.add_argument('--time-all', action='store_true', help="When comparing, include all timings.") - parser.add_argument('--diff', '-d', action='store_const', const=True, default=False, + parser.add_argument('--diff', '-d', action='store_true', help="Don't run tests; show differences between outputs and .expect files, optionally overwritting .expect files.") - parser.add_argument('--accept', '-a', action='store_const', const=True, default=False, + parser.add_argument('--accept', '-a', action='store_true', help="Don't run tests; copy outputs to .expect files.") - parser.add_argument('--open', '-o', action='store_const', const=True, default=False, + parser.add_argument('--open', '-o', action='store_true', help="Don't run tests; open one file.") parser.add_argument('--difftool', action='store', type=str, default="diff", @@ -363,6 +375,12 @@ def find_one(name, fname, compiler_cmds, timeout): yield from read_one_test(name, fname, compiler_cmds, timeout) else: debug(Debug.ERROR, "Test file {} not found".format(fname)) + elif ext == ".lst": + debug(Debug.INFO, "Loading tests from {}".format(fname)) + with open(fname) as reader: + for line in reader: + _name, _path = line.strip().split() + yield from find_one(_name, _path, compiler_cmds, timeout) else: debug(Debug.TRACE, "Ignoring {}".format(fname)) @@ -390,7 +408,7 @@ def run_tests(args): debug(Debug.ERROR, "Compiler not found: {}".format(compiler)) return - tests = list(find_tests(args.paths, [compiler + ' ' + " ".join(args.base_flags + args.flags) + tests = list(find_tests(args.path, [compiler + ' ' + " ".join(args.base_flags + args.flags) for compiler in args.compiler], args.exclude + Defaults.ALWAYS_EXCLUDED, args.timeout)) tests.sort(key=operator.attrgetter("name")) @@ -492,11 +510,11 @@ def main(): debug(Debug.WARNING, "If you run into issues, try using Windows' Python instead of Cygwin's") if args.diff or args.accept: - diff(args.paths, args.accept, args.difftool) + diff(args.path, args.accept, args.difftool) elif args.open: - os.startfile(args.paths[0]) + os.startfile(args.path[0]) elif args.compare: - compare_results(args.paths, args.time_all) + compare_results(args.path, args.time_all) else: run_tests(args) -- cgit v1.2.3 From 65334f8f33c92a1e37376d6484d60ee45b55ca1d Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 31 Jul 2015 15:11:03 -0700 Subject: Add tests for the server --- Source/DafnyServer/Server.cs | 2 +- Test/lit.site.cfg | 8 + Test/runTests.py | 89 ++-- Test/server/simple-session.transcript | 637 +++++++++++++++++++++++++++ Test/server/simple-session.transcript.expect | 299 +++++++++++++ 5 files changed, 1000 insertions(+), 35 deletions(-) create mode 100644 Test/server/simple-session.transcript create mode 100644 Test/server/simple-session.transcript.expect (limited to 'Test/runTests.py') diff --git a/Source/DafnyServer/Server.cs b/Source/DafnyServer/Server.cs index c6f619d3..74cdd8c2 100644 --- a/Source/DafnyServer/Server.cs +++ b/Source/DafnyServer/Server.cs @@ -22,7 +22,7 @@ namespace Microsoft.Dafny { if (hasArg && args[0] == "selftest") { VerificationTask.SelfTest(); } else if (hasArg && File.Exists(arg)) { - Console.WriteLine("# Reading from {0}", arg); + Console.WriteLine("# Reading from {0}", Path.GetFileName(arg)); Console.SetIn(new StreamReader(arg)); server.Loop(); } else { diff --git a/Test/lit.site.cfg b/Test/lit.site.cfg index a960bdbc..c5718f86 100644 --- a/Test/lit.site.cfg +++ b/Test/lit.site.cfg @@ -79,14 +79,21 @@ lit_config.note('Repository root is {}'.format(repositoryRoot)) binaryDir = os.path.join( repositoryRoot, 'Binaries') dafnyExecutable = os.path.join( binaryDir, 'Dafny.exe') +serverExecutable = os.path.join( binaryDir, 'DafnyServer.exe') if not os.path.exists(dafnyExecutable): lit_config.fatal('Could not find Dafny.exe at {}'.format(dafnyExecutable)) +if not os.path.exists(serverExecutable): + lit_config.warning('Could not find DafnyServer.exe at {}'.format(serverExecutable)) +else: + config.suffixes.append('.transcript') + dafnyExecutable = quotePath(dafnyExecutable) if os.name == 'posix': dafnyExecutable = 'mono ' + dafnyExecutable + serverExecutable = 'mono ' + serverExecutable if lit.util.which('mono') == None: lit_config.fatal('Cannot find mono. Make sure it is your PATH') @@ -105,6 +112,7 @@ if len(dafnyParams) > 0: lit_config.note('Using Dafny: {}\n'.format(dafnyExecutable)) config.substitutions.append( ('%dafny', dafnyExecutable) ) +config.substitutions.append( ('%server', serverExecutable) ) # Sanity check: Check solver executable is available # FIXME: Should this check be removed entirely? diff --git a/Test/runTests.py b/Test/runTests.py index fc9c20e7..ebdb0655 100644 --- a/Test/runTests.py +++ b/Test/runTests.py @@ -38,6 +38,7 @@ class Defaults: DAFNY_BIN = os.path.realpath(os.path.join(os.path.dirname(__file__), "../Binaries/Dafny.exe")) COMPILER = [DAFNY_BIN] FLAGS = ["/useBaseNameForFileName", "/compile:1", "/nologo", "/timeLimit:300"] + EXTENSIONS = [".dfy", ".transcript"] class Colors: RED = '\033[91m' @@ -103,7 +104,6 @@ class Test: def __init__(self, name, source_path, cmds, timeout, compiler_id = 0): self.name = name - self.dfy = None if self.name is None else (self.name + ".dfy") self.source_path = Test.uncygdrive(source_path) self.expect_path = Test.source_to_expect_path(self.source_path) self.source_directory, self.fname = os.path.split(self.source_path) @@ -182,7 +182,7 @@ class Test: debug(Debug.REPORT, "{} of {}".format(len(tests), len(results)), headers=status) if status != TestStatus.PASSED: for test in tests: - debug(Debug.REPORT, "* " + test.dfy, headers=status, silentheaders=True) + debug(Debug.REPORT, "* " + test.name, headers=status, silentheaders=True) debug(Debug.REPORT) @@ -190,14 +190,14 @@ class Test: if failing: with open("failing.lst", mode='w') as writer: for t in failing: - writer.write("{}\t{}\n".format(t.name, t.source_path)) + writer.write("{}\n".format(t.name)) debug(Debug.REPORT, "Some tests failed: use [runTests.py failing.lst] to rerun the failing tests") debug(Debug.REPORT, "Testing took {:.2f}s on {} thread(s)".format(results[0].suite_time, results[0].njobs)) def run(self): - debug(Debug.DEBUG, "Starting {}".format(self.dfy)) + debug(Debug.DEBUG, "Starting {}".format(self.name)) os.makedirs(self.temp_directory, exist_ok=True) # os.chdir(self.source_directory) @@ -227,7 +227,7 @@ class Test: stdout, stderr = stdout.strip(), stderr.strip() if stdout != b"" or stderr != b"": - debug(Debug.TRACE, "Writing the output of {} to {}".format(self.dfy, self.temp_output_path)) + debug(Debug.TRACE, "Writing the output of {} to {}".format(self.name, self.temp_output_path)) with open(self.temp_output_path, mode='ab') as writer: writer.write(stdout + stderr) if stderr != b"": @@ -249,7 +249,7 @@ class Test: fstring = "[{:5.2f}s] {} ({}{})" progress = "{}/{}".format(tid, len(alltests)) - message = fstring.format(self.duration, wrap_color(self.dfy, Colors.BRIGHT), + message = fstring.format(self.duration, wrap_color(self.name, Colors.BRIGHT), wrap_color(progress, Colors.BRIGHT), running) debug(Debug.INFO, message, headers=self.status) @@ -275,7 +275,7 @@ def setup_parser(): parser = argparse.ArgumentParser(description='Run the Dafny test suite.') parser.add_argument('path', type=str, action='store', nargs='+', - help='Input files or folders. Folders are searched for .dfy files. Lists of files can also be specified by passing a .lst file (for an example of such a file, look at failing.lst after running failing tests.') + help='Input files or folders. Folders are searched for test files. Lists of files can also be specified by passing a .lst file (for an example of such a file, look at failing.lst after running failing tests.') parser.add_argument('--compiler', type=str, action='append', default=None, help='Dafny executable. Default: {}'.format(Defaults.DAFNY_BIN)) @@ -293,11 +293,14 @@ def setup_parser(): help='Excluded directories. {} are automatically added.'.format(Defaults.ALWAYS_EXCLUDED)) parser.add_argument('--verbosity', action='store', type=int, default=1, - help='Set verbosity level. 0: Minimal; 1: Some info; 2: More info.') + help='Set verbosity level. 0: Minimal; 1: Some info; 2: More info; 3: Trace.') parser.add_argument('-v', action='store_const', default=1, dest="verbosity", const=2, help='Short for --verbosity 2.') + parser.add_argument('-vv', action='store_const', default=1, dest="verbosity", const=3, + help='Short for --verbosity 3.') + parser.add_argument('--report', '-r', action='store', type=str, default=None, help='Give an explicit name to the report file. Defaults to the current date and time.') @@ -339,7 +342,7 @@ def run_one_internal(test, test_id, args, running): # ignore further work once you receive a kill signal KILLED = True except Exception as e: - debug(Debug.ERROR, "[{}] {}".format(test.dfy, e)) + debug(Debug.ERROR, "[{}] {}".format(test.name, e)) test.status = TestStatus.UNKNOWN finally: running.remove(test_id) @@ -349,53 +352,71 @@ def run_one_internal(test, test_id, args, running): def run_one(args): return run_one_internal(*args) -def read_one_test(name, fname, compiler_cmds, timeout): +def get_server_path(compiler): + REGEXP = r"\bDafny.exe\b.*" + if re.search(REGEXP, compiler): + return re.sub(REGEXP, "DafnyServer.exe", compiler) + else: + return None + +def substitute_binaries(cmd, compiler): + cmd = cmd.replace("%dafny", compiler) + cmd = cmd.replace("%server", get_server_path(compiler)) + return cmd + +def read_one_test(fname, compiler_cmds, timeout): for cid, compiler_cmd in enumerate(compiler_cmds): source_path = os.path.realpath(fname) with open(source_path, mode='r') as reader: cmds = [] for line in reader: line = line.strip() - match = re.match("^// *RUN: *(?!%diff)([^ ].*)$", line) + match = re.match("^[/# ]*RUN: *(?!%diff)([^ ].*)$", line) if match: - cmds.append(match.groups()[0].replace("%dafny", compiler_cmd)) + debug(Debug.TRACE, "Found RUN spec: {}".format(line)) + cmds.append(substitute_binaries(match.groups()[0], compiler_cmd)) else: break if cmds: - yield Test(name, source_path, cmds, timeout, cid) + yield Test(fname, source_path, cmds, timeout, cid) else: - debug(Debug.INFO, "Test file {} has no RUN specification".format(fname)) + debug(Debug.WARNING, "Test file {} has no RUN specification".format(fname)) -def find_one(name, fname, compiler_cmds, timeout, allow_lst=False): - name, ext = os.path.splitext(fname) - if ext == ".dfy": +def find_one(fname, compiler_cmds, timeout): + _, ext = os.path.splitext(fname) + if ext in Defaults.EXTENSIONS: if os.path.exists(fname): debug(Debug.TRACE, "Found test file: {}".format(fname)) - yield from read_one_test(name, fname, compiler_cmds, timeout) + yield from read_one_test(fname, compiler_cmds, timeout) else: debug(Debug.ERROR, "Test file {} not found".format(fname)) - elif ext == ".lst" and allow_lst: #lst files are only read if explicitly listed on the CLI - debug(Debug.INFO, "Loading tests from {}".format(fname)) - with open(fname) as reader: - for line in reader: - _name, _path = line.strip().split() - yield from find_one(_name, _path, compiler_cmds, timeout) else: debug(Debug.TRACE, "Ignoring {}".format(fname)) -def find_tests(paths, compiler_cmds, excluded, timeout): +def expand_lsts(paths): for path in paths: + _, ext = os.path.splitext(path) + if ext == ".lst": #lst files are only read if explicitly listed on the CLI + debug(Debug.INFO, "Loading tests from {}".format(path)) + with open(path) as reader: + for line in reader: + _path = line.strip() + yield _path + else: + yield path + +def find_tests(paths, compiler_cmds, excluded, timeout): + for path in expand_lsts(paths): if os.path.isdir(path): debug(Debug.TRACE, "Searching for tests in {}".format(path)) for base, dirnames, fnames in os.walk(path): dirnames[:] = [d for d in dirnames if d not in excluded] for fname in fnames: - yield from find_one(fname, os.path.join(base, fname), compiler_cmds, timeout) + yield from find_one(os.path.join(base, fname), compiler_cmds, timeout) else: - yield from find_one(path, path, compiler_cmds, timeout, True) - + yield from find_one(path, compiler_cmds, timeout) def run_tests(args): if args.compiler is None: @@ -404,12 +425,15 @@ def run_tests(args): args.base_flags = Defaults.FLAGS for compiler in args.compiler: + server = get_server_path(compiler) if not os.path.exists(compiler): debug(Debug.ERROR, "Compiler not found: {}".format(compiler)) return + if not os.path.exists(server): + debug(Debug.WARNING, "Server not found") tests = list(find_tests(args.path, [compiler + ' ' + " ".join(args.base_flags + args.flags) - for compiler in args.compiler], + for compiler in args.compiler], args.exclude + Defaults.ALWAYS_EXCLUDED, args.timeout)) tests.sort(key=operator.attrgetter("name")) @@ -447,10 +471,7 @@ def run_tests(args): def diff(paths, accept, difftool): - for path in paths: - if not path.endswith(".dfy"): - path += ".dfy" - + for path in expand_lsts(paths): if not os.path.exists(path): debug(Debug.ERROR, "Not found: {}".format(path)) else: @@ -470,7 +491,7 @@ def compare_results(globs, time_all): from glob import glob paths = [path for g in globs for path in glob(g)] reports = {path: Test.load_report(path) for path in paths} - resultsets = {path: {test.dfy: (test.status, test.duration) for test in report} + resultsets = {path: {test.name: (test.status, test.duration) for test in report} for path, report in reports.items()} all_tests = set(name for resultset in resultsets.values() for name in resultset.keys()) diff --git a/Test/server/simple-session.transcript b/Test/server/simple-session.transcript new file mode 100644 index 00000000..26539267 --- /dev/null +++ b/Test/server/simple-session.transcript @@ -0,0 +1,637 @@ +# RUN: %server "%s" > "%t" +# RUN: %diff "%s.expect" "%t" +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xuICBhc3NlcnQgZmFsc2U7XG59XG4iLCJz +b3VyY2VJc0ZpbGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xuICBhc3NlcnQgZmFsc2U7XG4gfVxuIiwi +c291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xuICBhc3NlcnQgZmFsc2U7XG59XG4iLCJz +b3VyY2VJc0ZpbGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xuICBhc3NlcnQgZmFsc2U7XG59XG4iLCJz +b3VyY2VJc0ZpbGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG4iLCJzb3VyY2VJc0ZpbGUiOmZh +bHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7Iiwic291 +cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gICIs +InNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG59Iiwi +c291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG5cbn0i +LCJzb3VyY2VJc0ZpbGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIFxu +fSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIHhc +bn0iLCJzb3VyY2VJc0ZpbGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIFxu +fSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIHZh +clxufSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIHZh +ciB4IDo9IDE7XG59Iiwic291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIHZh +ciB4IDo9IDE7XG4gIFxufSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIHZh +ciB4IDo9IDE7XG4gIHZhciB5LCB6IDo9IDI7XG59Iiwic291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIHZh +ciB4IDo9IDE7XG4gIHZhciB5LCB6IDo9IDI7XG4gIFxufSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5tZXRob2QgTScoKSB7XG4gIHZh +ciB4IDo9IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIFxufSIsInNvdXJjZUlzRmlsZSI6ZmFs +c2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKCkg +e1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAyLCAzO1xuICBcbn0iLCJzb3VyY2VJc0Zp +bGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKCkg +e1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAyLCAzO1xuICBcbn0iLCJzb3VyY2VJc0Zp +bGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcblxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAyLCAzO1xuICBcbn0iLCJz +b3VyY2VJc0ZpbGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcblxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAyLCAzO1xuICBcbn0iLCJz +b3VyY2VJc0ZpbGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgXG57XG4gIHZhciB4IDo9IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIFxufSIs +InNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxXG57XG4gIHZhciB4IDo9IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIFxu +fSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxXG57XG4gIHZhciB4IDo9IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIFxu +fSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgXG59Iiwic291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzXG59Iiwic291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvclxufSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JyA6OiBcbn0iLCJzb3VyY2VJc0ZpbGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JyA6OiBpbnQsIHgnICogeCcgPiAwO1xufSIsInNvdXJj +ZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JyA6OiBpbnQsIHgnICogeCcgPiAwO1xufSIsInNvdXJj +ZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4J2ludCwgeCcgKiB4JyA+IDA7XG59Iiwic291cmNlSXNG +aWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50LCB4JyAqIHgnID4gMDtcbn0iLCJzb3VyY2VJ +c0ZpbGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6ICwgeCcgKiB4JyA+IDA7XG59Iiwic291 +cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPiAwO1xufSIsInNvdXJj +ZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbn0iLCJzb3Vy +Y2VJc0ZpbGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgXG59Iiwi +c291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzXG59 +Iiwic291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn0iLCJzb3VyY2VJc0ZpbGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuIiwic291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn0iLCJz +b3VyY2VJc0ZpbGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn0iLCJz +b3VyY2VJc0ZpbGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cbiIs +InNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNJyh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59Iiwic291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNJyh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59Iiwic291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNJyh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG4iLCJzb3VyY2VJc0ZpbGUiOmZhbHNl +fQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNJyh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTScodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiB4JyA+PSAwO1xuICBhc3NlcnQg +eCAqIHggPiAwO1xufSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0odDogbmF0KVxuICByZXF1aXJlcyB0 +ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAyLCAzO1xuICBhc3NlcnQgZm9y +YWxsIHgnOiBpbnQgOjogeCcgKiB4JyA+PSAwO1xuICBhc3NlcnQgeCAqIHggPiAwO1xufVxuXG5z +dGF0aWMgbWV0aG9kIE0odDogbmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAx +O1xuICB2YXIgeSwgeiA6PSAyLCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiB4 +JyA+PSAwO1xuICBhc3NlcnQgeCAqIHggPiAwO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0odDogbmF0 +KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAyLCAz +O1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiB4JyA+PSAwO1xuICBhc3NlcnQgeCAq +IHggPiAwO1xufSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiB4JyA+PSAwO1xuICBhc3NlcnQg +eCAqIHggPiAwO1xufSIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiB4JyA+PSAwO1xuICBhc3NlcnQg +eCAqIHggPiAwO1xufVxuIiwic291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnID49IDA7XG4gIGFzc2Vy +dCB4ICogeCA+IDA7XG59XG4iLCJzb3VyY2VJc0ZpbGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnICAwO1xuICBhc3NlcnQg +eCAqIHggPiAwO1xufVxuIiwic291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDwgMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cbiIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc2Vy +dCB4ICogeCA+IDA7XG59XG4iLCJzb3VyY2VJc0ZpbGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIFxuICBh +c3NlcnQgeCAqIHggPiAwO1xufVxuIiwic291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc1xu +ICBhc3NlcnQgeCAqIHggPiAwO1xufVxuIiwic291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc2Vy +XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG4iLCJzb3VyY2VJc0ZpbGUiOmZhbHNlfQ== +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc1xu +ICBhc3NlcnQgeCAqIHggPiAwO1xufVxuIiwic291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc3Vt +ZSB5IDwgMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cbiIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc3Vt +ZSB5IDwgMDtcbiAgYXNzZXJ0IDtcbn1cbiIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc3Vt +ZSB5IDwgMDtcbiAgYXNzZXJ0IDtcbn1cbiIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc3Vt +ZSB5IDwgMDtcbiAgYXNzZXJ0IGZhbDtcbn1cbiIsInNvdXJjZUlzRmlsZSI6ZmFsc2V9 +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc3Vt +ZSB5IDwgMDtcbiAgYXNzZXJ0IGZhbHNlO1xufVxuIiwic291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] +verify +eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp +bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50 +KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xufVxuXG5zdGF0aWMgbWV0aG9kIE0nKHQ6 +IG5hdClcbiAgcmVxdWlyZXMgdCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0g +MiwgMztcbiAgYXNzZXJ0IGZvcmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0 +IHggKiB4ID4gMDtcbn1cblxuXG5zdGF0aWMgbWV0aG9kIE0wKHQ6IG5hdClcbiAgcmVxdWlyZXMg +dCA+IDBcbntcbiAgdmFyIHggOj0gMTtcbiAgdmFyIHksIHogOj0gMiwgMztcbiAgYXNzZXJ0IGZv +cmFsbCB4JzogaW50IDo6IHgnICogeCcgPj0gMDtcbiAgYXNzZXJ0IHggKiB4ID4gMDtcbn1cblxu +c3RhdGljIG1ldGhvZCBNMSh0OiBuYXQpXG4gIHJlcXVpcmVzIHQgPiAwXG57XG4gIHZhciB4IDo9 +IDE7XG4gIHZhciB5LCB6IDo9IDIsIDM7XG4gIGFzc2VydCBmb3JhbGwgeCc6IGludCA6OiB4JyAq +IHgnID49IDA7XG4gIGFzc2VydCB4ICogeCA+IDA7XG59XG5cbnN0YXRpYyBtZXRob2QgTTIodDog +bmF0KVxuICByZXF1aXJlcyB0ID4gMFxue1xuICB2YXIgeCA6PSAxO1xuICB2YXIgeSwgeiA6PSAy +LCAzO1xuICBhc3NlcnQgZm9yYWxsIHgnOiBpbnQgOjogeCcgKiAtIHgnIDw9IDA7XG4gIGFzc3Vt +ZSB5IDwgMDtcbiAgYXNzZXJ0IGZhbHNlO1xufVxuIiwic291cmNlSXNGaWxlIjpmYWxzZX0= +[[DAFNY-CLIENT: EOM]] diff --git a/Test/server/simple-session.transcript.expect b/Test/server/simple-session.transcript.expect new file mode 100644 index 00000000..89c3351d --- /dev/null +++ b/Test/server/simple-session.transcript.expect @@ -0,0 +1,299 @@ +# Reading from simple-session.transcript +transcript(3,9): Error: assertion violation +Execution trace: + (0,0): anon0 +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(3,9): Error: assertion violation +Execution trace: + (0,0): anon0 +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(3,9): Error: assertion violation +Execution trace: + (0,0): anon0 +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(3,9): Error: assertion violation +Execution trace: + (0,0): anon0 +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,13): Error: rbrace expected +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(6,2): Error: rbrace expected +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(7,0): Error: invalid UpdateStmt +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(7,0): Error: ident expected +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(7,11): Error: the number of left-hand sides (2) and right-hand sides (1) must match for a multi-assignment +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(7,11): Error: the number of left-hand sides (2) and right-hand sides (1) must match for a multi-assignment +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(6,2): Error: EOF expected +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(6,2): Error: EOF expected +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(11,0): Error: invalid UpdateStmt +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(11,0): Error: semi expected +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(11,0): Error: invalid UnaryExpression +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,25): Error: openparen expected +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,25): Error: openparen expected +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,26): Error: invalid QSep +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,28): Error: invalid QSep +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,27): Error: invalid UnaryExpression +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(10,9): Error: assertion violation +Execution trace: + (0,0): anon0 +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(12,0): Error: invalid UpdateStmt +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,14): Error: Duplicate member name: M' +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,14): Error: Duplicate member name: M' +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,14): Error: Duplicate member name: M' +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,14): Error: Duplicate member name: M' +transcript(24,14): Error: Duplicate member name: M' +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,14): Error: Duplicate member name: M' +transcript(24,14): Error: Duplicate member name: M' +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,14): Error: Duplicate member name: M' +transcript(24,14): Error: Duplicate member name: M' +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,14): Error: Duplicate member name: M' +transcript(24,14): Error: Duplicate member name: M' +transcript(33,14): Error: Duplicate member name: M' +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,14): Error: Duplicate member name: M +transcript(33,14): Error: Duplicate member name: M +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(38,9): Error: assertion violation +Execution trace: + (0,0): anon0 +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(38,38): Error: semi expected +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(38,9): Error: assertion violation +Execution trace: + (0,0): anon0 +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(40,2): Error: invalid UpdateStmt +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(40,2): Error: invalid UpdateStmt +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(40,2): Error: invalid UpdateStmt +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(40,9): Error: invalid AssertStmt +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(40,9): Error: invalid AssertStmt +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(40,9): Error: unresolved identifier: fal +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] +Verification completed successfully! +[SUCCESS] [[DAFNY-SERVER: EOM]] -- cgit v1.2.3 From 9e1b3ef9e63eb9c823d275927b7a62cdfab576b2 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Wed, 12 Aug 2015 11:41:59 -0700 Subject: runTests.py: Pretty-print stderr output to TRACE upon test failure --- Test/runTests.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Test/runTests.py') diff --git a/Test/runTests.py b/Test/runTests.py index ebdb0655..0232f81b 100644 --- a/Test/runTests.py +++ b/Test/runTests.py @@ -231,7 +231,7 @@ class Test: with open(self.temp_output_path, mode='ab') as writer: writer.write(stdout + stderr) if stderr != b"": - debug(Debug.TRACE, stderr) + debug(Debug.TRACE, stderr.decode("utf-8")) self.update_status() except TimeoutExpired: -- cgit v1.2.3 From 6a24e8c90ac467678dbf9aeb0d16c3d36c2dcf44 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Tue, 18 Aug 2015 18:14:36 -0700 Subject: runTests: Report mean completion time of passed tests, excluding outliers --- Test/runTests.py | 23 ++++++++++++++++++++++- 1 file changed, 22 insertions(+), 1 deletion(-) (limited to 'Test/runTests.py') diff --git a/Test/runTests.py b/Test/runTests.py index 0232f81b..9f4fa5a5 100644 --- a/Test/runTests.py +++ b/Test/runTests.py @@ -6,6 +6,7 @@ import shutil import argparse import operator import platform +from math import floor, ceil from enum import Enum from time import time, strftime from collections import defaultdict @@ -168,6 +169,25 @@ class Test: results.append(Test.deserialize(row)) return results + @staticmethod + def mean_duration(results, margin): + durations = sorted(result.duration for result in results + if result.status == TestStatus.PASSED) + if len(durations) >= 15: + lq = durations[floor(0.25 * len(durations))] + hq = durations[ceil(0.85 * len(durations))] + iqr = hq - lq + filtered = [d for d in durations if (lq - margin * iqr) <= d <= (hq + margin * iqr)] + if filtered: + avg = sum(durations) / len(durations) + trimmed_avg = sum(filtered) / len(filtered) + outliers_count = len(durations) - len(filtered) + msg = "mean completion time: {:.2f}s".format(avg) + if outliers_count > 0: + msg += "; ignoring {} outliers: {:.2f}s".format(outliers_count, trimmed_avg) + return " ({})".format(msg) + return "" + @staticmethod def summarize(results): debug(Debug.INFO, "\nTesting complete ({} test(s))".format(len(results))) @@ -193,7 +213,8 @@ class Test: writer.write("{}\n".format(t.name)) debug(Debug.REPORT, "Some tests failed: use [runTests.py failing.lst] to rerun the failing tests") - debug(Debug.REPORT, "Testing took {:.2f}s on {} thread(s)".format(results[0].suite_time, results[0].njobs)) + debug(Debug.REPORT, "Testing took {:.2f}s on {} thread(s){}".format( + results[0].suite_time, results[0].njobs, Test.mean_duration(results, 1.5))) def run(self): -- cgit v1.2.3 From fcf9093f269b924555780e60fe05e4eff9de1cf4 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Wed, 19 Aug 2015 10:11:08 -0700 Subject: runTests: Include failed tests in mean completion time --- Test/runTests.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'Test/runTests.py') diff --git a/Test/runTests.py b/Test/runTests.py index 9f4fa5a5..eae29012 100644 --- a/Test/runTests.py +++ b/Test/runTests.py @@ -148,12 +148,12 @@ class Test: @staticmethod def build_report(tests, name): - time = strftime("%Y-%m-%d-%H-%M-%S") + now = strftime("%Y-%m-%d-%H-%M-%S") if name: directory, fname = os.path.split(name) - name = os.path.join(directory, time + "--" + fname) + name = os.path.join(directory, now + "--" + fname) else: - name = time + name = now with open(name + ".csv", mode='w', newline='') as writer: csv_writer = csv.DictWriter(writer, Test.COLUMNS, dialect='excel') @@ -172,7 +172,7 @@ class Test: @staticmethod def mean_duration(results, margin): durations = sorted(result.duration for result in results - if result.status == TestStatus.PASSED) + if result.status in (TestStatus.PASSED, TestStatus.FAILED)) if len(durations) >= 15: lq = durations[floor(0.25 * len(durations))] hq = durations[ceil(0.85 * len(durations))] -- cgit v1.2.3 From e5f9a4cbf74f7794ad13b2a5bd831fd54c20629c Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Wed, 19 Aug 2015 16:15:47 -0700 Subject: runTests: Accept tests one by one, even if they are given as a .lst file --- Test/runTests.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'Test/runTests.py') diff --git a/Test/runTests.py b/Test/runTests.py index eae29012..7cd90454 100644 --- a/Test/runTests.py +++ b/Test/runTests.py @@ -491,12 +491,13 @@ def run_tests(args): debug(Debug.ERROR, "Testing interrupted") -def diff(paths, accept, difftool): +def diff(paths, force_accept, difftool): for path in expand_lsts(paths): if not os.path.exists(path): debug(Debug.ERROR, "Not found: {}".format(path)) else: test = Test(None, path, [], None) + accept = force_accept if not accept: call([difftool, test.expect_path, test.temp_output_path]) -- cgit v1.2.3 From aa73a99a6fef9ada930d3b5b35e328006d8b30ee Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 21 Aug 2015 09:41:39 -0700 Subject: Ignore flycheck_* files in runTests --- Test/runTests.py | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) (limited to 'Test/runTests.py') diff --git a/Test/runTests.py b/Test/runTests.py index 7cd90454..53733eb1 100644 --- a/Test/runTests.py +++ b/Test/runTests.py @@ -35,7 +35,8 @@ except ImportError: pass class Defaults: - ALWAYS_EXCLUDED = ["Inputs", "Output", "sandbox", "desktop"] + EXCLUDED_FILES = ["^flycheck_"] + EXCLUDED_FOLDERS = ["Inputs", "Output", "sandbox", "desktop"] DAFNY_BIN = os.path.realpath(os.path.join(os.path.dirname(__file__), "../Binaries/Dafny.exe")) COMPILER = [DAFNY_BIN] FLAGS = ["/useBaseNameForFileName", "/compile:1", "/nologo", "/timeLimit:300"] @@ -311,7 +312,7 @@ def setup_parser(): help='Number of test workers.') parser.add_argument('--exclude', action='append', type=str, default=[], - help='Excluded directories. {} are automatically added.'.format(Defaults.ALWAYS_EXCLUDED)) + help='Excluded directories. {} are automatically added.'.format(Defaults.EXCLUDED_FOLDERS)) parser.add_argument('--verbosity', action='store', type=int, default=1, help='Set verbosity level. 0: Minimal; 1: Some info; 2: More info; 3: Trace.') @@ -405,8 +406,9 @@ def read_one_test(fname, compiler_cmds, timeout): def find_one(fname, compiler_cmds, timeout): - _, ext = os.path.splitext(fname) - if ext in Defaults.EXTENSIONS: + _, name = os.path.split(fname) + _, ext = os.path.splitext(name) + if ext in Defaults.EXTENSIONS and not any(re.search(pattern, name, re.IGNORECASE) for pattern in Defaults.EXCLUDED_FILES): if os.path.exists(fname): debug(Debug.TRACE, "Found test file: {}".format(fname)) yield from read_one_test(fname, compiler_cmds, timeout) @@ -455,7 +457,7 @@ def run_tests(args): tests = list(find_tests(args.path, [compiler + ' ' + " ".join(args.base_flags + args.flags) for compiler in args.compiler], - args.exclude + Defaults.ALWAYS_EXCLUDED, args.timeout)) + args.exclude + Defaults.EXCLUDED_FOLDERS, args.timeout)) tests.sort(key=operator.attrgetter("name")) args.njobs = max(1, min(args.njobs or os.cpu_count() or 1, len(tests))) -- cgit v1.2.3 From 0434fa61124d979d254fa4d38fdc1db06a578d18 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 21 Aug 2015 09:58:38 -0700 Subject: Interleave stderr output with test results; this allows one to print stuff directly to stderr in Dafny without breaking tests --- Test/runTests.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'Test/runTests.py') diff --git a/Test/runTests.py b/Test/runTests.py index 53733eb1..8caa65d1 100644 --- a/Test/runTests.py +++ b/Test/runTests.py @@ -248,12 +248,12 @@ class Test: self.duration = self.end - self.start stdout, stderr = stdout.strip(), stderr.strip() - if stdout != b"" or stderr != b"": + if stdout != b"": debug(Debug.TRACE, "Writing the output of {} to {}".format(self.name, self.temp_output_path)) with open(self.temp_output_path, mode='ab') as writer: - writer.write(stdout + stderr) + writer.write(stdout) if stderr != b"": - debug(Debug.TRACE, stderr.decode("utf-8")) + debug(Debug.INFO, stderr.decode("utf-8")) self.update_status() except TimeoutExpired: -- cgit v1.2.3