From 87a9ba9e82dfa727000edaaa8134e1feb083a704 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 26 Sep 2024 07:01:03 -0700 Subject: [PATCH] Adding tests for --message_format json --- examples/Makefile.common | 8 + tests/error-messages/.gitignore | 3 + .../AQualMismatch.fst.json_expected | 7 + .../error-messages/AnotType.fst.json_expected | 8 + .../ArgsAndQuals.fst.json_expected | 7 + .../ArrowRanges.fst.json_expected | 8 + .../AssertNorm.fst.json_expected | 5 + .../error-messages/Asserts.fst.json_expected | 11 + .../BadEmptyRecord.fst.json_expected | 5 + tests/error-messages/Basic.fst.json_expected | 38 +++ .../error-messages/Bug1918.fst.json_expected | 5 + .../error-messages/Bug1988.fst.json_expected | 11 + .../error-messages/Bug1997.fst.json_expected | 295 ++++++++++++++++++ .../error-messages/Bug2010.fst.json_expected | 5 + .../error-messages/Bug2021.fst.json_expected | 20 ++ .../error-messages/Bug2245.fst.json_expected | 5 + .../error-messages/Bug2820.fst.json_expected | 21 ++ .../error-messages/Bug2899.fst.json_expected | 14 + .../error-messages/Bug2953.fst.json_expected | 5 + .../error-messages/Bug2980.fst.json_expected | 5 + .../error-messages/Bug2981.fst.json_expected | 5 + .../error-messages/Bug3099.fst.json_expected | 7 + .../error-messages/Bug3102.fst.json_expected | 20 ++ .../error-messages/Bug3145.fst.json_expected | 29 ++ .../error-messages/Bug3227.fst.json_expected | 76 +++++ .../error-messages/Bug3292.fst.json_expected | 83 +++++ tests/error-messages/Calc.fst.json_expected | 35 +++ .../error-messages/CalcImpl.fst.json_expected | 161 ++++++++++ .../Coercions.fst.json_expected | 23 ++ .../error-messages/DTuples.fst.json_expected | 143 +++++++++ .../DecreasesTypeWarning.fst.json_expected | 4 + .../DumpUvarsOf.fst.json_expected | 15 + .../error-messages/Erasable.fst.json_expected | 23 ++ .../ExpectFailure.fst.json_expected | 23 ++ .../GhostImplicits.fst.json_expected | 5 + tests/error-messages/IfCond.fst.json_expected | 5 + tests/error-messages/IfThen.fst.json_expected | 5 + .../Inference.fst.json_expected | 6 + tests/error-messages/Makefile | 55 +++- .../NegativeTests.BST.fst.json_expected | 11 + .../NegativeTests.Bug260.fst.json_expected | 7 + .../NegativeTests.False.fst.json_expected | 12 + .../NegativeTests.Heap.fst.json_expected | 5 + .../NegativeTests.Neg.fst.json_expected | 41 +++ ...NegativeTests.Positivity.fst.json_expected | 20 ++ .../NegativeTests.Set.fst.json_expected | 15 + ...iveTests.ShortCircuiting.fst.json_expected | 11 + ...egativeTests.Termination.fst.json_expected | 43 +++ ...iveTests.ZZImplicitFalse.fst.json_expected | 7 + .../OccursCheckOnArrows.fst.json_expected | 5 + .../OptionStack.fst.json_expected | 14 + .../error-messages/PatAnnot.fst.json_expected | 20 ++ .../PatCoerce.fst.json_expected | 7 + .../PatternMatch.fst.json_expected | 44 +++ .../QuickTest.fst.json_expected | 5 + .../QuickTestNBE.fst.json_expected | 5 + .../RecordFields.fst.json_expected | 11 + ...ResolveImplicitsErrorPos.fst.json_expected | 10 + .../SMTPatSymbols.fst.json_expected | 3 + tests/error-messages/SeqLit.fst.json_expected | 78 +++++ .../StableErr.fst.json_expected | 5 + .../StrictUnfolding.fst.json_expected | 25 ++ .../StringNormalization.fst.json_expected | 5 + ...FunctionalExtensionality.fst.json_expected | 14 + .../TestErrorLocations.fst.json_expected | 51 +++ .../TestHasEq.fst.json_expected | 11 + .../UnboundOp.fst.json_expected | 5 + tests/error-messages/Unit2.fst.json_expected | 5 + .../UnresolvedFields.fst.json_expected | 11 + .../WPExtensionality.fst.json_expected | 5 + 70 files changed, 1703 insertions(+), 17 deletions(-) create mode 100644 tests/error-messages/AQualMismatch.fst.json_expected create mode 100644 tests/error-messages/AnotType.fst.json_expected create mode 100644 tests/error-messages/ArgsAndQuals.fst.json_expected create mode 100644 tests/error-messages/ArrowRanges.fst.json_expected create mode 100644 tests/error-messages/AssertNorm.fst.json_expected create mode 100644 tests/error-messages/Asserts.fst.json_expected create mode 100644 tests/error-messages/BadEmptyRecord.fst.json_expected create mode 100644 tests/error-messages/Basic.fst.json_expected create mode 100644 tests/error-messages/Bug1918.fst.json_expected create mode 100644 tests/error-messages/Bug1988.fst.json_expected create mode 100644 tests/error-messages/Bug1997.fst.json_expected create mode 100644 tests/error-messages/Bug2010.fst.json_expected create mode 100644 tests/error-messages/Bug2021.fst.json_expected create mode 100644 tests/error-messages/Bug2245.fst.json_expected create mode 100644 tests/error-messages/Bug2820.fst.json_expected create mode 100644 tests/error-messages/Bug2899.fst.json_expected create mode 100644 tests/error-messages/Bug2953.fst.json_expected create mode 100644 tests/error-messages/Bug2980.fst.json_expected create mode 100644 tests/error-messages/Bug2981.fst.json_expected create mode 100644 tests/error-messages/Bug3099.fst.json_expected create mode 100644 tests/error-messages/Bug3102.fst.json_expected create mode 100644 tests/error-messages/Bug3145.fst.json_expected create mode 100644 tests/error-messages/Bug3227.fst.json_expected create mode 100644 tests/error-messages/Bug3292.fst.json_expected create mode 100644 tests/error-messages/Calc.fst.json_expected create mode 100644 tests/error-messages/CalcImpl.fst.json_expected create mode 100644 tests/error-messages/Coercions.fst.json_expected create mode 100644 tests/error-messages/DTuples.fst.json_expected create mode 100644 tests/error-messages/DecreasesTypeWarning.fst.json_expected create mode 100644 tests/error-messages/DumpUvarsOf.fst.json_expected create mode 100644 tests/error-messages/Erasable.fst.json_expected create mode 100644 tests/error-messages/ExpectFailure.fst.json_expected create mode 100644 tests/error-messages/GhostImplicits.fst.json_expected create mode 100644 tests/error-messages/IfCond.fst.json_expected create mode 100644 tests/error-messages/IfThen.fst.json_expected create mode 100644 tests/error-messages/Inference.fst.json_expected create mode 100644 tests/error-messages/NegativeTests.BST.fst.json_expected create mode 100644 tests/error-messages/NegativeTests.Bug260.fst.json_expected create mode 100644 tests/error-messages/NegativeTests.False.fst.json_expected create mode 100644 tests/error-messages/NegativeTests.Heap.fst.json_expected create mode 100644 tests/error-messages/NegativeTests.Neg.fst.json_expected create mode 100644 tests/error-messages/NegativeTests.Positivity.fst.json_expected create mode 100644 tests/error-messages/NegativeTests.Set.fst.json_expected create mode 100644 tests/error-messages/NegativeTests.ShortCircuiting.fst.json_expected create mode 100644 tests/error-messages/NegativeTests.Termination.fst.json_expected create mode 100644 tests/error-messages/NegativeTests.ZZImplicitFalse.fst.json_expected create mode 100644 tests/error-messages/OccursCheckOnArrows.fst.json_expected create mode 100644 tests/error-messages/OptionStack.fst.json_expected create mode 100644 tests/error-messages/PatAnnot.fst.json_expected create mode 100644 tests/error-messages/PatCoerce.fst.json_expected create mode 100644 tests/error-messages/PatternMatch.fst.json_expected create mode 100644 tests/error-messages/QuickTest.fst.json_expected create mode 100644 tests/error-messages/QuickTestNBE.fst.json_expected create mode 100644 tests/error-messages/RecordFields.fst.json_expected create mode 100644 tests/error-messages/ResolveImplicitsErrorPos.fst.json_expected create mode 100644 tests/error-messages/SMTPatSymbols.fst.json_expected create mode 100644 tests/error-messages/SeqLit.fst.json_expected create mode 100644 tests/error-messages/StableErr.fst.json_expected create mode 100644 tests/error-messages/StrictUnfolding.fst.json_expected create mode 100644 tests/error-messages/StringNormalization.fst.json_expected create mode 100644 tests/error-messages/Test.FunctionalExtensionality.fst.json_expected create mode 100644 tests/error-messages/TestErrorLocations.fst.json_expected create mode 100644 tests/error-messages/TestHasEq.fst.json_expected create mode 100644 tests/error-messages/UnboundOp.fst.json_expected create mode 100644 tests/error-messages/Unit2.fst.json_expected create mode 100644 tests/error-messages/UnresolvedFields.fst.json_expected create mode 100644 tests/error-messages/WPExtensionality.fst.json_expected diff --git a/examples/Makefile.common b/examples/Makefile.common index 505092b1445..53814a59a23 100644 --- a/examples/Makefile.common +++ b/examples/Makefile.common @@ -102,6 +102,14 @@ include .depend $(call msg, "OUTPUT", $(basename $(notdir $@))) $(Q)$(VERBOSE_FSTAR) -f --print_expected_failures $< >$@ 2>&1 +%.fst.json_output: %.fst + $(call msg, "JSONOUT", $(basename $(notdir $@))) + $(Q)$(VERBOSE_FSTAR) --message_format json -f --print_expected_failures $< >$@ 2>&1 + +%.fsti.json_output: %.fsti + $(call msg, "JSONOUT", $(basename $(notdir $@))) + $(Q)$(VERBOSE_FSTAR) --message_format json -f --print_expected_failures $< >$@ 2>&1 + clean: rm -rf $(CACHE_DIR) diff --git a/tests/error-messages/.gitignore b/tests/error-messages/.gitignore index 15878c51119..99e3e101bb3 100644 --- a/tests/error-messages/.gitignore +++ b/tests/error-messages/.gitignore @@ -1,2 +1,5 @@ *.output +*.json_output *.check +*.human_check +*.json_check diff --git a/tests/error-messages/AQualMismatch.fst.json_expected b/tests/error-messages/AQualMismatch.fst.json_expected new file mode 100644 index 00000000000..0c709512895 --- /dev/null +++ b/tests/error-messages/AQualMismatch.fst.json_expected @@ -0,0 +1,7 @@ +>> Got issues: [ +{"msg":["Inconsistent implicit argument annotation on argument x","Got: '#'","Expected: ''"],"level":"Error","range":{"def":{"file_name":"AQualMismatch.fst","start_pos":{"line":6,"col":7},"end_pos":{"line":6,"col":8}},"use":{"file_name":"AQualMismatch.fst","start_pos":{"line":6,"col":7},"end_pos":{"line":6,"col":8}}},"number":91,"ctx":["While typechecking the top-level declaration `let f`","While typechecking the top-level declaration `[@@expect_failure] let f`"]} +>>] +{"msg":["AQualMismatch.f\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"AQualMismatch.fst","start_pos":{"line":3,"col":4},"end_pos":{"line":3,"col":5}},"use":{"file_name":"AQualMismatch.fst","start_pos":{"line":3,"col":4},"end_pos":{"line":3,"col":5}}},"number":240,"ctx":["While desugaring module AQualMismatch"]} +{"msg":["Missing definitions in module AQualMismatch: f"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"AQualMismatch.fst","start_pos":{"line":6,"col":0},"end_pos":{"line":6,"col":12}}},"number":240,"ctx":[]} +Verified module: AQualMismatch +All verification conditions discharged successfully diff --git a/tests/error-messages/AnotType.fst.json_expected b/tests/error-messages/AnotType.fst.json_expected new file mode 100644 index 00000000000..b3bff7f6336 --- /dev/null +++ b/tests/error-messages/AnotType.fst.json_expected @@ -0,0 +1,8 @@ +>> Got issues: [ +{"msg":["Type annotation Prims.int for inductive AnotType.tc is not Type or eqtype, or it\nis eqtype but contains noeq/unopteq qualifiers"],"level":"Error","range":{"def":{"file_name":"AnotType.fst","start_pos":{"line":19,"col":5},"end_pos":{"line":19,"col":7}},"use":{"file_name":"AnotType.fst","start_pos":{"line":19,"col":5},"end_pos":{"line":19,"col":7}}},"number":309,"ctx":["While typechecking the top-level declaration `type AnotType.tc`","While typechecking the top-level declaration `[@@expect_failure] type AnotType.tc`"]} +>>] +>> Got issues: [ +{"msg":["Expected expression of type Type0\ngot expression tb\nof type Type"],"level":"Error","range":{"def":{"file_name":"AnotType.fst","start_pos":{"line":27,"col":14},"end_pos":{"line":27,"col":16}},"use":{"file_name":"AnotType.fst","start_pos":{"line":27,"col":14},"end_pos":{"line":27,"col":16}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]} +>>] +Verified module: AnotType +All verification conditions discharged successfully diff --git a/tests/error-messages/ArgsAndQuals.fst.json_expected b/tests/error-messages/ArgsAndQuals.fst.json_expected new file mode 100644 index 00000000000..f1545bc8d52 --- /dev/null +++ b/tests/error-messages/ArgsAndQuals.fst.json_expected @@ -0,0 +1,7 @@ +>> Got issues: [ +{"msg":["Inconsistent implicit argument annotation on argument uu___","Got: '#'","Expected: '$'"],"level":"Error","range":{"def":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":25,"col":16},"end_pos":{"line":25,"col":18}},"use":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":25,"col":16},"end_pos":{"line":25,"col":18}}},"number":91,"ctx":["While typechecking the top-level declaration `let test1`","While typechecking the top-level declaration `[@@expect_failure] let test1`"]} +>>] +{"msg":["ArgsAndQuals.test1\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":23,"col":4},"end_pos":{"line":23,"col":9}},"use":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":23,"col":4},"end_pos":{"line":23,"col":9}}},"number":240,"ctx":["While desugaring module ArgsAndQuals"]} +{"msg":["Missing definitions in module ArgsAndQuals: test1"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":25,"col":0},"end_pos":{"line":25,"col":29}}},"number":240,"ctx":[]} +Verified module: ArgsAndQuals +All verification conditions discharged successfully diff --git a/tests/error-messages/ArrowRanges.fst.json_expected b/tests/error-messages/ArrowRanges.fst.json_expected new file mode 100644 index 00000000000..d019cc1a11d --- /dev/null +++ b/tests/error-messages/ArrowRanges.fst.json_expected @@ -0,0 +1,8 @@ +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type Prims.eqtype\ngot type Type0","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":73,"col":23},"end_pos":{"line":73,"col":30}},"use":{"file_name":"ArrowRanges.fst","start_pos":{"line":4,"col":30},"end_pos":{"line":4,"col":39}}},"number":19,"ctx":["While typechecking the top-level declaration `let ppof`","While typechecking the top-level declaration `[@@expect_failure] let ppof`"]} +>>] +>> Got issues: [ +{"msg":["Failed to prove that the type\n'ArrowRanges.ppof'\nsupports decidable equality because of this argument.","Add either the 'noeq' or 'unopteq' qualifier","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"ArrowRanges.fst","start_pos":{"line":7,"col":0},"end_pos":{"line":11,"col":1}},"use":{"file_name":"ArrowRanges.fst","start_pos":{"line":8,"col":10},"end_pos":{"line":8,"col":28}}},"number":19,"ctx":["While typechecking the top-level declaration `type ArrowRanges.ppof`","While typechecking the top-level declaration `[@@expect_failure] type ArrowRanges.ppof`"]} +>>] +Verified module: ArrowRanges +All verification conditions discharged successfully diff --git a/tests/error-messages/AssertNorm.fst.json_expected b/tests/error-messages/AssertNorm.fst.json_expected new file mode 100644 index 00000000000..9f6b602a8a1 --- /dev/null +++ b/tests/error-messages/AssertNorm.fst.json_expected @@ -0,0 +1,5 @@ +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"AssertNorm.fst","start_pos":{"line":7,"col":14},"end_pos":{"line":7,"col":30}},"use":{"file_name":"AssertNorm.fst","start_pos":{"line":7,"col":2},"end_pos":{"line":7,"col":13}}},"number":19,"ctx":["While typechecking the top-level declaration `let f`","While typechecking the top-level declaration `[@@expect_failure] let f`"]} +>>] +Verified module: AssertNorm +All verification conditions discharged successfully diff --git a/tests/error-messages/Asserts.fst.json_expected b/tests/error-messages/Asserts.fst.json_expected new file mode 100644 index 00000000000..b51bae7c3fa --- /dev/null +++ b/tests/error-messages/Asserts.fst.json_expected @@ -0,0 +1,11 @@ +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Asserts.fst","start_pos":{"line":6,"col":9},"end_pos":{"line":6,"col":17}},"use":{"file_name":"Asserts.fst","start_pos":{"line":6,"col":9},"end_pos":{"line":6,"col":17}}},"number":19,"ctx":["While typechecking the top-level declaration `let test`","While typechecking the top-level declaration `[@@expect_failure] let test`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Asserts.fst","start_pos":{"line":11,"col":9},"end_pos":{"line":11,"col":17}},"use":{"file_name":"Asserts.fst","start_pos":{"line":11,"col":2},"end_pos":{"line":11,"col":8}}},"number":19,"ctx":["While typechecking the top-level declaration `let test2`","While typechecking the top-level declaration `[@@expect_failure] let test2`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Asserts.fst","start_pos":{"line":16,"col":9},"end_pos":{"line":16,"col":14}},"use":{"file_name":"Asserts.fst","start_pos":{"line":16,"col":2},"end_pos":{"line":16,"col":8}}},"number":19,"ctx":["While typechecking the top-level declaration `let test3`","While typechecking the top-level declaration `[@@expect_failure] let test3`"]} +>>] +Verified module: Asserts +All verification conditions discharged successfully diff --git a/tests/error-messages/BadEmptyRecord.fst.json_expected b/tests/error-messages/BadEmptyRecord.fst.json_expected new file mode 100644 index 00000000000..2d14bacf5d7 --- /dev/null +++ b/tests/error-messages/BadEmptyRecord.fst.json_expected @@ -0,0 +1,5 @@ +>> Got issues: [ +{"msg":["Could not resolve the type for this record."],"level":"Error","range":{"def":{"file_name":"BadEmptyRecord.fst","start_pos":{"line":9,"col":6},"end_pos":{"line":9,"col":8}},"use":{"file_name":"BadEmptyRecord.fst","start_pos":{"line":9,"col":6},"end_pos":{"line":9,"col":8}}},"number":360,"ctx":["While typechecking the top-level declaration `let test`","While typechecking the top-level declaration `[@@expect_failure] let test`"]} +>>] +Verified module: BadEmptyRecord +All verification conditions discharged successfully diff --git a/tests/error-messages/Basic.fst.json_expected b/tests/error-messages/Basic.fst.json_expected new file mode 100644 index 00000000000..7a5d46ffd34 --- /dev/null +++ b/tests/error-messages/Basic.fst.json_expected @@ -0,0 +1,38 @@ +>> Got issues: [ +{"msg":["Expected expression of type Prims.int\ngot expression true\nof type Prims.bool"],"level":"Error","range":{"def":{"file_name":"Basic.fst","start_pos":{"line":4,"col":13},"end_pos":{"line":4,"col":17}},"use":{"file_name":"Basic.fst","start_pos":{"line":4,"col":13},"end_pos":{"line":4,"col":17}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Basic.fst","start_pos":{"line":6,"col":45},"end_pos":{"line":6,"col":50}},"use":{"file_name":"Basic.fst","start_pos":{"line":6,"col":38},"end_pos":{"line":6,"col":44}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___1`","While typechecking the top-level declaration `[@@expect_failure] let uu___1`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Basic.fst","start_pos":{"line":7,"col":45},"end_pos":{"line":7,"col":50}},"use":{"file_name":"Basic.fst","start_pos":{"line":7,"col":38},"end_pos":{"line":7,"col":44}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___2`","While typechecking the top-level declaration `[@@expect_failure] let uu___2`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Basic.fst","start_pos":{"line":8,"col":45},"end_pos":{"line":8,"col":50}},"use":{"file_name":"Basic.fst","start_pos":{"line":8,"col":38},"end_pos":{"line":8,"col":44}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___4`","While typechecking the top-level declaration `[@@expect_failure] let uu___4`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Basic.fst","start_pos":{"line":9,"col":45},"end_pos":{"line":9,"col":50}},"use":{"file_name":"Basic.fst","start_pos":{"line":9,"col":38},"end_pos":{"line":9,"col":44}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___6`","While typechecking the top-level declaration `[@@expect_failure] let uu___6`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Basic.fst","start_pos":{"line":11,"col":50},"end_pos":{"line":11,"col":55}},"use":{"file_name":"Basic.fst","start_pos":{"line":11,"col":38},"end_pos":{"line":11,"col":49}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___9`","While typechecking the top-level declaration `[@@expect_failure] let uu___9`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Basic.fst","start_pos":{"line":12,"col":50},"end_pos":{"line":12,"col":55}},"use":{"file_name":"Basic.fst","start_pos":{"line":12,"col":38},"end_pos":{"line":12,"col":49}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___10`","While typechecking the top-level declaration `[@@expect_failure] let uu___10`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Basic.fst","start_pos":{"line":13,"col":50},"end_pos":{"line":13,"col":55}},"use":{"file_name":"Basic.fst","start_pos":{"line":13,"col":38},"end_pos":{"line":13,"col":49}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___12`","While typechecking the top-level declaration `[@@expect_failure] let uu___12`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Basic.fst","start_pos":{"line":14,"col":50},"end_pos":{"line":14,"col":55}},"use":{"file_name":"Basic.fst","start_pos":{"line":14,"col":38},"end_pos":{"line":14,"col":49}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___14`","While typechecking the top-level declaration `[@@expect_failure] let uu___14`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":451,"col":90},"end_pos":{"line":451,"col":102}},"use":{"file_name":"Basic.fst","start_pos":{"line":17,"col":29},"end_pos":{"line":17,"col":31}}},"number":19,"ctx":["While typechecking the top-level declaration `let test2`","While typechecking the top-level declaration `[@@expect_failure] let test2`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":451,"col":90},"end_pos":{"line":451,"col":102}},"use":{"file_name":"Basic.fst","start_pos":{"line":20,"col":29},"end_pos":{"line":20,"col":31}}},"number":19,"ctx":["While typechecking the top-level declaration `let test3`","While typechecking the top-level declaration `[@@expect_failure] let test3`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":451,"col":90},"end_pos":{"line":451,"col":102}},"use":{"file_name":"Basic.fst","start_pos":{"line":23,"col":46},"end_pos":{"line":23,"col":48}}},"number":19,"ctx":["While typechecking the top-level declaration `let test6`","While typechecking the top-level declaration `[@@expect_failure] let test6`"]} +>>] +Verified module: Basic +All verification conditions discharged successfully diff --git a/tests/error-messages/Bug1918.fst.json_expected b/tests/error-messages/Bug1918.fst.json_expected new file mode 100644 index 00000000000..5c42dd627ac --- /dev/null +++ b/tests/error-messages/Bug1918.fst.json_expected @@ -0,0 +1,5 @@ +>> Got issues: [ +{"msg":["Could not solve typeclass constraint `Bug1918.mon`"],"level":"Error","range":{"def":{"file_name":"FStar.Tactics.Typeclasses.fst","start_pos":{"line":297,"col":6},"end_pos":{"line":300,"col":7}},"use":{"file_name":"Bug1918.fst","start_pos":{"line":11,"col":13},"end_pos":{"line":11,"col":14}}},"number":228,"ctx":["While synthesizing term with a tactic","Running tactic for meta-arg","While typechecking the top-level declaration `let comp2`","While typechecking the top-level declaration `[@@expect_failure] let comp2`"]} +>>] +Verified module: Bug1918 +All verification conditions discharged successfully diff --git a/tests/error-messages/Bug1988.fst.json_expected b/tests/error-messages/Bug1988.fst.json_expected new file mode 100644 index 00000000000..3c8aa50053d --- /dev/null +++ b/tests/error-messages/Bug1988.fst.json_expected @@ -0,0 +1,11 @@ +>> Got issues: [ +{"msg":["Expected expression of type Prims.int\ngot expression \"string literal\"\nof type Prims.string"],"level":"Error","range":{"def":{"file_name":"Bug1988.fst","start_pos":{"line":4,"col":14},"end_pos":{"line":4,"col":30}},"use":{"file_name":"Bug1988.fst","start_pos":{"line":4,"col":14},"end_pos":{"line":4,"col":30}}},"number":189,"ctx":["While typechecking the top-level declaration `let x`","While typechecking the top-level declaration `[@@expect_failure] let x`"]} +>>] +>> Got issues: [ +{"msg":["Prims.string is not equal to the expected type _: ident -> Prims.string"],"level":"Error","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"Bug1988.fst","start_pos":{"line":15,"col":32},"end_pos":{"line":15,"col":38}}},"number":54,"ctx":["While solving deferred constraints","solve_non_tactic_deferred_constraints","While typechecking the top-level declaration `let f1`","While typechecking the top-level declaration `[@@expect_failure] let f1`"]} +>>] +>> Got issues: [ +{"msg":["Prims.string is not a subtype of the expected type _: (*?u21*) _ -> (*?u22*) _"],"level":"Error","range":{"def":{"file_name":"Bug1988.fst","start_pos":{"line":21,"col":32},"end_pos":{"line":21,"col":38}},"use":{"file_name":"Bug1988.fst","start_pos":{"line":21,"col":32},"end_pos":{"line":21,"col":38}}},"number":54,"ctx":["While solving deferred constraints","solve_non_tactic_deferred_constraints","While typechecking the top-level declaration `let f2`","While typechecking the top-level declaration `[@@expect_failure] let f2`"]} +>>] +Verified module: Bug1988 +All verification conditions discharged successfully diff --git a/tests/error-messages/Bug1997.fst.json_expected b/tests/error-messages/Bug1997.fst.json_expected new file mode 100644 index 00000000000..786b8ea9a7e --- /dev/null +++ b/tests/error-messages/Bug1997.fst.json_expected @@ -0,0 +1,295 @@ +Module after desugaring: +module Bug1997 +Declarations: [ +let op_Equals_Hat a b = a + b +let test1 a b c = a =^ b =^ c +let test2 a b c = a =^ b =^ c +let test3 a b c = a =^ (b =^ c) +private +let _ = FStar.Pervasives.assert_norm (Bug1997.test1 == Bug1997.test2) + +let imp_assoc_0 p q r = p ==> q ==> r +let imp_assoc_1 p q r = p ==> q ==> r +let imp_assoc_2 p q r = (p ==> q) ==> r +private +let _ = FStar.Pervasives.assert_norm (Bug1997.imp_assoc_0 == Bug1997.imp_assoc_1) + +let imp_iff_0 p q r = p ==> q <==> r +let imp_iff_1 p q r = p ==> q <==> r +let imp_iff_2 p q r = p ==> (q <==> r) +private +let _ = FStar.Pervasives.assert_norm (Bug1997.imp_iff_0 == Bug1997.imp_iff_1) + +let imp_conj_1 p q r s = p ==> q /\ r ==> s +let imp_conj_2 p q r s = (p ==> q) /\ (r ==> s) +let imp_conj_3 p q r s = p ==> q /\ (r ==> s) +let imp_conj_4 p q r s = p ==> q /\ r ==> s +private +let _ = FStar.Pervasives.assert_norm (Bug1997.imp_conj_1 == Bug1997.imp_conj_4) + + + + + +let impneg1 p q r = p ==> q /\ ~p ==> r +let impneg2 p q r = (p ==> q) /\ (~p ==> r) +let impneg3 p q r = p ==> q /\ (~p ==> r) +let impneg4 p q r = p ==> q /\ ~p ==> r +private +let _ = FStar.Pervasives.assert_norm (Bug1997.impneg1 == Bug1997.impneg4) + + + + + +let cd1 p q r = p /\ q \/ r +let cd2 p q r = p /\ q \/ r +let cd3 p q r = p /\ (q \/ r) +private +let _ = FStar.Pervasives.assert_norm (Bug1997.cd1 == Bug1997.cd2) + + +let m0 p q r s = p /\ (q \/ r) /\ s +let m1 p q r s = p /\ q \/ r /\ s +let m2 p q r s = p /\ q \/ r /\ s +let m3 p q r s = p /\ q \/ r /\ s +let m4 p q r s = p /\ q \/ r /\ s +private +let _ = FStar.Pervasives.assert_norm (Bug1997.m1 == Bug1997.m2) +private +let _ = FStar.Pervasives.assert_norm (Bug1997.m1 == Bug1997.m3) +private +let _ = FStar.Pervasives.assert_norm (Bug1997.m1 == Bug1997.m4) + + + + +let n0 p q r s = p \/ q /\ r \/ s +let n1 p q r s = p \/ q /\ r \/ s +let n2 p q r s = (p \/ q) /\ r \/ s +let n3 p q r s = (p \/ q) /\ (r \/ s) +let n4 p q r s = p \/ q /\ (r \/ s) +private +let _ = FStar.Pervasives.assert_norm (Bug1997.n0 == Bug1997.n1) + + + + + + +] + +Module before type checking: +module Bug1997 +Declarations: [ +let op_Equals_Hat a b = a + b +let test1 a b c = a =^ b =^ c +let test2 a b c = a =^ b =^ c +let test3 a b c = a =^ (b =^ c) +private +let _ = FStar.Pervasives.assert_norm (Bug1997.test1 == Bug1997.test2) + +let imp_assoc_0 p q r = p ==> q ==> r +let imp_assoc_1 p q r = p ==> q ==> r +let imp_assoc_2 p q r = (p ==> q) ==> r +private +let _ = FStar.Pervasives.assert_norm (Bug1997.imp_assoc_0 == Bug1997.imp_assoc_1) + +let imp_iff_0 p q r = p ==> q <==> r +let imp_iff_1 p q r = p ==> q <==> r +let imp_iff_2 p q r = p ==> (q <==> r) +private +let _ = FStar.Pervasives.assert_norm (Bug1997.imp_iff_0 == Bug1997.imp_iff_1) + +let imp_conj_1 p q r s = p ==> q /\ r ==> s +let imp_conj_2 p q r s = (p ==> q) /\ (r ==> s) +let imp_conj_3 p q r s = p ==> q /\ (r ==> s) +let imp_conj_4 p q r s = p ==> q /\ r ==> s +private +let _ = FStar.Pervasives.assert_norm (Bug1997.imp_conj_1 == Bug1997.imp_conj_4) + + + + + +let impneg1 p q r = p ==> q /\ ~p ==> r +let impneg2 p q r = (p ==> q) /\ (~p ==> r) +let impneg3 p q r = p ==> q /\ (~p ==> r) +let impneg4 p q r = p ==> q /\ ~p ==> r +private +let _ = FStar.Pervasives.assert_norm (Bug1997.impneg1 == Bug1997.impneg4) + + + + + +let cd1 p q r = p /\ q \/ r +let cd2 p q r = p /\ q \/ r +let cd3 p q r = p /\ (q \/ r) +private +let _ = FStar.Pervasives.assert_norm (Bug1997.cd1 == Bug1997.cd2) + + +let m0 p q r s = p /\ (q \/ r) /\ s +let m1 p q r s = p /\ q \/ r /\ s +let m2 p q r s = p /\ q \/ r /\ s +let m3 p q r s = p /\ q \/ r /\ s +let m4 p q r s = p /\ q \/ r /\ s +private +let _ = FStar.Pervasives.assert_norm (Bug1997.m1 == Bug1997.m2) +private +let _ = FStar.Pervasives.assert_norm (Bug1997.m1 == Bug1997.m3) +private +let _ = FStar.Pervasives.assert_norm (Bug1997.m1 == Bug1997.m4) + + + + +let n0 p q r s = p \/ q /\ r \/ s +let n1 p q r s = p \/ q /\ r \/ s +let n2 p q r s = (p \/ q) /\ r \/ s +let n3 p q r s = (p \/ q) /\ (r \/ s) +let n4 p q r s = p \/ q /\ (r \/ s) +private +let _ = FStar.Pervasives.assert_norm (Bug1997.n0 == Bug1997.n1) + + + + + + +] + +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Bug1997.fst","start_pos":{"line":13,"col":39},"end_pos":{"line":13,"col":55}},"use":{"file_name":"Bug1997.fst","start_pos":{"line":13,"col":27},"end_pos":{"line":13,"col":38}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___12`","While typechecking the top-level declaration `[@@expect_failure] let uu___12`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Bug1997.fst","start_pos":{"line":21,"col":39},"end_pos":{"line":21,"col":67}},"use":{"file_name":"Bug1997.fst","start_pos":{"line":21,"col":27},"end_pos":{"line":21,"col":38}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___23`","While typechecking the top-level declaration `[@@expect_failure] let uu___23`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Bug1997.fst","start_pos":{"line":29,"col":39},"end_pos":{"line":29,"col":63}},"use":{"file_name":"Bug1997.fst","start_pos":{"line":29,"col":27},"end_pos":{"line":29,"col":38}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___34`","While typechecking the top-level declaration `[@@expect_failure] let uu___34`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Bug1997.fst","start_pos":{"line":38,"col":39},"end_pos":{"line":38,"col":65}},"use":{"file_name":"Bug1997.fst","start_pos":{"line":38,"col":27},"end_pos":{"line":38,"col":38}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___52`","While typechecking the top-level declaration `[@@expect_failure] let uu___52`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Bug1997.fst","start_pos":{"line":39,"col":39},"end_pos":{"line":39,"col":65}},"use":{"file_name":"Bug1997.fst","start_pos":{"line":39,"col":27},"end_pos":{"line":39,"col":38}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___53`","While typechecking the top-level declaration `[@@expect_failure] let uu___53`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Bug1997.fst","start_pos":{"line":40,"col":39},"end_pos":{"line":40,"col":65}},"use":{"file_name":"Bug1997.fst","start_pos":{"line":40,"col":27},"end_pos":{"line":40,"col":38}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___54`","While typechecking the top-level declaration `[@@expect_failure] let uu___54`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Bug1997.fst","start_pos":{"line":41,"col":39},"end_pos":{"line":41,"col":65}},"use":{"file_name":"Bug1997.fst","start_pos":{"line":41,"col":27},"end_pos":{"line":41,"col":38}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___55`","While typechecking the top-level declaration `[@@expect_failure] let uu___55`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Bug1997.fst","start_pos":{"line":42,"col":39},"end_pos":{"line":42,"col":65}},"use":{"file_name":"Bug1997.fst","start_pos":{"line":42,"col":27},"end_pos":{"line":42,"col":38}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___56`","While typechecking the top-level declaration `[@@expect_failure] let uu___56`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Bug1997.fst","start_pos":{"line":51,"col":39},"end_pos":{"line":51,"col":59}},"use":{"file_name":"Bug1997.fst","start_pos":{"line":51,"col":27},"end_pos":{"line":51,"col":38}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___70`","While typechecking the top-level declaration `[@@expect_failure] let uu___70`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Bug1997.fst","start_pos":{"line":52,"col":39},"end_pos":{"line":52,"col":59}},"use":{"file_name":"Bug1997.fst","start_pos":{"line":52,"col":27},"end_pos":{"line":52,"col":38}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___71`","While typechecking the top-level declaration `[@@expect_failure] let uu___71`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Bug1997.fst","start_pos":{"line":53,"col":39},"end_pos":{"line":53,"col":59}},"use":{"file_name":"Bug1997.fst","start_pos":{"line":53,"col":27},"end_pos":{"line":53,"col":38}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___72`","While typechecking the top-level declaration `[@@expect_failure] let uu___72`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Bug1997.fst","start_pos":{"line":54,"col":39},"end_pos":{"line":54,"col":59}},"use":{"file_name":"Bug1997.fst","start_pos":{"line":54,"col":27},"end_pos":{"line":54,"col":38}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___73`","While typechecking the top-level declaration `[@@expect_failure] let uu___73`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Bug1997.fst","start_pos":{"line":55,"col":39},"end_pos":{"line":55,"col":59}},"use":{"file_name":"Bug1997.fst","start_pos":{"line":55,"col":27},"end_pos":{"line":55,"col":38}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___74`","While typechecking the top-level declaration `[@@expect_failure] let uu___74`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Bug1997.fst","start_pos":{"line":63,"col":39},"end_pos":{"line":63,"col":51}},"use":{"file_name":"Bug1997.fst","start_pos":{"line":63,"col":27},"end_pos":{"line":63,"col":38}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___85`","While typechecking the top-level declaration `[@@expect_failure] let uu___85`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Bug1997.fst","start_pos":{"line":64,"col":39},"end_pos":{"line":64,"col":51}},"use":{"file_name":"Bug1997.fst","start_pos":{"line":64,"col":27},"end_pos":{"line":64,"col":38}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___86`","While typechecking the top-level declaration `[@@expect_failure] let uu___86`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Bug1997.fst","start_pos":{"line":75,"col":39},"end_pos":{"line":75,"col":49}},"use":{"file_name":"Bug1997.fst","start_pos":{"line":75,"col":27},"end_pos":{"line":75,"col":38}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___110`","While typechecking the top-level declaration `[@@expect_failure] let uu___110`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Bug1997.fst","start_pos":{"line":76,"col":39},"end_pos":{"line":76,"col":49}},"use":{"file_name":"Bug1997.fst","start_pos":{"line":76,"col":27},"end_pos":{"line":76,"col":38}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___111`","While typechecking the top-level declaration `[@@expect_failure] let uu___111`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Bug1997.fst","start_pos":{"line":77,"col":39},"end_pos":{"line":77,"col":49}},"use":{"file_name":"Bug1997.fst","start_pos":{"line":77,"col":27},"end_pos":{"line":77,"col":38}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___112`","While typechecking the top-level declaration `[@@expect_failure] let uu___112`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Bug1997.fst","start_pos":{"line":78,"col":39},"end_pos":{"line":78,"col":49}},"use":{"file_name":"Bug1997.fst","start_pos":{"line":78,"col":27},"end_pos":{"line":78,"col":38}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___113`","While typechecking the top-level declaration `[@@expect_failure] let uu___113`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Bug1997.fst","start_pos":{"line":87,"col":39},"end_pos":{"line":87,"col":49}},"use":{"file_name":"Bug1997.fst","start_pos":{"line":87,"col":27},"end_pos":{"line":87,"col":38}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___135`","While typechecking the top-level declaration `[@@expect_failure] let uu___135`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Bug1997.fst","start_pos":{"line":88,"col":39},"end_pos":{"line":88,"col":49}},"use":{"file_name":"Bug1997.fst","start_pos":{"line":88,"col":27},"end_pos":{"line":88,"col":38}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___136`","While typechecking the top-level declaration `[@@expect_failure] let uu___136`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Bug1997.fst","start_pos":{"line":89,"col":39},"end_pos":{"line":89,"col":49}},"use":{"file_name":"Bug1997.fst","start_pos":{"line":89,"col":27},"end_pos":{"line":89,"col":38}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___137`","While typechecking the top-level declaration `[@@expect_failure] let uu___137`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Bug1997.fst","start_pos":{"line":90,"col":39},"end_pos":{"line":90,"col":49}},"use":{"file_name":"Bug1997.fst","start_pos":{"line":90,"col":27},"end_pos":{"line":90,"col":38}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___138`","While typechecking the top-level declaration `[@@expect_failure] let uu___138`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Bug1997.fst","start_pos":{"line":91,"col":39},"end_pos":{"line":91,"col":49}},"use":{"file_name":"Bug1997.fst","start_pos":{"line":91,"col":27},"end_pos":{"line":91,"col":38}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___139`","While typechecking the top-level declaration `[@@expect_failure] let uu___139`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Bug1997.fst","start_pos":{"line":92,"col":39},"end_pos":{"line":92,"col":49}},"use":{"file_name":"Bug1997.fst","start_pos":{"line":92,"col":27},"end_pos":{"line":92,"col":38}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___140`","While typechecking the top-level declaration `[@@expect_failure] let uu___140`"]} +>>] +Module after type checking: +module Bug1997 +Declarations: [ +let op_Equals_Hat a b = a + b +let test1 a b c = a =^ b =^ c +let test2 a b c = a =^ b =^ c +let test3 a b c = a =^ (b =^ c) +private +let _ = FStar.Pervasives.assert_norm (Bug1997.test1 == Bug1997.test2) +let imp_assoc_0 p q r = p ==> q ==> r +let imp_assoc_1 p q r = p ==> q ==> r +let imp_assoc_2 p q r = (p ==> q) ==> r +private +let _ = FStar.Pervasives.assert_norm (Bug1997.imp_assoc_0 == Bug1997.imp_assoc_1) +let imp_iff_0 p q r = p ==> q <==> r +let imp_iff_1 p q r = p ==> q <==> r +let imp_iff_2 p q r = p ==> (q <==> r) +private +let _ = FStar.Pervasives.assert_norm (Bug1997.imp_iff_0 == Bug1997.imp_iff_1) +let imp_conj_1 p q r s = p ==> q /\ r ==> s +let imp_conj_2 p q r s = (p ==> q) /\ (r ==> s) +let imp_conj_3 p q r s = p ==> q /\ (r ==> s) +let imp_conj_4 p q r s = p ==> q /\ r ==> s +private +let _ = FStar.Pervasives.assert_norm (Bug1997.imp_conj_1 == Bug1997.imp_conj_4) +let impneg1 p q r = p ==> q /\ ~p ==> r +let impneg2 p q r = (p ==> q) /\ (~p ==> r) +let impneg3 p q r = p ==> q /\ (~p ==> r) +let impneg4 p q r = p ==> q /\ ~p ==> r +private +let _ = FStar.Pervasives.assert_norm (Bug1997.impneg1 == Bug1997.impneg4) +let cd1 p q r = p /\ q \/ r +let cd2 p q r = p /\ q \/ r +let cd3 p q r = p /\ (q \/ r) +private +let _ = FStar.Pervasives.assert_norm (Bug1997.cd1 == Bug1997.cd2) +let m0 p q r s = p /\ (q \/ r) /\ s +let m1 p q r s = p /\ q \/ r /\ s +let m2 p q r s = p /\ q \/ r /\ s +let m3 p q r s = p /\ q \/ r /\ s +let m4 p q r s = p /\ q \/ r /\ s +private +let _ = FStar.Pervasives.assert_norm (Bug1997.m1 == Bug1997.m2) +private +let _ = FStar.Pervasives.assert_norm (Bug1997.m1 == Bug1997.m3) +private +let _ = FStar.Pervasives.assert_norm (Bug1997.m1 == Bug1997.m4) +let n0 p q r s = p \/ q /\ r \/ s +let n1 p q r s = p \/ q /\ r \/ s +let n2 p q r s = (p \/ q) /\ r \/ s +let n3 p q r s = (p \/ q) /\ (r \/ s) +let n4 p q r s = p \/ q /\ (r \/ s) +private +let _ = FStar.Pervasives.assert_norm (Bug1997.n0 == Bug1997.n1) +] + +Verified module: Bug1997 +All verification conditions discharged successfully diff --git a/tests/error-messages/Bug2010.fst.json_expected b/tests/error-messages/Bug2010.fst.json_expected new file mode 100644 index 00000000000..2c0b1ccafd8 --- /dev/null +++ b/tests/error-messages/Bug2010.fst.json_expected @@ -0,0 +1,5 @@ +>> Got issues: [ +{"msg":["Failed to resolve implicit argument ?14\nof type Prims.nat\nintroduced for user-provided implicit term at Bug2010.fst(6,66-6,67)"],"level":"Error","range":{"def":{"file_name":"Bug2010.fst","start_pos":{"line":6,"col":66},"end_pos":{"line":6,"col":67}},"use":{"file_name":"Bug2010.fst","start_pos":{"line":6,"col":66},"end_pos":{"line":6,"col":67}}},"number":66,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let concat'`","While typechecking the top-level declaration `[@@expect_failure] let concat'`"]} +>>] +Verified module: Bug2010 +All verification conditions discharged successfully diff --git a/tests/error-messages/Bug2021.fst.json_expected b/tests/error-messages/Bug2021.fst.json_expected new file mode 100644 index 00000000000..66aa2effca8 --- /dev/null +++ b/tests/error-messages/Bug2021.fst.json_expected @@ -0,0 +1,20 @@ +>> Got issues: [ +{"msg":["Failed to resolve implicit argument ?2\nof type Type\nintroduced for user-provided implicit term at Bug2021.fst(5,15-5,16)"],"level":"Error","range":{"def":{"file_name":"Bug2021.fst","start_pos":{"line":5,"col":15},"end_pos":{"line":5,"col":16}},"use":{"file_name":"Bug2021.fst","start_pos":{"line":5,"col":15},"end_pos":{"line":5,"col":16}}},"number":66,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let test0`","While typechecking the top-level declaration `[@@expect_failure] let test0`"]} +>>] +>> Got issues: [ +{"msg":["Failed to resolve implicit argument ?2\nof type Type\nintroduced for user-provided implicit term at Bug2021.fst(10,8-10,9)"],"level":"Error","range":{"def":{"file_name":"Bug2021.fst","start_pos":{"line":10,"col":8},"end_pos":{"line":10,"col":9}},"use":{"file_name":"Bug2021.fst","start_pos":{"line":10,"col":8},"end_pos":{"line":10,"col":9}}},"number":66,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let test1`","While typechecking the top-level declaration `[@@expect_failure] let test1`"]} +>>] +>> Got issues: [ +{"msg":["Failed to resolve implicit argument ?5\nof type Type\nintroduced for user-provided implicit term at Bug2021.fst(16,12-16,13)"],"level":"Error","range":{"def":{"file_name":"Bug2021.fst","start_pos":{"line":16,"col":12},"end_pos":{"line":16,"col":13}},"use":{"file_name":"Bug2021.fst","start_pos":{"line":16,"col":12},"end_pos":{"line":16,"col":13}}},"number":66,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let test2`","While typechecking the top-level declaration `[@@expect_failure] let test2`"]} +>>] +>> Got issues: [ +{"msg":["Failed to resolve implicit argument ?9\nof type Prims.int\nintroduced for Instantiating implicit argument"],"level":"Error","range":{"def":{"file_name":"Bug2021.fst","start_pos":{"line":23,"col":11},"end_pos":{"line":23,"col":12}},"use":{"file_name":"Bug2021.fst","start_pos":{"line":24,"col":13},"end_pos":{"line":24,"col":14}}},"number":66,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let test3`","While typechecking the top-level declaration `[@@expect_failure] let test3`"]} +>>] +>> Got issues: [ +{"msg":["Failed to resolve implicit argument ?10\nof type Prims.int\nintroduced for Instantiating implicit argument"],"level":"Error","range":{"def":{"file_name":"Bug2021.fst","start_pos":{"line":29,"col":11},"end_pos":{"line":29,"col":12}},"use":{"file_name":"Bug2021.fst","start_pos":{"line":30,"col":13},"end_pos":{"line":30,"col":17}}},"number":66,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let test4`","While typechecking the top-level declaration `[@@expect_failure] let test4`"]} +>>] +>> Got issues: [ +{"msg":["Failed to resolve implicit argument ?13\nof type Prims.int\nintroduced for Instantiating implicit argument"],"level":"Error","range":{"def":{"file_name":"Bug2021.fst","start_pos":{"line":36,"col":11},"end_pos":{"line":36,"col":12}},"use":{"file_name":"Bug2021.fst","start_pos":{"line":37,"col":13},"end_pos":{"line":37,"col":17}}},"number":66,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let test5`","While typechecking the top-level declaration `[@@expect_failure] let test5`"]} +>>] +Verified module: Bug2021 +All verification conditions discharged successfully diff --git a/tests/error-messages/Bug2245.fst.json_expected b/tests/error-messages/Bug2245.fst.json_expected new file mode 100644 index 00000000000..1d868b63567 --- /dev/null +++ b/tests/error-messages/Bug2245.fst.json_expected @@ -0,0 +1,5 @@ +>> Got issues: [ +{"msg":["Expected expression of type (Prims.int & Prims.int) & Prims.int\ngot expression a\nof type Prims.int & Prims.int & Prims.int"],"level":"Error","range":{"def":{"file_name":"Bug2245.fst","start_pos":{"line":6,"col":23},"end_pos":{"line":6,"col":24}},"use":{"file_name":"Bug2245.fst","start_pos":{"line":6,"col":23},"end_pos":{"line":6,"col":24}}},"number":189,"ctx":["While typechecking the top-level declaration `let b`","While typechecking the top-level declaration `[@@expect_failure] let b`"]} +>>] +Verified module: Bug2245 +All verification conditions discharged successfully diff --git a/tests/error-messages/Bug2820.fst.json_expected b/tests/error-messages/Bug2820.fst.json_expected new file mode 100644 index 00000000000..6a7d8d3ec05 --- /dev/null +++ b/tests/error-messages/Bug2820.fst.json_expected @@ -0,0 +1,21 @@ +Module after desugaring: +module Bug2820 +Declarations: [ +let basic _ = () <: FStar.Pervasives.Lemma (ensures forall (x: x: _{x + 1 == 1 + x}). Prims.l_True) +] + +Module before type checking: +module Bug2820 +Declarations: [ +let basic _ = () <: FStar.Pervasives.Lemma (ensures forall (x: x: _{x + 1 == 1 + x}). Prims.l_True) +] + +Module after type checking: +module Bug2820 +Declarations: [ +let basic _ = + () <: FStar.Pervasives.Lemma (ensures forall (x: Prims.int{x + 1 == 1 + x}). Prims.l_True) +] + +Verified module: Bug2820 +All verification conditions discharged successfully diff --git a/tests/error-messages/Bug2899.fst.json_expected b/tests/error-messages/Bug2899.fst.json_expected new file mode 100644 index 00000000000..740eddb1cc0 --- /dev/null +++ b/tests/error-messages/Bug2899.fst.json_expected @@ -0,0 +1,14 @@ +>> Got issues: [ +{"msg":["Tactic failed","Tactic got stuck!","Reduction stopped at: FStar.Stubs.Tactics.Result.Success (Prims.admit ())\n \"(((proofstate)))\"","The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?"],"level":"Error","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":212,"col":48},"end_pos":{"line":212,"col":58}},"use":{"file_name":"Bug2899.fst","start_pos":{"line":7,"col":12},"end_pos":{"line":7,"col":18}}},"number":170,"ctx":["While preprocessing VC with a tactic","While checking for top-level effects","While typechecking the top-level declaration `let test0`","While typechecking the top-level declaration `[@@expect_failure] let test0`"]} +>>] +>> Got issues: [ +{"msg":["Tactic failed","Tactic got stuck!","Reduction stopped at: Prims.admit ()","The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?"],"level":"Error","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":212,"col":48},"end_pos":{"line":212,"col":58}},"use":{"file_name":"Bug2899.fst","start_pos":{"line":10,"col":12},"end_pos":{"line":10,"col":18}}},"number":170,"ctx":["While preprocessing VC with a tactic","While checking for top-level effects","While typechecking the top-level declaration `let test1`","While typechecking the top-level declaration `[@@expect_failure] let test1`"]} +>>] +>> Got issues: [ +{"msg":["Tactic failed","Tactic got stuck!","Reduction stopped at: FStar.Stubs.Tactics.V2.Builtins.dump (Prims.admit ())\n \"(((proofstate)))\"","The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?"],"level":"Error","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":212,"col":48},"end_pos":{"line":212,"col":58}},"use":{"file_name":"Bug2899.fst","start_pos":{"line":13,"col":12},"end_pos":{"line":13,"col":18}}},"number":170,"ctx":["While preprocessing VC with a tactic","While checking for top-level effects","While typechecking the top-level declaration `let test2`","While typechecking the top-level declaration `[@@expect_failure] let test2`"]} +>>] +>> Got issues: [ +{"msg":["Tactic failed","Tactic got stuck!","Reduction stopped at: reify (tac ()) \"(((proofstate)))\"",""],"level":"Error","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":212,"col":48},"end_pos":{"line":212,"col":58}},"use":{"file_name":"Bug2899.fst","start_pos":{"line":17,"col":50},"end_pos":{"line":17,"col":66}}},"number":170,"ctx":["While preprocessing VC with a tactic","While typechecking the top-level declaration `let eval_tactic`","While typechecking the top-level declaration `[@@expect_failure] let eval_tactic`"]} +>>] +Verified module: Bug2899 +All verification conditions discharged successfully diff --git a/tests/error-messages/Bug2953.fst.json_expected b/tests/error-messages/Bug2953.fst.json_expected new file mode 100644 index 00000000000..1d33a583424 --- /dev/null +++ b/tests/error-messages/Bug2953.fst.json_expected @@ -0,0 +1,5 @@ +>> Got issues: [ +{"msg":["When clauses are not yet supported in --verify mode; they will be some day"],"level":"Error","range":{"def":{"file_name":"Bug2953.fst","start_pos":{"line":14,"col":21},"end_pos":{"line":14,"col":31}},"use":{"file_name":"Bug2953.fst","start_pos":{"line":14,"col":21},"end_pos":{"line":14,"col":31}}},"number":236,"ctx":["While typechecking the top-level declaration `let open_view`","While typechecking the top-level declaration `[@@expect_failure] let open_view`"]} +>>] +Verified module: Bug2953 +All verification conditions discharged successfully diff --git a/tests/error-messages/Bug2980.fst.json_expected b/tests/error-messages/Bug2980.fst.json_expected new file mode 100644 index 00000000000..0f65468c6bf --- /dev/null +++ b/tests/error-messages/Bug2980.fst.json_expected @@ -0,0 +1,5 @@ +>> Got issues: [ +{"msg":["Expected expression of type Type0\ngot expression Bug2980.t\nof type _: Prims.int -> Type0"],"level":"Error","range":{"def":{"file_name":"Bug2980.fst","start_pos":{"line":5,"col":4},"end_pos":{"line":5,"col":5}},"use":{"file_name":"Bug2980.fst","start_pos":{"line":5,"col":4},"end_pos":{"line":5,"col":5}}},"number":189,"ctx":["While typechecking the top-level declaration `type Bug2980.t`","While typechecking the top-level declaration `[@@expect_failure] type Bug2980.t`"]} +>>] +Verified module: Bug2980 +All verification conditions discharged successfully diff --git a/tests/error-messages/Bug2981.fst.json_expected b/tests/error-messages/Bug2981.fst.json_expected new file mode 100644 index 00000000000..b372344e166 --- /dev/null +++ b/tests/error-messages/Bug2981.fst.json_expected @@ -0,0 +1,5 @@ +>> Got issues: [ +{"msg":["Bound variable\n'g'\nescapes because of impure applications in the type of\n'check'","Add explicit let-bindings to avoid this"],"level":"Error","range":{"def":{"file_name":"Bug2981.fst","start_pos":{"line":10,"col":10},"end_pos":{"line":10,"col":27}},"use":{"file_name":"Bug2981.fst","start_pos":{"line":10,"col":10},"end_pos":{"line":10,"col":27}}},"number":56,"ctx":["While checking for escaped variables","While typechecking the top-level declaration `let test1`","While typechecking the top-level declaration `[@@expect_failure] let test1`"]} +>>] +Verified module: Bug2981 +All verification conditions discharged successfully diff --git a/tests/error-messages/Bug3099.fst.json_expected b/tests/error-messages/Bug3099.fst.json_expected new file mode 100644 index 00000000000..d079194cd8a --- /dev/null +++ b/tests/error-messages/Bug3099.fst.json_expected @@ -0,0 +1,7 @@ +proof-state: State dump @ depth 0 (X): +Location: Bug3099.fst(11,50-11,64) +Goal 1/1: +(_: Prims.unit), (return_val: Prims.eqtype), (_: return_val == Prims.int & (Prims.int & (Prims.int & Prims.int))), (any_result: Prims.bool), (_: true == any_result), (any_result'0: Prims.logical), (_: Prims.l_True == any_result'0) |- _ : Prims.squash ((1, (2, (3, 4))) = (1, (2, (3, 4)))) + +Verified module: Bug3099 +All verification conditions discharged successfully diff --git a/tests/error-messages/Bug3102.fst.json_expected b/tests/error-messages/Bug3102.fst.json_expected new file mode 100644 index 00000000000..8e4f47922ec --- /dev/null +++ b/tests/error-messages/Bug3102.fst.json_expected @@ -0,0 +1,20 @@ +>> Got issues: [ +{"msg":["Bound variable\n'e1'\nwould escape in the type of this letbinding","Add a type annotation that does not mention it"],"level":"Error","range":{"def":{"file_name":"Bug3102.fst","start_pos":{"line":8,"col":17},"end_pos":{"line":10,"col":9}},"use":{"file_name":"Bug3102.fst","start_pos":{"line":8,"col":17},"end_pos":{"line":10,"col":9}}},"number":56,"ctx":["While checking for escaped variables","While typechecking the top-level declaration `let min`","While typechecking the top-level declaration `[@@expect_failure] let min`"]} +>>] +>> Got issues: [ +{"msg":["(*?u23*) _ g t1 t2 is not equal to the expected type e2"],"level":"Error","range":{"def":{"file_name":"Bug3102.fst","start_pos":{"line":23,"col":4},"end_pos":{"line":23,"col":27}},"use":{"file_name":"Bug3102.fst","start_pos":{"line":23,"col":4},"end_pos":{"line":23,"col":27}}},"number":54,"ctx":["While solving deferred constraints","solve_non_tactic_deferred_constraints","While typechecking the top-level declaration `let test1`","While typechecking the top-level declaration `[@@expect_failure] let test1`"]} +>>] +>> Got issues: [ +{"msg":["(*?u20*) _ is not equal to the expected type e2"],"level":"Error","range":{"def":{"file_name":"Bug3102.fst","start_pos":{"line":29,"col":4},"end_pos":{"line":29,"col":27}},"use":{"file_name":"Bug3102.fst","start_pos":{"line":29,"col":4},"end_pos":{"line":29,"col":27}}},"number":54,"ctx":["While solving deferred constraints","solve_non_tactic_deferred_constraints","While typechecking the top-level declaration `let test2`","While typechecking the top-level declaration `[@@expect_failure] let test2`"]} +>>] +>> Got issues: [ +{"msg":["Bound variable\n'e2'\nwould escape in the type of this letbinding","Add a type annotation that does not mention it"],"level":"Error","range":{"def":{"file_name":"Bug3102.fst","start_pos":{"line":33,"col":29},"end_pos":{"line":35,"col":27}},"use":{"file_name":"Bug3102.fst","start_pos":{"line":33,"col":29},"end_pos":{"line":35,"col":27}}},"number":56,"ctx":["While checking for escaped variables","While typechecking the top-level declaration `let test3`","While typechecking the top-level declaration `[@@expect_failure] let test3`"]} +>>] +>> Got issues: [ +{"msg":["Bound variable\n'z'\nwould escape in the type of this letbinding","Add a type annotation that does not mention it"],"level":"Error","range":{"def":{"file_name":"Bug3102.fst","start_pos":{"line":41,"col":16},"end_pos":{"line":43,"col":8}},"use":{"file_name":"Bug3102.fst","start_pos":{"line":41,"col":16},"end_pos":{"line":43,"col":8}}},"number":56,"ctx":["While checking for escaped variables","While typechecking the top-level declaration `let gg`","While typechecking the top-level declaration `[@@expect_failure] let gg`"]} +>>] +>> Got issues: [ +{"msg":["Bound variable\n'z'\nwould escape in the type of this letbinding","Add a type annotation that does not mention it"],"level":"Error","range":{"def":{"file_name":"Bug3102.fst","start_pos":{"line":49,"col":16},"end_pos":{"line":51,"col":7}},"use":{"file_name":"Bug3102.fst","start_pos":{"line":49,"col":16},"end_pos":{"line":51,"col":7}}},"number":56,"ctx":["While checking for escaped variables","While typechecking the top-level declaration `let g`","While typechecking the top-level declaration `[@@expect_failure] let g`"]} +>>] +Verified module: Bug3102 +All verification conditions discharged successfully diff --git a/tests/error-messages/Bug3145.fst.json_expected b/tests/error-messages/Bug3145.fst.json_expected new file mode 100644 index 00000000000..f2c2f6f2486 --- /dev/null +++ b/tests/error-messages/Bug3145.fst.json_expected @@ -0,0 +1,29 @@ +Module after desugaring: +module Bug3145 +Declarations: [ +let t1 = Prims.int & Prims.int & Prims.int +let t2 = (Prims.int & Prims.int) & Prims.int +let t3 = Prims.int & (Prims.int & Prims.int) +let t4 = Prims.int & Prims.int & Prims.int +] + +Module before type checking: +module Bug3145 +Declarations: [ +let t1 = Prims.int & Prims.int & Prims.int +let t2 = (Prims.int & Prims.int) & Prims.int +let t3 = Prims.int & (Prims.int & Prims.int) +let t4 = Prims.int & Prims.int & Prims.int +] + +Module after type checking: +module Bug3145 +Declarations: [ +let t1 = Prims.int & Prims.int & Prims.int +let t2 = (Prims.int & Prims.int) & Prims.int +let t3 = Prims.int & (Prims.int & Prims.int) +let t4 = Prims.int & Prims.int & Prims.int +] + +Verified module: Bug3145 +All verification conditions discharged successfully diff --git a/tests/error-messages/Bug3227.fst.json_expected b/tests/error-messages/Bug3227.fst.json_expected new file mode 100644 index 00000000000..2da662f37fd --- /dev/null +++ b/tests/error-messages/Bug3227.fst.json_expected @@ -0,0 +1,76 @@ +Module after desugaring: +module Bug3227 +Declarations: [ +type box (a: Type) = { } + +let proj b = x (x (x b)) <: Prims.int +type box2 (a: Type) = | Box2 : x: a -> Bug3227.box2 a + + + +let test b = Box2? b && Box2? b.x +noeq +type boxf (a: Type) = { } + +let test2 r = ff r 5 +noeq +type boxfi (a: Type) = { } + +let test3 r = ff r +let test4 r x = ff r x <: a +] + +Module before type checking: +module Bug3227 +Declarations: [ +type box (a: Type) = { } + +let proj b = x (x (x b)) <: Prims.int +type box2 (a: Type) = | Box2 : x: a -> Bug3227.box2 a + + + +let test b = Box2? b && Box2? b.x +noeq +type boxf (a: Type) = { } + +let test2 r = ff r 5 +noeq +type boxfi (a: Type) = { } + +let test3 r = ff r +let test4 r x = ff r x <: a +] + +Module after type checking: +module Bug3227 +Declarations: [ +type box (a: Type) = { x:a } +val box__uu___haseq: forall (a: Type). {:pattern Prims.hasEq (Bug3227.box a)} + Prims.l_True /\ Prims.hasEq a ==> Prims.hasEq (Bug3227.box a) + + +let proj b = b.x.x.x <: Prims.int +type box2 (a: Type) = | Box2 : x: a -> Bug3227.box2 a +val box2__uu___haseq: forall (a: Type). {:pattern Prims.hasEq (Bug3227.box2 a)} + Prims.l_True /\ Prims.hasEq a ==> Prims.hasEq (Bug3227.box2 a) + + + + +let test b = Box2? b && Box2? b.x +noeq +type boxf (a: Type) = { ff:_: a -> a } + + +let test2 r = r.ff 5 +noeq +type boxfi (a: Type) = { ff:a } + + +let test3 r = r.ff +let test4 r x = r.ff x <: a +] + +Verified module: Bug3227 +All verification conditions discharged successfully diff --git a/tests/error-messages/Bug3292.fst.json_expected b/tests/error-messages/Bug3292.fst.json_expected new file mode 100644 index 00000000000..c8b1ebd3fc7 --- /dev/null +++ b/tests/error-messages/Bug3292.fst.json_expected @@ -0,0 +1,83 @@ +Module after desugaring: +module Bug3292 +Declarations: [ +#set-options "--print_implicits" +let op_Plus #a x y = x, y +let op_Minus #a x y = x, y +let op_Slash #a x y = x, y +let op_Greater #a x y = x, y +let op_Less #a x y = x, y +let op_GreaterEquals #a x y = x, y +let op_LessEquals #a x y = x, y +private +let _ = 1 + 1 +private +let _ = 1 - 1 +private +let _ = 1 / 1 +private +let _ = 1 > 1 +private +let _ = 1 < 1 +private +let _ = 1 >= 1 +private +let _ = 1 <= 1 +] + +Module before type checking: +module Bug3292 +Declarations: [ +#set-options "--print_implicits" +let op_Plus x y = x, y +let op_Minus x y = x, y +let op_Slash x y = x, y +let op_Greater x y = x, y +let op_Less x y = x, y +let op_GreaterEquals x y = x, y +let op_LessEquals x y = x, y +private +let _ = 1 + 1 +private +let _ = 1 - 1 +private +let _ = 1 / 1 +private +let _ = 1 > 1 +private +let _ = 1 < 1 +private +let _ = 1 >= 1 +private +let _ = 1 <= 1 +] + +Module after type checking: +module Bug3292 +Declarations: [ +#set-options "--print_implicits" +let op_Plus #a x y = FStar.Pervasives.Native.Mktuple2 #a #a x y +let op_Minus #a x y = FStar.Pervasives.Native.Mktuple2 #a #a x y +let op_Slash #a x y = FStar.Pervasives.Native.Mktuple2 #a #a x y +let op_Greater #a x y = FStar.Pervasives.Native.Mktuple2 #a #a x y +let op_Less #a x y = FStar.Pervasives.Native.Mktuple2 #a #a x y +let op_GreaterEquals #a x y = FStar.Pervasives.Native.Mktuple2 #a #a x y +let op_LessEquals #a x y = FStar.Pervasives.Native.Mktuple2 #a #a x y +private +let _ = Bug3292.op_Plus #Prims.int 1 1 +private +let _ = 1 - 1 +private +let _ = Bug3292.op_Slash #Prims.int 1 1 +private +let _ = Bug3292.op_Greater #Prims.int 1 1 +private +let _ = Bug3292.op_Less #Prims.int 1 1 +private +let _ = 1 >= 1 +private +let _ = 1 <= 1 +] + +Verified module: Bug3292 +All verification conditions discharged successfully diff --git a/tests/error-messages/Calc.fst.json_expected b/tests/error-messages/Calc.fst.json_expected new file mode 100644 index 00000000000..a67e9e7dba8 --- /dev/null +++ b/tests/error-messages/Calc.fst.json_expected @@ -0,0 +1,35 @@ +>> Got issues: [ +{"msg":["Could not prove that this calc-chain is compatible","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"FStar.Calc.fsti","start_pos":{"line":47,"col":50},"end_pos":{"line":47,"col":55}},"use":{"file_name":"Calc.fst","start_pos":{"line":12,"col":2},"end_pos":{"line":12,"col":13}}},"number":19,"ctx":["While typechecking the top-level declaration `let test_gt_lt_elab`","While typechecking the top-level declaration `[@@expect_failure] let test_gt_lt_elab`"]} +>>] +>> Got issues: [ +{"msg":["Could not prove that this calc-chain is compatible","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Calc.fst","start_pos":{"line":22,"col":7},"end_pos":{"line":22,"col":11}},"use":{"file_name":"Calc.fst","start_pos":{"line":22,"col":2},"end_pos":{"line":28,"col":3}}},"number":19,"ctx":["While typechecking the top-level declaration `let test_gt_lt`","While typechecking the top-level declaration `[@@expect_failure] let test_gt_lt`"]} +>>] +>> Got issues: [ +{"msg":["Could not prove that this calc-chain is compatible","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Calc.fst","start_pos":{"line":33,"col":7},"end_pos":{"line":33,"col":10}},"use":{"file_name":"Calc.fst","start_pos":{"line":33,"col":2},"end_pos":{"line":35,"col":3}}},"number":19,"ctx":["While typechecking the top-level declaration `let test_singl`","While typechecking the top-level declaration `[@@expect_failure] let test_singl`"]} +>>] +>> Got issues: [ +{"msg":["Could not prove that this calc-chain is compatible","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Calc.fst","start_pos":{"line":40,"col":7},"end_pos":{"line":40,"col":10}},"use":{"file_name":"Calc.fst","start_pos":{"line":40,"col":2},"end_pos":{"line":44,"col":3}}},"number":19,"ctx":["While typechecking the top-level declaration `let test`","While typechecking the top-level declaration `[@@expect_failure] let test`"]} +>>] +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type Prims.squash (1 == 2)\ngot type Prims.unit","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Calc.fst","start_pos":{"line":51,"col":3},"end_pos":{"line":51,"col":5}},"use":{"file_name":"Calc.fst","start_pos":{"line":51,"col":6},"end_pos":{"line":51,"col":8}}},"number":19,"ctx":["While typechecking the top-level declaration `let fail1`","While typechecking the top-level declaration `[@@expect_failure] let fail1`"]} +>>] +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type Prims.squash (2 == 3)\ngot type Prims.unit","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Calc.fst","start_pos":{"line":65,"col":3},"end_pos":{"line":65,"col":5}},"use":{"file_name":"Calc.fst","start_pos":{"line":65,"col":6},"end_pos":{"line":65,"col":8}}},"number":19,"ctx":["While typechecking the top-level declaration `let fail2`","While typechecking the top-level declaration `[@@expect_failure] let fail2`"]} +>>] +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type Prims.squash (3 == 4)\ngot type Prims.unit","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Calc.fst","start_pos":{"line":79,"col":3},"end_pos":{"line":79,"col":5}},"use":{"file_name":"Calc.fst","start_pos":{"line":79,"col":6},"end_pos":{"line":79,"col":8}}},"number":19,"ctx":["While typechecking the top-level declaration `let fail3`","While typechecking the top-level declaration `[@@expect_failure] let fail3`"]} +>>] +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type Prims.squash q\ngot type Prims.unit","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Calc.fst","start_pos":{"line":91,"col":20},"end_pos":{"line":91,"col":21}},"use":{"file_name":"Calc.fst","start_pos":{"line":93,"col":42},"end_pos":{"line":93,"col":44}}},"number":19,"ctx":["While typechecking the top-level declaration `let test_impl_elab`","While typechecking the top-level declaration `[@@expect_failure] let test_impl_elab`"]} +>>] +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type Prims.squash q\ngot type Prims.unit","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Calc.fst","start_pos":{"line":101,"col":4},"end_pos":{"line":101,"col":5}},"use":{"file_name":"Calc.fst","start_pos":{"line":100,"col":10},"end_pos":{"line":100,"col":12}}},"number":19,"ctx":["While typechecking the top-level declaration `let test_impl`","While typechecking the top-level declaration `[@@expect_failure] let test_impl`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Calc.fst","start_pos":{"line":105,"col":12},"end_pos":{"line":105,"col":17}},"use":{"file_name":"Calc.fst","start_pos":{"line":114,"col":17},"end_pos":{"line":114,"col":25}}},"number":19,"ctx":["While typechecking the top-level declaration `let test_1763_elab`","While typechecking the top-level declaration `[@@expect_failure] let test_1763_elab`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Calc.fst","start_pos":{"line":105,"col":12},"end_pos":{"line":105,"col":17}},"use":{"file_name":"Calc.fst","start_pos":{"line":121,"col":9},"end_pos":{"line":121,"col":17}}},"number":19,"ctx":["While typechecking the top-level declaration `let test_1763`","While typechecking the top-level declaration `[@@expect_failure] let test_1763`"]} +>>] +Verified module: Calc +All verification conditions discharged successfully diff --git a/tests/error-messages/CalcImpl.fst.json_expected b/tests/error-messages/CalcImpl.fst.json_expected new file mode 100644 index 00000000000..a966d0fb0a4 --- /dev/null +++ b/tests/error-messages/CalcImpl.fst.json_expected @@ -0,0 +1,161 @@ +Module after desugaring: +module CalcImpl +Declarations: [ +assume +val p:Prims.prop +assume +val q:Prims.prop +assume +val lem (_: Prims.unit) : FStar.Pervasives.Lemma (requires CalcImpl.p) (ensures CalcImpl.q) +let test _ = + FStar.Calc.calc_finish (fun x3 y4 -> x3 ==> y4 <: Type0) + (fun _ -> + FStar.Calc.calc_step (fun x5 y6 -> x5 ==> y6 <: Type0) + CalcImpl.q + (fun _ -> FStar.Calc.calc_init CalcImpl.p) + (fun _ -> FStar.Calc.calc_push_impl (fun _ -> CalcImpl.lem ()))) +let any p q = Prims.l_True +let test3 _ = + FStar.Calc.calc_finish (fun x18 y19 -> CalcImpl.any x18 y19 <: Type0) + (fun _ -> + FStar.Calc.calc_step (fun x24 y25 -> x24 <==> y25 <: Type0) + CalcImpl.q + (fun _ -> + FStar.Calc.calc_step (fun x22 y23 -> x22 ==> y23 <: Type0) + (CalcImpl.q /\ CalcImpl.q) + (fun _ -> + FStar.Calc.calc_step (fun x20 y21 -> x20 <==> y21 <: Type0) + CalcImpl.p + (fun _ -> FStar.Calc.calc_init (CalcImpl.p /\ CalcImpl.p)) + (fun _ -> ())) + (fun _ -> FStar.Calc.calc_push_impl (fun _ -> CalcImpl.lem ()))) + (fun _ -> ())) +let test4 _ = + FStar.Calc.calc_finish (fun x43 y44 -> CalcImpl.any x43 y44 <: Type0) + (fun _ -> + FStar.Calc.calc_step (fun x49 y50 -> x49 <==> y50 <: Type0) + CalcImpl.q + (fun _ -> + FStar.Calc.calc_step (fun x47 y48 -> x47 ==> y48 <: Type0) + (CalcImpl.q /\ CalcImpl.q) + (fun _ -> + FStar.Calc.calc_step (fun x45 y46 -> x45 <==> y46 <: Type0) + CalcImpl.p + (fun _ -> FStar.Calc.calc_init (CalcImpl.p /\ CalcImpl.p)) + (fun _ -> ())) + (fun _ -> FStar.Calc.calc_push_impl (fun _ -> CalcImpl.lem ()))) + (fun _ -> ())) +let op_Equals_Equals_Greater = Prims.op_LessThan +let test5 _ = + FStar.Calc.calc_finish (fun x68 y69 -> x68 ==> y69 <: Type0) + (fun _ -> + FStar.Calc.calc_step (fun x70 y71 -> x70 ==> y71 <: Type0) + 2 + (fun _ -> FStar.Calc.calc_init 1) + (fun _ -> ())) +] + +Module before type checking: +module CalcImpl +Declarations: [ +assume +val p:Prims.prop +assume +val q:Prims.prop +assume +val lem (_: Prims.unit) : FStar.Pervasives.Lemma (requires CalcImpl.p) (ensures CalcImpl.q) +let test _ = + FStar.Calc.calc_finish (fun x3 y4 -> x3 ==> y4 <: Type0) + (fun _ -> + FStar.Calc.calc_step (fun x5 y6 -> x5 ==> y6 <: Type0) + CalcImpl.q + (fun _ -> FStar.Calc.calc_init CalcImpl.p) + (fun _ -> FStar.Calc.calc_push_impl (fun _ -> CalcImpl.lem ()))) +let any p q = Prims.l_True +let test3 _ = + FStar.Calc.calc_finish (fun x18 y19 -> CalcImpl.any x18 y19 <: Type0) + (fun _ -> + FStar.Calc.calc_step (fun x24 y25 -> x24 <==> y25 <: Type0) + CalcImpl.q + (fun _ -> + FStar.Calc.calc_step (fun x22 y23 -> x22 ==> y23 <: Type0) + (CalcImpl.q /\ CalcImpl.q) + (fun _ -> + FStar.Calc.calc_step (fun x20 y21 -> x20 <==> y21 <: Type0) + CalcImpl.p + (fun _ -> FStar.Calc.calc_init (CalcImpl.p /\ CalcImpl.p)) + (fun _ -> ())) + (fun _ -> FStar.Calc.calc_push_impl (fun _ -> CalcImpl.lem ()))) + (fun _ -> ())) +let test4 _ = + FStar.Calc.calc_finish (fun x43 y44 -> CalcImpl.any x43 y44 <: Type0) + (fun _ -> + FStar.Calc.calc_step (fun x49 y50 -> x49 <==> y50 <: Type0) + CalcImpl.q + (fun _ -> + FStar.Calc.calc_step (fun x47 y48 -> x47 ==> y48 <: Type0) + (CalcImpl.q /\ CalcImpl.q) + (fun _ -> + FStar.Calc.calc_step (fun x45 y46 -> x45 <==> y46 <: Type0) + CalcImpl.p + (fun _ -> FStar.Calc.calc_init (CalcImpl.p /\ CalcImpl.p)) + (fun _ -> ())) + (fun _ -> FStar.Calc.calc_push_impl (fun _ -> CalcImpl.lem ()))) + (fun _ -> ())) +let op_Equals_Equals_Greater = Prims.op_LessThan +let test5 _ = + FStar.Calc.calc_finish (fun x68 y69 -> x68 ==> y69 <: Type0) + (fun _ -> + FStar.Calc.calc_step (fun x70 y71 -> x70 ==> y71 <: Type0) + 2 + (fun _ -> FStar.Calc.calc_init 1) + (fun _ -> ())) +] + +Module after type checking: +module CalcImpl +Declarations: [ +assume +val p:Prims.prop +assume +val q:Prims.prop +assume +val lem (_: Prims.unit) : FStar.Pervasives.Lemma (requires CalcImpl.p) (ensures CalcImpl.q) +let test _ = + calc ( ==> ) { + CalcImpl.p; + ( ==> ) { FStar.Calc.calc_push_impl (fun _ -> CalcImpl.lem ()) } + CalcImpl.q; + } +let any p q = Prims.l_True +let test3 _ = + calc (CalcImpl.any) { + CalcImpl.p /\ CalcImpl.p; + ( <==> ) { () } + CalcImpl.p; + ( ==> ) { FStar.Calc.calc_push_impl (fun _ -> CalcImpl.lem ()) } + CalcImpl.q /\ CalcImpl.q; + ( <==> ) { () } + CalcImpl.q; + } +let test4 _ = + calc (CalcImpl.any) { + CalcImpl.p /\ CalcImpl.p; + ( <==> ) { () } + CalcImpl.p; + ( ==> ) { FStar.Calc.calc_push_impl (fun _ -> CalcImpl.lem ()) } + CalcImpl.q /\ CalcImpl.q; + ( <==> ) { () } + CalcImpl.q; + } +let op_Equals_Equals_Greater = Prims.op_LessThan +let test5 _ = + calc ( ==> ) { + 1; + ( ==> ) { () } + 2; + } +] + +Verified module: CalcImpl +All verification conditions discharged successfully diff --git a/tests/error-messages/Coercions.fst.json_expected b/tests/error-messages/Coercions.fst.json_expected new file mode 100644 index 00000000000..5a3cfd212bc --- /dev/null +++ b/tests/error-messages/Coercions.fst.json_expected @@ -0,0 +1,23 @@ +>> Got issues: [ +{"msg":["Computed type Prims.int\nand effect GTot\nis not compatible with the annotated type Prims.int\nand effect Tot"],"level":"Error","range":{"def":{"file_name":"Coercions.fst","start_pos":{"line":6,"col":38},"end_pos":{"line":6,"col":39}},"use":{"file_name":"Coercions.fst","start_pos":{"line":6,"col":38},"end_pos":{"line":6,"col":39}}},"number":34,"ctx":["While typechecking the top-level declaration `let test0`","While typechecking the top-level declaration `[@@expect_failure] let test0`"]} +>>] +>> Got issues: [ +{"msg":["Computed type 'a\nand effect GTot\nis not compatible with the annotated type 'a\nand effect Tot"],"level":"Error","range":{"def":{"file_name":"Coercions.fst","start_pos":{"line":19,"col":37},"end_pos":{"line":19,"col":38}},"use":{"file_name":"Coercions.fst","start_pos":{"line":19,"col":37},"end_pos":{"line":19,"col":38}}},"number":34,"ctx":["While typechecking the top-level declaration `let test0'`","While typechecking the top-level declaration `[@@expect_failure] let test0'`"]} +>>] +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":680,"col":18},"end_pos":{"line":680,"col":24}},"use":{"file_name":"Coercions.fst","start_pos":{"line":71,"col":4},"end_pos":{"line":71,"col":8}}},"number":19,"ctx":["While typechecking the top-level declaration `let test_literal_bad`","While typechecking the top-level declaration `[@@expect_failure] let test_literal_bad`"]} +>>] +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":680,"col":18},"end_pos":{"line":680,"col":24}},"use":{"file_name":"Coercions.fst","start_pos":{"line":74,"col":49},"end_pos":{"line":74,"col":57}}},"number":19,"ctx":["While typechecking the top-level declaration `let test_int_nat_1`","While typechecking the top-level declaration `[@@expect_failure] let test_int_nat_1`"]} +>>] +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":680,"col":18},"end_pos":{"line":680,"col":24}},"use":{"file_name":"Coercions.fst","start_pos":{"line":76,"col":55},"end_pos":{"line":76,"col":56}}},"number":19,"ctx":["While typechecking the top-level declaration `let test_int_nat_2`","While typechecking the top-level declaration `[@@expect_failure] let test_int_nat_2`"]} +>>] +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":680,"col":18},"end_pos":{"line":680,"col":24}},"use":{"file_name":"Coercions.fst","start_pos":{"line":78,"col":50},"end_pos":{"line":78,"col":51}}},"number":19,"ctx":["While typechecking the top-level declaration `let test_int_nat_1'`","While typechecking the top-level declaration `[@@expect_failure] let test_int_nat_1'`"]} +>>] +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":680,"col":18},"end_pos":{"line":680,"col":24}},"use":{"file_name":"Coercions.fst","start_pos":{"line":80,"col":51},"end_pos":{"line":80,"col":52}}},"number":19,"ctx":["While typechecking the top-level declaration `let test_int_nat_2'`","While typechecking the top-level declaration `[@@expect_failure] let test_int_nat_2'`"]} +>>] +Verified module: Coercions +All verification conditions discharged successfully diff --git a/tests/error-messages/DTuples.fst.json_expected b/tests/error-messages/DTuples.fst.json_expected new file mode 100644 index 00000000000..060c892d55e --- /dev/null +++ b/tests/error-messages/DTuples.fst.json_expected @@ -0,0 +1,143 @@ +Module after desugaring: +module DTuples +Declarations: [ +private +let _ = a: Prims.int & b: Prims.int{a > b} & c: Prims.int{c == a + b} +private +let _ = a: Prims.int & b: Prims.int{a > b} & c: Prims.int{c == a + b} +private +let _ = a: Prims.int & z: b: Prims.int{a > b} & c: Prims.int{c == a + z} +private +let _ = a: Prims.int & b: Prims.int{a > b} & Prims.unit +private +let _ = a: Prims.int & b: Prims.int & Prims.int +private +let _ = a: Prims.int & b: Prims.int & c: Prims.int & Prims.int +private +let _ = a: Prims.int & b: Prims.int & c: Prims.int & d: Prims.int & Prims.int +private +let _ = Prims.int & Prims.int +private +let _ = Prims.int & Prims.int & Prims.int +private +let _ = Prims.int & Prims.int & Prims.int & Prims.int +private +let _ = Prims.int & Prims.int & Prims.int & Prims.int & Prims.int +private +let _ = Prims.int & (Prims.int & Prims.int) +private +let _ = Prims.int & (Prims.int & (Prims.int & Prims.int)) +private +let _ = Prims.int & (Prims.int & (Prims.int & (Prims.int & Prims.int))) +private +let _ = FStar.Pervasives.Native.tuple4 Prims.int Prims.bool +private +let _ = Prims.int & Prims.bool & Prims.string & Prims.unit +private +let _ = FStar.Pervasives.dtuple4 Prims.int (fun _ -> Prims.bool) +let t1 = 1, 2, 3 +let t2 = (1, 2), 3 +let t3 = 1, (2, 3) +let d1 = (| 1, 2, 3 |) +let d2 = (| (1, 2), 3 |) +let d3 = (| 1, (2, 3) |) +let dd2 = (| (| 1, 2 |), 3 |) +let dd3 = (| 1, (| 2, 3 |) |) +] + +Module before type checking: +module DTuples +Declarations: [ +private +let _ = a: Prims.int & b: Prims.int{a > b} & c: Prims.int{c == a + b} +private +let _ = a: Prims.int & b: Prims.int{a > b} & c: Prims.int{c == a + b} +private +let _ = a: Prims.int & z: b: Prims.int{a > b} & c: Prims.int{c == a + z} +private +let _ = a: Prims.int & b: Prims.int{a > b} & Prims.unit +private +let _ = a: Prims.int & b: Prims.int & Prims.int +private +let _ = a: Prims.int & b: Prims.int & c: Prims.int & Prims.int +private +let _ = a: Prims.int & b: Prims.int & c: Prims.int & d: Prims.int & Prims.int +private +let _ = Prims.int & Prims.int +private +let _ = Prims.int & Prims.int & Prims.int +private +let _ = Prims.int & Prims.int & Prims.int & Prims.int +private +let _ = Prims.int & Prims.int & Prims.int & Prims.int & Prims.int +private +let _ = Prims.int & (Prims.int & Prims.int) +private +let _ = Prims.int & (Prims.int & (Prims.int & Prims.int)) +private +let _ = Prims.int & (Prims.int & (Prims.int & (Prims.int & Prims.int))) +private +let _ = FStar.Pervasives.Native.tuple4 Prims.int Prims.bool +private +let _ = Prims.int & Prims.bool & Prims.string & Prims.unit +private +let _ = FStar.Pervasives.dtuple4 Prims.int (fun _ -> Prims.bool) +let t1 = 1, 2, 3 +let t2 = (1, 2), 3 +let t3 = 1, (2, 3) +let d1 = (| 1, 2, 3 |) +let d2 = (| (1, 2), 3 |) +let d3 = (| 1, (2, 3) |) +let dd2 = (| (| 1, 2 |), 3 |) +let dd3 = (| 1, (| 2, 3 |) |) +] + +Module after type checking: +module DTuples +Declarations: [ +private +let _ = a: Prims.int & b: Prims.int{a > b} & c: Prims.int{c == a + b} +private +let _ = a: Prims.int & b: Prims.int{a > b} & c: Prims.int{c == a + b} +private +let _ = a: Prims.int & z: b: Prims.int{a > b} & c: Prims.int{c == a + z} +private +let _ = a: Prims.int & b: Prims.int{a > b} & Prims.unit +private +let _ = a: Prims.int & b: Prims.int & Prims.int +private +let _ = a: Prims.int & b: Prims.int & c: Prims.int & Prims.int +private +let _ = a: Prims.int & b: Prims.int & c: Prims.int & d: Prims.int & Prims.int +private +let _ = Prims.int & Prims.int +private +let _ = Prims.int & Prims.int & Prims.int +private +let _ = Prims.int & Prims.int & Prims.int & Prims.int +private +let _ = Prims.int & Prims.int & Prims.int & Prims.int & Prims.int +private +let _ = Prims.int & (Prims.int & Prims.int) +private +let _ = Prims.int & (Prims.int & (Prims.int & Prims.int)) +private +let _ = Prims.int & (Prims.int & (Prims.int & (Prims.int & Prims.int))) +private +let _ = FStar.Pervasives.Native.tuple4 Prims.int Prims.bool +private +let _ = Prims.int & Prims.bool & Prims.string & Prims.unit +private +let _ = FStar.Pervasives.dtuple4 Prims.int (fun _ -> Prims.bool) +let t1 = 1, 2, 3 +let t2 = (1, 2), 3 +let t3 = 1, (2, 3) +let d1 = (| 1, 2, 3 |) +let d2 = (| (1, 2), 3 |) +let d3 = (| 1, (2, 3) |) +let dd2 = (| (| 1, 2 |), 3 |) +let dd3 = (| 1, (| 2, 3 |) |) +] + +Verified module: DTuples +All verification conditions discharged successfully diff --git a/tests/error-messages/DecreasesTypeWarning.fst.json_expected b/tests/error-messages/DecreasesTypeWarning.fst.json_expected new file mode 100644 index 00000000000..24cec7c5ef0 --- /dev/null +++ b/tests/error-messages/DecreasesTypeWarning.fst.json_expected @@ -0,0 +1,4 @@ +{"msg":["In the decreases clause for this function, the SMT solver may not be able to\nprove that the types of\n x (bound in DecreasesTypeWarning.fst(3,11-3,12))\nand xs (bound in DecreasesTypeWarning.fst(5,7-5,9))\nare equal.","The type of the first term is: Prims.nat","The type of the second term is: Prims.list Prims.nat","If the proof fails, try annotating these with the same type."],"level":"Warning","range":{"def":{"file_name":"DecreasesTypeWarning.fst","start_pos":{"line":3,"col":11},"end_pos":{"line":3,"col":12}},"use":{"file_name":"DecreasesTypeWarning.fst","start_pos":{"line":3,"col":11},"end_pos":{"line":3,"col":12}}},"number":290,"ctx":["While typechecking the top-level declaration `let rec f and g`"]} +{"msg":["In the decreases clause for this function, the SMT solver may not be able to\nprove that the types of\n xs (bound in DecreasesTypeWarning.fst(5,7-5,9))\nand x (bound in DecreasesTypeWarning.fst(3,11-3,12))\nare equal.","The type of the first term is: Prims.list Prims.nat","The type of the second term is: Prims.nat","If the proof fails, try annotating these with the same type."],"level":"Warning","range":{"def":{"file_name":"DecreasesTypeWarning.fst","start_pos":{"line":5,"col":7},"end_pos":{"line":5,"col":9}},"use":{"file_name":"DecreasesTypeWarning.fst","start_pos":{"line":5,"col":7},"end_pos":{"line":5,"col":9}}},"number":290,"ctx":["While typechecking the top-level declaration `let rec f and g`"]} +Verified module: DecreasesTypeWarning +All verification conditions discharged successfully diff --git a/tests/error-messages/DumpUvarsOf.fst.json_expected b/tests/error-messages/DumpUvarsOf.fst.json_expected new file mode 100644 index 00000000000..27641e26fca --- /dev/null +++ b/tests/error-messages/DumpUvarsOf.fst.json_expected @@ -0,0 +1,15 @@ +proof-state: State dump @ depth 1 (1): +Location: DumpUvarsOf.fst(13,4-13,12) +Goal 1/1: +(_: Prims.unit) |- _ : Prims.squash (DumpUvarsOf.p (*?u89*) _ (*?u90*) _) + +proof-state: State dump @ depth 1 (2): +Location: DumpUvarsOf.fst(14,4-14,36) +Goal 1/2: +(_: Prims.unit) |- _ : Prims.bool + +Goal 2/2: +(_: Prims.unit) |- _ : Prims.int + +Verified module: DumpUvarsOf +All verification conditions discharged successfully diff --git a/tests/error-messages/Erasable.fst.json_expected b/tests/error-messages/Erasable.fst.json_expected new file mode 100644 index 00000000000..08c75ccad90 --- /dev/null +++ b/tests/error-messages/Erasable.fst.json_expected @@ -0,0 +1,23 @@ +>> Got issues: [ +{"msg":["Incompatible attributes and qualifiers: erasable types do not support decidable\nequality and must be marked `noeq`."],"level":"Error","range":{"def":{"file_name":"Erasable.fst","start_pos":{"line":6,"col":0},"end_pos":{"line":8,"col":17}},"use":{"file_name":"Erasable.fst","start_pos":{"line":6,"col":0},"end_pos":{"line":8,"col":17}}},"number":162,"ctx":["While typechecking the top-level declaration `type Erasable.t0`","While typechecking the top-level declaration `[@@expect_failure] type Erasable.t0`"]} +>>] +>> Got issues: [ +{"msg":["Computed type Prims.int\nand effect Prims.GHOST\nis not compatible with the annotated type Prims.int\nand effect Tot"],"level":"Error","range":{"def":{"file_name":"Erasable.fst","start_pos":{"line":18,"col":2},"end_pos":{"line":20,"col":15}},"use":{"file_name":"Erasable.fst","start_pos":{"line":18,"col":2},"end_pos":{"line":20,"col":15}}},"number":34,"ctx":["While typechecking the top-level declaration `let test0_fail`","While typechecking the top-level declaration `[@@expect_failure] let test0_fail`"]} +>>] +>> Got issues: [ +{"msg":["Computed type Prims.int\nand effect GTot\nis not compatible with the annotated type Prims.int\nand effect Tot"],"level":"Error","range":{"def":{"file_name":"Erasable.fst","start_pos":{"line":28,"col":42},"end_pos":{"line":28,"col":52}},"use":{"file_name":"Erasable.fst","start_pos":{"line":28,"col":42},"end_pos":{"line":28,"col":52}}},"number":34,"ctx":["While typechecking the top-level declaration `let test1_fail`","While typechecking the top-level declaration `[@@expect_failure] let test1_fail`"]} +>>] +>> Got issues: [ +{"msg":["Illegal attribute: the `erasable` attribute is only permitted on inductive type\ndefinitions and abbreviations for non-informative types.","The term\nPrims.nat\nis considered informative."],"level":"Error","range":{"def":{"file_name":"Erasable.fst","start_pos":{"line":41,"col":12},"end_pos":{"line":41,"col":15}},"use":{"file_name":"Erasable.fst","start_pos":{"line":41,"col":12},"end_pos":{"line":41,"col":15}}},"number":162,"ctx":["While typechecking the top-level declaration `let e_nat`","While typechecking the top-level declaration `[@@expect_failure] let e_nat`"]} +>>] +>> Got issues: [ +{"msg":["Mismatch of attributes between declaration and definition.","Declaration is marked `erasable` but the definition is not."],"level":"Error","range":{"def":{"file_name":"Erasable.fst","start_pos":{"line":52,"col":0},"end_pos":{"line":52,"col":17}},"use":{"file_name":"Erasable.fst","start_pos":{"line":52,"col":0},"end_pos":{"line":52,"col":17}}},"number":162,"ctx":["While typechecking the top-level declaration `let e_nat_2`","While typechecking the top-level declaration `[@@expect_failure] let e_nat_2`"]} +>>] +>> Got issues: [ +{"msg":["Mismatch of attributes between declaration and definition.","Declaration is marked `erasable` but the definition is not."],"level":"Error","range":{"def":{"file_name":"Erasable.fst","start_pos":{"line":59,"col":0},"end_pos":{"line":59,"col":29}},"use":{"file_name":"Erasable.fst","start_pos":{"line":59,"col":0},"end_pos":{"line":59,"col":29}}},"number":162,"ctx":["While typechecking the top-level declaration `type Erasable.e_nat_3`","While typechecking the top-level declaration `[@@expect_failure] type Erasable.e_nat_3`"]} +>>] +{"msg":["Erasable.e_nat_2\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"Erasable.fst","start_pos":{"line":49,"col":4},"end_pos":{"line":49,"col":11}},"use":{"file_name":"Erasable.fst","start_pos":{"line":49,"col":4},"end_pos":{"line":49,"col":11}}},"number":240,"ctx":["While desugaring module Erasable"]} +{"msg":["Erasable.e_nat_3\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"Erasable.fst","start_pos":{"line":56,"col":4},"end_pos":{"line":56,"col":11}},"use":{"file_name":"Erasable.fst","start_pos":{"line":56,"col":4},"end_pos":{"line":56,"col":11}}},"number":240,"ctx":["While desugaring module Erasable"]} +{"msg":["Missing definitions in module Erasable:\n e_nat_2\n e_nat_3"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"Erasable.fst","start_pos":{"line":73,"col":0},"end_pos":{"line":73,"col":19}}},"number":240,"ctx":[]} +Verified module: Erasable +All verification conditions discharged successfully diff --git a/tests/error-messages/ExpectFailure.fst.json_expected b/tests/error-messages/ExpectFailure.fst.json_expected new file mode 100644 index 00000000000..e867cfa3742 --- /dev/null +++ b/tests/error-messages/ExpectFailure.fst.json_expected @@ -0,0 +1,23 @@ +>> Got issues: [ +{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":20,"col":12},"end_pos":{"line":20,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":20,"col":12},"end_pos":{"line":20,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]} +>>] +>> Got issues: [ +{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":24,"col":12},"end_pos":{"line":24,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":24,"col":12},"end_pos":{"line":24,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___1`","While typechecking the top-level declaration `[@@expect_failure] let uu___1`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":28,"col":15},"end_pos":{"line":28,"col":20}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":28,"col":8},"end_pos":{"line":28,"col":14}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___2`","While typechecking the top-level declaration `[@@expect_failure] let uu___2`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":30,"col":15},"end_pos":{"line":30,"col":20}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":30,"col":8},"end_pos":{"line":30,"col":14}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___3`","While typechecking the top-level declaration `[@@expect_failure] let uu___3`"]} +>>] +>> Got issues: [ +{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":43,"col":12},"end_pos":{"line":43,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":43,"col":12},"end_pos":{"line":43,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___6`","While typechecking the top-level declaration `[@@expect_failure] let uu___6`"]} +>>] +>> Got issues: [ +{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":50,"col":12},"end_pos":{"line":50,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":50,"col":12},"end_pos":{"line":50,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___7`","While typechecking the top-level declaration `[@@expect_failure] let uu___7`"]} +>>] +>> Got issues: [ +{"msg":["Expected expression of type Prims.int\ngot expression 'a'\nof type FStar.Char.char"],"level":"Error","range":{"def":{"file_name":"ExpectFailure.fst","start_pos":{"line":61,"col":12},"end_pos":{"line":61,"col":15}},"use":{"file_name":"ExpectFailure.fst","start_pos":{"line":61,"col":12},"end_pos":{"line":61,"col":15}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___8`","While typechecking the top-level declaration `[@@expect_failure] let uu___8`"]} +>>] +Verified module: ExpectFailure +All verification conditions discharged successfully diff --git a/tests/error-messages/GhostImplicits.fst.json_expected b/tests/error-messages/GhostImplicits.fst.json_expected new file mode 100644 index 00000000000..e4970e81d41 --- /dev/null +++ b/tests/error-messages/GhostImplicits.fst.json_expected @@ -0,0 +1,5 @@ +>> Got issues: [ +{"msg":["Computed type Prims.nat\nand effect Prims.GHOST\nis not compatible with the annotated type Prims.nat\nand effect Tot"],"level":"Error","range":{"def":{"file_name":"GhostImplicits.fst","start_pos":{"line":25,"col":54},"end_pos":{"line":25,"col":57}},"use":{"file_name":"GhostImplicits.fst","start_pos":{"line":25,"col":54},"end_pos":{"line":25,"col":57}}},"number":34,"ctx":["While typechecking the top-level declaration `let test3`","While typechecking the top-level declaration `[@@expect_failure] let test3`"]} +>>] +Verified module: GhostImplicits +All verification conditions discharged successfully diff --git a/tests/error-messages/IfCond.fst.json_expected b/tests/error-messages/IfCond.fst.json_expected new file mode 100644 index 00000000000..ee8e7bcc5f3 --- /dev/null +++ b/tests/error-messages/IfCond.fst.json_expected @@ -0,0 +1,5 @@ +>> Got issues: [ +{"msg":["Expected expression of type Prims.bool\ngot expression 2\nof type Prims.int"],"level":"Error","range":{"def":{"file_name":"IfCond.fst","start_pos":{"line":4,"col":17},"end_pos":{"line":4,"col":18}},"use":{"file_name":"IfCond.fst","start_pos":{"line":4,"col":17},"end_pos":{"line":4,"col":18}}},"number":189,"ctx":["While typechecking the top-level declaration `let test`","While typechecking the top-level declaration `[@@expect_failure] let test`"]} +>>] +Verified module: IfCond +All verification conditions discharged successfully diff --git a/tests/error-messages/IfThen.fst.json_expected b/tests/error-messages/IfThen.fst.json_expected new file mode 100644 index 00000000000..62146ad901a --- /dev/null +++ b/tests/error-messages/IfThen.fst.json_expected @@ -0,0 +1,5 @@ +>> Got issues: [ +{"msg":["Expected expression of type Prims.int\ngot expression ()\nof type Prims.unit"],"level":"Error","range":{"def":{"file_name":"IfThen.fst","start_pos":{"line":5,"col":2},"end_pos":{"line":6,"col":6}},"use":{"file_name":"IfThen.fst","start_pos":{"line":5,"col":2},"end_pos":{"line":6,"col":6}}},"number":189,"ctx":["While typechecking the top-level declaration `let test`","While typechecking the top-level declaration `[@@expect_failure] let test`"]} +>>] +Verified module: IfThen +All verification conditions discharged successfully diff --git a/tests/error-messages/Inference.fst.json_expected b/tests/error-messages/Inference.fst.json_expected new file mode 100644 index 00000000000..bd6d4c0098f --- /dev/null +++ b/tests/error-messages/Inference.fst.json_expected @@ -0,0 +1,6 @@ +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type Prims.eqtype\ngot type Type0","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":73,"col":23},"end_pos":{"line":73,"col":30}},"use":{"file_name":"Inference.fst","start_pos":{"line":20,"col":14},"end_pos":{"line":20,"col":15}}},"number":19,"ctx":["While typechecking the top-level declaration `let alloc_fails`","While typechecking the top-level declaration `[@@expect_failure] let alloc_fails`"]} +{"msg":["Subtyping check failed","Expected type Prims.eqtype\ngot type Type0","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":73,"col":23},"end_pos":{"line":73,"col":30}},"use":{"file_name":"Inference.fst","start_pos":{"line":20,"col":14},"end_pos":{"line":20,"col":15}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let alloc_fails`","While typechecking the top-level declaration `[@@expect_failure] let alloc_fails`"]} +>>] +Verified module: Inference +All verification conditions discharged successfully diff --git a/tests/error-messages/Makefile b/tests/error-messages/Makefile index 0ea77d42015..0a916b2a11a 100644 --- a/tests/error-messages/Makefile +++ b/tests/error-messages/Makefile @@ -1,4 +1,5 @@ FSTAR_HOME=../.. +all: check-all FSTAR_FILES=$(wildcard *.fst) @@ -18,43 +19,63 @@ OTHERFLAGS+=--already_cached 'Prims FStar' OTHERFLAGS := $(filter-out --query_stats, $(OTHERFLAGS)) OTHERFLAGS := $(filter-out --hint_info, $(OTHERFLAGS)) -check-all: $(addsuffix .check, $(FSTAR_FILES)) -all: check-all +check-all: $(addsuffix .human_check, $(FSTAR_FILES)) \ + $(addsuffix .json_check, $(FSTAR_FILES)) # For these tests, we check that the resugared output -# matches the expected file. -Bug1997.fst.output: OTHERFLAGS+=--dump_module Bug1997 -Bug2820.fst.output: OTHERFLAGS+=--dump_module Bug2820 -Bug3145.fst.output: OTHERFLAGS+=--dump_module Bug3145 -Bug3227.fst.output: OTHERFLAGS+=--dump_module Bug3227 -Bug3292.fst.output: OTHERFLAGS+=--dump_module Bug3292 -CalcImpl.fst.output: OTHERFLAGS+=--dump_module CalcImpl -DTuples.fst.output: OTHERFLAGS+=--dump_module DTuples -SeqLit.fst.output: OTHERFLAGS+=--dump_module SeqLit +# matches the expected file. We have to repeat the lines for +# json_output, sadly. +Bug1997.fst.json_output : OTHERFLAGS+=--dump_module Bug1997 +Bug1997.fst.output : OTHERFLAGS+=--dump_module Bug1997 +Bug2820.fst.json_output : OTHERFLAGS+=--dump_module Bug2820 +Bug2820.fst.output : OTHERFLAGS+=--dump_module Bug2820 +Bug3145.fst.json_output : OTHERFLAGS+=--dump_module Bug3145 +Bug3145.fst.output : OTHERFLAGS+=--dump_module Bug3145 +Bug3227.fst.json_output : OTHERFLAGS+=--dump_module Bug3227 +Bug3227.fst.output : OTHERFLAGS+=--dump_module Bug3227 +Bug3292.fst.json_output : OTHERFLAGS+=--dump_module Bug3292 +Bug3292.fst.output : OTHERFLAGS+=--dump_module Bug3292 +CalcImpl.fst.json_output : OTHERFLAGS+=--dump_module CalcImpl +CalcImpl.fst.output : OTHERFLAGS+=--dump_module CalcImpl +DTuples.fst.json_output : OTHERFLAGS+=--dump_module DTuples +DTuples.fst.output : OTHERFLAGS+=--dump_module DTuples +SeqLit.fst.json_output : OTHERFLAGS+=--dump_module SeqLit +SeqLit.fst.output : OTHERFLAGS+=--dump_module SeqLit include $(FSTAR_HOME)/examples/Makefile.common -%.check: %.expected %.output +.PHONY: %.human_check +%.human_check: %.expected %.output + $(Q)diff -u --strip-trailing-cr $^ + $(Q)touch $@ + +.PHONY: %.json_check +%.json_check: %.json_expected %.json_output $(Q)diff -u --strip-trailing-cr $^ $(Q)touch $@ -%.accept: %.output - $(Q)cp $< $(patsubst %.output,%.expected,$<) +.PHONY: %.accept +%.accept: %.output %.json_output + $(Q)R=$(patsubst %.output,%,$<) && \ + cp $$R.output $$R.expected && \ + cp $$R.json_output $$R.json_expected +.PHONY: %.clean clean: $(call msg, "CLEAN", $<) $(Q)rm -f .depend - $(Q)rm -f *.check $(Q)rm -f *.output + $(Q)rm -f *.json_output $(Q)rm -rf _output $(Q)rm -rf _cache +.PHONY: accept accept: $(addsuffix .accept, $(FSTAR_FILES)) -.PHONY: %.check - # Re-do all tests +.PHONY: re re: clean all # Keep the output files so we can look at them easily .SECONDARY: $(patsubst %,%.output,$(FSTAR_FILES)) +.SECONDARY: $(patsubst %,%.json_output,$(FSTAR_FILES)) diff --git a/tests/error-messages/NegativeTests.BST.fst.json_expected b/tests/error-messages/NegativeTests.BST.fst.json_expected new file mode 100644 index 00000000000..b74b518fc33 --- /dev/null +++ b/tests/error-messages/NegativeTests.BST.fst.json_expected @@ -0,0 +1,11 @@ +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type\n right:\n FStar.Pervasives.Native.option (tree 2)\n { 0 <= 1 /\\ 1 <= 2 /\\ None? right == (1 = 2) /\\\n None? FStar.Pervasives.Native.None == (1 = 0) }\ngot type FStar.Pervasives.Native.option (tree 2)","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"NegativeTests.BST.fst","start_pos":{"line":27,"col":36},"end_pos":{"line":27,"col":58}},"use":{"file_name":"NegativeTests.BST.fst","start_pos":{"line":37,"col":38},"end_pos":{"line":37,"col":42}}},"number":19,"ctx":["While typechecking the top-level declaration `let bad_node_1`","While typechecking the top-level declaration `[@@expect_failure] let bad_node_1`"]} +>>] +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type\n right:\n FStar.Pervasives.Native.option (tree (l + 1))\n { l <= l /\\ l <= l + 1 /\\ None? right == (l = l + 1) /\\\n None? (FStar.Pervasives.Native.Some t) == (l = l) }\ngot type FStar.Pervasives.Native.option (tree (l + 1))","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"NegativeTests.BST.fst","start_pos":{"line":27,"col":36},"end_pos":{"line":27,"col":58}},"use":{"file_name":"NegativeTests.BST.fst","start_pos":{"line":40,"col":61},"end_pos":{"line":40,"col":65}}},"number":19,"ctx":["While typechecking the top-level declaration `let bad_node_2`","While typechecking the top-level declaration `[@@expect_failure] let bad_node_2`"]} +>>] +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type\n right:\n FStar.Pervasives.Native.option (tree (l + 1))\n { l <= l + 1 /\\ l + 1 <= l + 1 /\\ None? right == (l + 1 = l + 1) /\\\n None? (FStar.Pervasives.Native.Some t1) == (l + 1 = l) }\ngot type FStar.Pervasives.Native.option (tree (l + 1))","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"NegativeTests.BST.fst","start_pos":{"line":27,"col":36},"end_pos":{"line":27,"col":58}},"use":{"file_name":"NegativeTests.BST.fst","start_pos":{"line":43,"col":78},"end_pos":{"line":43,"col":87}}},"number":19,"ctx":["While typechecking the top-level declaration `let bad_node_3`","While typechecking the top-level declaration `[@@expect_failure] let bad_node_3`"]} +>>] +Verified module: NegativeTests.BST +All verification conditions discharged successfully diff --git a/tests/error-messages/NegativeTests.Bug260.fst.json_expected b/tests/error-messages/NegativeTests.Bug260.fst.json_expected new file mode 100644 index 00000000000..8fa52c910cf --- /dev/null +++ b/tests/error-messages/NegativeTests.Bug260.fst.json_expected @@ -0,0 +1,7 @@ +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type validity (S (S t))\ngot type validity (S t)","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"NegativeTests.Bug260.fst","start_pos":{"line":23,"col":37},"end_pos":{"line":26,"col":9}},"use":{"file_name":"NegativeTests.Bug260.fst","start_pos":{"line":26,"col":12},"end_pos":{"line":26,"col":19}}},"number":19,"ctx":["While typechecking the top-level declaration `let bad`","While typechecking the top-level declaration `[@@expect_failure] let bad`"]} +>>] +{"msg":["NegativeTests.Bug260.bad\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"NegativeTests.Bug260.fst","start_pos":{"line":23,"col":4},"end_pos":{"line":23,"col":7}},"use":{"file_name":"NegativeTests.Bug260.fst","start_pos":{"line":23,"col":4},"end_pos":{"line":23,"col":7}}},"number":240,"ctx":["While desugaring module NegativeTests.Bug260"]} +{"msg":["Missing definitions in module NegativeTests.Bug260: bad"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"NegativeTests.Bug260.fst","start_pos":{"line":36,"col":0},"end_pos":{"line":36,"col":34}}},"number":240,"ctx":[]} +Verified module: NegativeTests.Bug260 +All verification conditions discharged successfully diff --git a/tests/error-messages/NegativeTests.False.fst.json_expected b/tests/error-messages/NegativeTests.False.fst.json_expected new file mode 100644 index 00000000000..c5c93b87420 --- /dev/null +++ b/tests/error-messages/NegativeTests.False.fst.json_expected @@ -0,0 +1,12 @@ +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":459,"col":77},"end_pos":{"line":459,"col":89}},"use":{"file_name":"NegativeTests.False.fst","start_pos":{"line":23,"col":13},"end_pos":{"line":23,"col":33}}},"number":19,"ctx":["While typechecking the top-level declaration `let bar`","While typechecking the top-level declaration `[@@expect_failure] let bar`"]} +>>] +>> Got issues: [ +{"msg":["Expected type Prims.l_True \\/ Prims.l_True\nbut Prims.Left Prims.T\nhas type Prims.sum (*?u1*) _ Prims.l_True"],"level":"Error","range":{"def":{"file_name":"NegativeTests.False.fst","start_pos":{"line":30,"col":18},"end_pos":{"line":30,"col":41}},"use":{"file_name":"NegativeTests.False.fst","start_pos":{"line":30,"col":18},"end_pos":{"line":30,"col":41}}},"number":12,"ctx":["While typechecking the top-level declaration `let absurd`","While typechecking the top-level declaration `[@@expect_failure] let absurd`"]} +{"msg":["Expected type Prims.l_True \\/ Prims.l_True\nbut Prims.Right Prims.T\nhas type Prims.sum Prims.l_True (*?u6*) _"],"level":"Error","range":{"def":{"file_name":"NegativeTests.False.fst","start_pos":{"line":30,"col":42},"end_pos":{"line":30,"col":66}},"use":{"file_name":"NegativeTests.False.fst","start_pos":{"line":30,"col":42},"end_pos":{"line":30,"col":66}}},"number":12,"ctx":["While typechecking the top-level declaration `let absurd`","While typechecking the top-level declaration `[@@expect_failure] let absurd`"]} +>>] +{"msg":["NegativeTests.False.bar\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"NegativeTests.False.fst","start_pos":{"line":21,"col":4},"end_pos":{"line":21,"col":7}},"use":{"file_name":"NegativeTests.False.fst","start_pos":{"line":21,"col":4},"end_pos":{"line":21,"col":7}}},"number":240,"ctx":["While desugaring module NegativeTests.False"]} +{"msg":["NegativeTests.False.absurd\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"NegativeTests.False.fst","start_pos":{"line":28,"col":4},"end_pos":{"line":28,"col":10}},"use":{"file_name":"NegativeTests.False.fst","start_pos":{"line":28,"col":4},"end_pos":{"line":28,"col":10}}},"number":240,"ctx":["While desugaring module NegativeTests.False"]} +{"msg":["Missing definitions in module NegativeTests.False:\n absurd\n bar"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"NegativeTests.False.fst","start_pos":{"line":30,"col":0},"end_pos":{"line":30,"col":66}}},"number":240,"ctx":[]} +Verified module: NegativeTests.False +All verification conditions discharged successfully diff --git a/tests/error-messages/NegativeTests.Heap.fst.json_expected b/tests/error-messages/NegativeTests.Heap.fst.json_expected new file mode 100644 index 00000000000..d2483620e64 --- /dev/null +++ b/tests/error-messages/NegativeTests.Heap.fst.json_expected @@ -0,0 +1,5 @@ +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"NegativeTests.Heap.fst","start_pos":{"line":26,"col":21},"end_pos":{"line":26,"col":54}},"use":{"file_name":"NegativeTests.Heap.fst","start_pos":{"line":26,"col":21},"end_pos":{"line":26,"col":54}}},"number":19,"ctx":["While typechecking the top-level declaration `let test2`","While typechecking the top-level declaration `[@@expect_failure] let test2`"]} +>>] +Verified module: NegativeTests.Heap +All verification conditions discharged successfully diff --git a/tests/error-messages/NegativeTests.Neg.fst.json_expected b/tests/error-messages/NegativeTests.Neg.fst.json_expected new file mode 100644 index 00000000000..7525f0ac3d6 --- /dev/null +++ b/tests/error-messages/NegativeTests.Neg.fst.json_expected @@ -0,0 +1,41 @@ +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":680,"col":18},"end_pos":{"line":680,"col":24}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":20,"col":8},"end_pos":{"line":20,"col":10}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let x`","While typechecking the top-level declaration `[@@expect_failure] let x`"]} +>>] +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":680,"col":18},"end_pos":{"line":680,"col":24}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":24,"col":8},"end_pos":{"line":24,"col":10}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let y`","While typechecking the top-level declaration `[@@expect_failure] let y`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":27,"col":30},"end_pos":{"line":27,"col":35}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":27,"col":30},"end_pos":{"line":27,"col":35}}},"number":19,"ctx":["While typechecking the top-level declaration `let assert_0_eq_1`","While typechecking the top-level declaration `[@@expect_failure] let assert_0_eq_1`"]} +>>] +>> Got issues: [ +{"msg":["Patterns are incomplete","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":30,"col":28},"end_pos":{"line":31,"col":15}}},"number":19,"ctx":["While typechecking the top-level declaration `let hd_int_inexhaustive`","While typechecking the top-level declaration `[@@expect_failure] let hd_int_inexhaustive`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":33,"col":44},"end_pos":{"line":33,"col":57}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":38,"col":32},"end_pos":{"line":38,"col":42}}},"number":19,"ctx":["While typechecking the top-level declaration `let test_precondition_label`","While typechecking the top-level declaration `[@@expect_failure] let test_precondition_label`"]} +>>] +>> Got issues: [ +{"msg":["Could not prove post-condition","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":40,"col":83},"end_pos":{"line":40,"col":88}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":42,"col":33},"end_pos":{"line":42,"col":34}}},"number":19,"ctx":["While typechecking the top-level declaration `let test_postcondition_label`","While typechecking the top-level declaration `[@@expect_failure] let test_postcondition_label`"]} +>>] +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type _: FStar.Pervasives.Native.option 'a {Some? _}\ngot type FStar.Pervasives.Native.option 'a","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"FStar.Pervasives.Native.fst","start_pos":{"line":33,"col":4},"end_pos":{"line":33,"col":8}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":46,"col":30},"end_pos":{"line":46,"col":31}}},"number":19,"ctx":["While typechecking the top-level declaration `let bad_projector`","While typechecking the top-level declaration `[@@expect_failure] let bad_projector`"]} +>>] +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type _: FStar.Pervasives.result Prims.int {V? _}\ngot type FStar.Pervasives.result Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"FStar.Pervasives.fsti","start_pos":{"line":519,"col":4},"end_pos":{"line":519,"col":5}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":50,"col":45},"end_pos":{"line":50,"col":47}}},"number":19,"ctx":["While typechecking the top-level declaration `val NegativeTests.Neg.test`","While typechecking the top-level declaration `[@@expect_failure] val NegativeTests.Neg.test`"]} +>>] +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":680,"col":18},"end_pos":{"line":680,"col":24}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":55,"col":25},"end_pos":{"line":55,"col":26}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let h1`","While typechecking the top-level declaration `[@@expect_failure] let h1`"]} +>>] +>> Got issues: [ +{"msg":["Type annotation _: Type0{NegativeTests.Neg.phi_1510} for inductive\nNegativeTests.Neg.t is not Type or eqtype, or it is eqtype but contains\nnoeq/unopteq qualifiers"],"level":"Error","range":{"def":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":59,"col":5},"end_pos":{"line":59,"col":6}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":59,"col":5},"end_pos":{"line":59,"col":6}}},"number":309,"ctx":["While typechecking the top-level declaration `type NegativeTests.Neg.t`","While typechecking the top-level declaration `[@@expect_failure] type NegativeTests.Neg.t`"]} +>>] +>> Got issues: [ +{"msg":["Type annotation _: Type{Prims.l_False} for inductive NegativeTests.Neg.t2 is not\nType or eqtype, or it is eqtype but contains noeq/unopteq qualifiers"],"level":"Error","range":{"def":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":63,"col":5},"end_pos":{"line":63,"col":7}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":63,"col":5},"end_pos":{"line":63,"col":7}}},"number":309,"ctx":["While typechecking the top-level declaration `type NegativeTests.Neg.t2`","While typechecking the top-level declaration `[@@expect_failure] type NegativeTests.Neg.t2`"]} +>>] +{"msg":["NegativeTests.Neg.x\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":18,"col":4},"end_pos":{"line":18,"col":5}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":18,"col":4},"end_pos":{"line":18,"col":5}}},"number":240,"ctx":["While desugaring module NegativeTests.Neg"]} +{"msg":["NegativeTests.Neg.y\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":22,"col":4},"end_pos":{"line":22,"col":5}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":22,"col":4},"end_pos":{"line":22,"col":5}}},"number":240,"ctx":["While desugaring module NegativeTests.Neg"]} +{"msg":["NegativeTests.Neg.test_precondition_label\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":36,"col":4},"end_pos":{"line":36,"col":27}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":36,"col":4},"end_pos":{"line":36,"col":27}}},"number":240,"ctx":["While desugaring module NegativeTests.Neg"]} +{"msg":["NegativeTests.Neg.test_postcondition_label\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":40,"col":4},"end_pos":{"line":40,"col":28}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":40,"col":4},"end_pos":{"line":40,"col":28}}},"number":240,"ctx":["While desugaring module NegativeTests.Neg"]} +{"msg":["NegativeTests.Neg.bad_projector\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":44,"col":4},"end_pos":{"line":44,"col":17}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":44,"col":4},"end_pos":{"line":44,"col":17}}},"number":240,"ctx":["While desugaring module NegativeTests.Neg"]} +{"msg":["Missing definitions in module NegativeTests.Neg:\n bad_projector\n test_postcondition_label\n test_precondition_label\n x\n y"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":63,"col":0},"end_pos":{"line":63,"col":32}}},"number":240,"ctx":[]} +Verified module: NegativeTests.Neg +All verification conditions discharged successfully diff --git a/tests/error-messages/NegativeTests.Positivity.fst.json_expected b/tests/error-messages/NegativeTests.Positivity.fst.json_expected new file mode 100644 index 00000000000..1672d7ba66c --- /dev/null +++ b/tests/error-messages/NegativeTests.Positivity.fst.json_expected @@ -0,0 +1,20 @@ +>> Got issues: [ +{"msg":["Inductive type NegativeTests.Positivity.t1 does not satisfy the strict positivity condition"],"level":"Error","range":{"def":{"file_name":"NegativeTests.Positivity.fst","start_pos":{"line":22,"col":10},"end_pos":{"line":22,"col":12}},"use":{"file_name":"NegativeTests.Positivity.fst","start_pos":{"line":22,"col":10},"end_pos":{"line":22,"col":12}}},"number":3,"ctx":["While typechecking the top-level declaration `type NegativeTests.Positivity.t1`","While typechecking the top-level declaration `[@@expect_failure] type NegativeTests.Positivity.t1`"]} +>>] +>> Got issues: [ +{"msg":["Inductive type NegativeTests.Positivity.t5 does not satisfy the strict positivity condition"],"level":"Error","range":{"def":{"file_name":"NegativeTests.Positivity.fst","start_pos":{"line":37,"col":10},"end_pos":{"line":37,"col":12}},"use":{"file_name":"NegativeTests.Positivity.fst","start_pos":{"line":37,"col":10},"end_pos":{"line":37,"col":12}}},"number":3,"ctx":["While typechecking the top-level declaration `type NegativeTests.Positivity.t5`","While typechecking the top-level declaration `[@@expect_failure] type NegativeTests.Positivity.t5`"]} +>>] +>> Got issues: [ +{"msg":["Type NegativeTests.Positivity.t7 is not strictly positive since it instantiates a non-uniformly recursive parameter or index NegativeTests.Positivity.t7 of NegativeTests.Positivity.t6"],"level":"Error","range":{"def":{"file_name":"NegativeTests.Positivity.fst","start_pos":{"line":49,"col":12},"end_pos":{"line":49,"col":14}},"use":{"file_name":"NegativeTests.Positivity.fst","start_pos":{"line":49,"col":4},"end_pos":{"line":49,"col":7}}},"number":3,"ctx":["While typechecking the top-level declaration `type NegativeTests.Positivity.t7`","While typechecking the top-level declaration `[@@expect_failure] type NegativeTests.Positivity.t7`"]} +>>] +>> Got issues: [ +{"msg":["Type NegativeTests.Positivity.t8 is not strictly positive since it instantiates a non-uniformly recursive parameter or index NegativeTests.Positivity.t8 of NegativeTests.Positivity.t6"],"level":"Error","range":{"def":{"file_name":"NegativeTests.Positivity.fst","start_pos":{"line":54,"col":16},"end_pos":{"line":54,"col":18}},"use":{"file_name":"NegativeTests.Positivity.fst","start_pos":{"line":54,"col":4},"end_pos":{"line":54,"col":7}}},"number":3,"ctx":["While typechecking the top-level declaration `type NegativeTests.Positivity.t8`","While typechecking the top-level declaration `[@@expect_failure] type NegativeTests.Positivity.t8`"]} +>>] +>> Got issues: [ +{"msg":["Inductive type NegativeTests.Positivity.t10 does not satisfy the strict positivity condition"],"level":"Error","range":{"def":{"file_name":"NegativeTests.Positivity.fst","start_pos":{"line":61,"col":10},"end_pos":{"line":61,"col":13}},"use":{"file_name":"NegativeTests.Positivity.fst","start_pos":{"line":61,"col":10},"end_pos":{"line":61,"col":13}}},"number":3,"ctx":["While typechecking the top-level declaration `type NegativeTests.Positivity.t10`","While typechecking the top-level declaration `[@@expect_failure] type NegativeTests.Positivity.t10`"]} +>>] +>> Got issues: [ +{"msg":["Inductive type NegativeTests.Positivity.t11 does not satisfy the strict positivity condition"],"level":"Error","range":{"def":{"file_name":"NegativeTests.Positivity.fst","start_pos":{"line":66,"col":10},"end_pos":{"line":66,"col":13}},"use":{"file_name":"NegativeTests.Positivity.fst","start_pos":{"line":66,"col":10},"end_pos":{"line":66,"col":13}}},"number":3,"ctx":["While typechecking the top-level declaration `type NegativeTests.Positivity.t11`","While typechecking the top-level declaration `[@@expect_failure] type NegativeTests.Positivity.t11`"]} +>>] +Verified module: NegativeTests.Positivity +All verification conditions discharged successfully diff --git a/tests/error-messages/NegativeTests.Set.fst.json_expected b/tests/error-messages/NegativeTests.Set.fst.json_expected new file mode 100644 index 00000000000..59580de7b6e --- /dev/null +++ b/tests/error-messages/NegativeTests.Set.fst.json_expected @@ -0,0 +1,15 @@ +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"NegativeTests.Set.fst","start_pos":{"line":28,"col":9},"end_pos":{"line":28,"col":30}},"use":{"file_name":"NegativeTests.Set.fst","start_pos":{"line":28,"col":9},"end_pos":{"line":28,"col":30}}},"number":19,"ctx":["While typechecking the top-level declaration `let should_fail1`","While typechecking the top-level declaration `[@@expect_failure] let should_fail1`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"NegativeTests.Set.fst","start_pos":{"line":33,"col":9},"end_pos":{"line":33,"col":67}},"use":{"file_name":"NegativeTests.Set.fst","start_pos":{"line":33,"col":9},"end_pos":{"line":33,"col":67}}},"number":19,"ctx":["While typechecking the top-level declaration `let should_fail2`","While typechecking the top-level declaration `[@@expect_failure] let should_fail2`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"NegativeTests.Set.fst","start_pos":{"line":38,"col":9},"end_pos":{"line":38,"col":52}},"use":{"file_name":"NegativeTests.Set.fst","start_pos":{"line":38,"col":9},"end_pos":{"line":38,"col":52}}},"number":19,"ctx":["While typechecking the top-level declaration `let should_fail3`","While typechecking the top-level declaration `[@@expect_failure] let should_fail3`"]} +>>] +{"msg":["NegativeTests.Set.should_fail1\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"NegativeTests.Set.fst","start_pos":{"line":25,"col":4},"end_pos":{"line":25,"col":16}},"use":{"file_name":"NegativeTests.Set.fst","start_pos":{"line":25,"col":4},"end_pos":{"line":25,"col":16}}},"number":240,"ctx":["While desugaring module NegativeTests.Set"]} +{"msg":["NegativeTests.Set.should_fail2\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"NegativeTests.Set.fst","start_pos":{"line":30,"col":4},"end_pos":{"line":30,"col":16}},"use":{"file_name":"NegativeTests.Set.fst","start_pos":{"line":30,"col":4},"end_pos":{"line":30,"col":16}}},"number":240,"ctx":["While desugaring module NegativeTests.Set"]} +{"msg":["NegativeTests.Set.should_fail3\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"NegativeTests.Set.fst","start_pos":{"line":35,"col":4},"end_pos":{"line":35,"col":16}},"use":{"file_name":"NegativeTests.Set.fst","start_pos":{"line":35,"col":4},"end_pos":{"line":35,"col":16}}},"number":240,"ctx":["While desugaring module NegativeTests.Set"]} +{"msg":["Missing definitions in module NegativeTests.Set:\n should_fail1\n should_fail2\n should_fail3"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"NegativeTests.Set.fst","start_pos":{"line":37,"col":0},"end_pos":{"line":38,"col":52}}},"number":240,"ctx":[]} +Verified module: NegativeTests.Set +All verification conditions discharged successfully diff --git a/tests/error-messages/NegativeTests.ShortCircuiting.fst.json_expected b/tests/error-messages/NegativeTests.ShortCircuiting.fst.json_expected new file mode 100644 index 00000000000..276cbe6aed4 --- /dev/null +++ b/tests/error-messages/NegativeTests.ShortCircuiting.fst.json_expected @@ -0,0 +1,11 @@ +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type b: Prims.bool{bad_p b}\ngot type Prims.bool","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"NegativeTests.ShortCircuiting.fst","start_pos":{"line":19,"col":31},"end_pos":{"line":19,"col":38}},"use":{"file_name":"NegativeTests.ShortCircuiting.fst","start_pos":{"line":21,"col":16},"end_pos":{"line":21,"col":33}}},"number":19,"ctx":["While typechecking the top-level declaration `let rec bad`","While typechecking the top-level declaration `[@@expect_failure] let rec bad`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":451,"col":90},"end_pos":{"line":451,"col":102}},"use":{"file_name":"NegativeTests.ShortCircuiting.fst","start_pos":{"line":25,"col":11},"end_pos":{"line":25,"col":36}}},"number":19,"ctx":["While typechecking the top-level declaration `let ff`","While typechecking the top-level declaration `[@@expect_failure] let ff`"]} +>>] +{"msg":["NegativeTests.ShortCircuiting.bad\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"NegativeTests.ShortCircuiting.fst","start_pos":{"line":19,"col":4},"end_pos":{"line":19,"col":7}},"use":{"file_name":"NegativeTests.ShortCircuiting.fst","start_pos":{"line":19,"col":4},"end_pos":{"line":19,"col":7}}},"number":240,"ctx":["While desugaring module NegativeTests.ShortCircuiting"]} +{"msg":["NegativeTests.ShortCircuiting.ff\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"NegativeTests.ShortCircuiting.fst","start_pos":{"line":23,"col":4},"end_pos":{"line":23,"col":6}},"use":{"file_name":"NegativeTests.ShortCircuiting.fst","start_pos":{"line":23,"col":4},"end_pos":{"line":23,"col":6}}},"number":240,"ctx":["While desugaring module NegativeTests.ShortCircuiting"]} +{"msg":["Missing definitions in module NegativeTests.ShortCircuiting:\n bad\n ff"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"NegativeTests.ShortCircuiting.fst","start_pos":{"line":25,"col":0},"end_pos":{"line":25,"col":36}}},"number":240,"ctx":[]} +Verified module: NegativeTests.ShortCircuiting +All verification conditions discharged successfully diff --git a/tests/error-messages/NegativeTests.Termination.fst.json_expected b/tests/error-messages/NegativeTests.Termination.fst.json_expected new file mode 100644 index 00000000000..1f3fce16960 --- /dev/null +++ b/tests/error-messages/NegativeTests.Termination.fst.json_expected @@ -0,0 +1,43 @@ +>> Got issues: [ +{"msg":["Could not prove termination of this recursive call","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":18,"col":12},"end_pos":{"line":21,"col":29}},"use":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":21,"col":28},"end_pos":{"line":21,"col":29}}},"number":19,"ctx":["While typechecking the top-level declaration `let rec bug15`","While typechecking the top-level declaration `[@@expect_failure] let rec bug15`"]} +>>] +>> Got issues: [ +{"msg":["Could not prove termination of this recursive call","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":25,"col":23},"end_pos":{"line":28,"col":35}},"use":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":28,"col":26},"end_pos":{"line":28,"col":35}}},"number":19,"ctx":["While typechecking the top-level declaration `let rec repeat_diverge`","While typechecking the top-level declaration `[@@expect_failure] let rec repeat_diverge`"]} +>>] +>> Got issues: [ +{"msg":["Could not prove termination of this recursive call","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":31,"col":19},"end_pos":{"line":36,"col":54}},"use":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":35,"col":43},"end_pos":{"line":35,"col":44}}},"number":19,"ctx":["While typechecking the top-level declaration `let rec ackermann_bad`","While typechecking the top-level declaration `[@@expect_failure] let rec ackermann_bad`"]} +>>] +>> Got issues: [ +{"msg":["Could not prove termination of this recursive call","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":40,"col":23},"end_pos":{"line":42,"col":29}},"use":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":42,"col":28},"end_pos":{"line":42,"col":29}}},"number":19,"ctx":["While typechecking the top-level declaration `let rec length_bad`","While typechecking the top-level declaration `[@@expect_failure] let rec length_bad`"]} +>>] +>> Got issues: [ +{"msg":["Could not prove termination of this recursive call","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":53,"col":2},"end_pos":{"line":55,"col":29}},"use":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":55,"col":15},"end_pos":{"line":55,"col":29}}},"number":19,"ctx":["While typechecking the top-level declaration `let rec strangeZeroBad`","While typechecking the top-level declaration `[@@expect_failure] let rec strangeZeroBad`"]} +>>] +>> Got issues: [ +{"msg":["Could not prove termination of this recursive call","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":64,"col":2},"end_pos":{"line":67,"col":29}},"use":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":67,"col":19},"end_pos":{"line":67,"col":29}}},"number":19,"ctx":["While typechecking the top-level declaration `let rec t1`","While typechecking the top-level declaration `[@@expect_failure] let rec t1`"]} +>>] +>> Got issues: [ +{"msg":["Could not prove termination of this recursive call","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":71,"col":13},"end_pos":{"line":75,"col":35}},"use":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":75,"col":34},"end_pos":{"line":75,"col":35}}},"number":19,"ctx":["While typechecking the top-level declaration `let rec plus`","While typechecking the top-level declaration `[@@expect_failure] let rec plus`"]} +>>] +>> Got issues: [ +{"msg":["Patterns are incomplete","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":80,"col":2},"end_pos":{"line":82,"col":14}}},"number":19,"ctx":["While typechecking the top-level declaration `let plus'`","While typechecking the top-level declaration `[@@expect_failure] let plus'`"]} +>>] +>> Got issues: [ +{"msg":["Could not prove termination of this recursive call","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":86,"col":15},"end_pos":{"line":89,"col":31}},"use":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":89,"col":29},"end_pos":{"line":89,"col":31}}},"number":19,"ctx":["While typechecking the top-level declaration `let rec minus`","While typechecking the top-level declaration `[@@expect_failure] let rec minus`"]} +>>] +>> Got issues: [ +{"msg":["Could not prove termination of this recursive call","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":94,"col":2},"end_pos":{"line":96,"col":26}},"use":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":96,"col":20},"end_pos":{"line":96,"col":26}}},"number":19,"ctx":["While typechecking the top-level declaration `let rec xxx`","While typechecking the top-level declaration `[@@expect_failure] let rec xxx`"]} +>>] +{"msg":["NegativeTests.Termination.bug15\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":18,"col":4},"end_pos":{"line":18,"col":9}},"use":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":18,"col":4},"end_pos":{"line":18,"col":9}}},"number":240,"ctx":["While desugaring module NegativeTests.Termination"]} +{"msg":["NegativeTests.Termination.repeat_diverge\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":23,"col":4},"end_pos":{"line":23,"col":18}},"use":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":23,"col":4},"end_pos":{"line":23,"col":18}}},"number":240,"ctx":["While desugaring module NegativeTests.Termination"]} +{"msg":["NegativeTests.Termination.ackermann_bad\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":31,"col":4},"end_pos":{"line":31,"col":17}},"use":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":31,"col":4},"end_pos":{"line":31,"col":17}}},"number":240,"ctx":["While desugaring module NegativeTests.Termination"]} +{"msg":["NegativeTests.Termination.length_bad\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":38,"col":4},"end_pos":{"line":38,"col":14}},"use":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":38,"col":4},"end_pos":{"line":38,"col":14}}},"number":240,"ctx":["While desugaring module NegativeTests.Termination"]} +{"msg":["NegativeTests.Termination.strangeZeroBad\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":50,"col":4},"end_pos":{"line":50,"col":18}},"use":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":50,"col":4},"end_pos":{"line":50,"col":18}}},"number":240,"ctx":["While desugaring module NegativeTests.Termination"]} +{"msg":["NegativeTests.Termination.t1\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":61,"col":4},"end_pos":{"line":61,"col":6}},"use":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":61,"col":4},"end_pos":{"line":61,"col":6}}},"number":240,"ctx":["While desugaring module NegativeTests.Termination"]} +{"msg":["NegativeTests.Termination.plus\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":69,"col":4},"end_pos":{"line":69,"col":8}},"use":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":69,"col":4},"end_pos":{"line":69,"col":8}}},"number":240,"ctx":["While desugaring module NegativeTests.Termination"]} +{"msg":["NegativeTests.Termination.plus'\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":77,"col":4},"end_pos":{"line":77,"col":9}},"use":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":77,"col":4},"end_pos":{"line":77,"col":9}}},"number":240,"ctx":["While desugaring module NegativeTests.Termination"]} +{"msg":["NegativeTests.Termination.minus\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":84,"col":4},"end_pos":{"line":84,"col":9}},"use":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":84,"col":4},"end_pos":{"line":84,"col":9}}},"number":240,"ctx":["While desugaring module NegativeTests.Termination"]} +{"msg":["NegativeTests.Termination.xxx\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":91,"col":4},"end_pos":{"line":91,"col":7}},"use":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":91,"col":4},"end_pos":{"line":91,"col":7}}},"number":240,"ctx":["While desugaring module NegativeTests.Termination"]} +{"msg":["Missing definitions in module NegativeTests.Termination:\n ackermann_bad\n bug15\n length_bad\n minus\n plus\n plus'\n repeat_diverge\n strangeZeroBad\n t1\n xxx"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"NegativeTests.Termination.fst","start_pos":{"line":93,"col":0},"end_pos":{"line":96,"col":26}}},"number":240,"ctx":[]} +Verified module: NegativeTests.Termination +All verification conditions discharged successfully diff --git a/tests/error-messages/NegativeTests.ZZImplicitFalse.fst.json_expected b/tests/error-messages/NegativeTests.ZZImplicitFalse.fst.json_expected new file mode 100644 index 00000000000..c2287841254 --- /dev/null +++ b/tests/error-messages/NegativeTests.ZZImplicitFalse.fst.json_expected @@ -0,0 +1,7 @@ +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type Prims.l_False\ngot type Prims.unit","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":159,"col":29},"end_pos":{"line":159,"col":34}},"use":{"file_name":"NegativeTests.ZZImplicitFalse.fst","start_pos":{"line":20,"col":27},"end_pos":{"line":20,"col":28}}},"number":19,"ctx":["While typechecking the top-level declaration `let test`","While typechecking the top-level declaration `[@@expect_failure] let test`"]} +>>] +{"msg":["NegativeTests.ZZImplicitFalse.test\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"NegativeTests.ZZImplicitFalse.fst","start_pos":{"line":18,"col":4},"end_pos":{"line":18,"col":8}},"use":{"file_name":"NegativeTests.ZZImplicitFalse.fst","start_pos":{"line":18,"col":4},"end_pos":{"line":18,"col":8}}},"number":240,"ctx":["While desugaring module NegativeTests.ZZImplicitFalse"]} +{"msg":["Missing definitions in module NegativeTests.ZZImplicitFalse: test"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"NegativeTests.ZZImplicitFalse.fst","start_pos":{"line":20,"col":0},"end_pos":{"line":20,"col":34}}},"number":240,"ctx":[]} +Verified module: NegativeTests.ZZImplicitFalse +All verification conditions discharged successfully diff --git a/tests/error-messages/OccursCheckOnArrows.fst.json_expected b/tests/error-messages/OccursCheckOnArrows.fst.json_expected new file mode 100644 index 00000000000..9b99c70d220 --- /dev/null +++ b/tests/error-messages/OccursCheckOnArrows.fst.json_expected @@ -0,0 +1,5 @@ +>> Got issues: [ +{"msg":["_: (*?u5*) _ -> (*?u4*) _ is not a subtype of the expected type (*?u5*) _"],"level":"Error","range":{"def":{"file_name":"OccursCheckOnArrows.fst","start_pos":{"line":18,"col":9},"end_pos":{"line":18,"col":10}},"use":{"file_name":"OccursCheckOnArrows.fst","start_pos":{"line":18,"col":15},"end_pos":{"line":18,"col":16}}},"number":54,"ctx":["While solving deferred constraints","solve_non_tactic_deferred_constraints","While typechecking the top-level declaration `let oops`","While typechecking the top-level declaration `[@@expect_failure] let oops`"]} +>>] +Verified module: OccursCheckOnArrows +All verification conditions discharged successfully diff --git a/tests/error-messages/OptionStack.fst.json_expected b/tests/error-messages/OptionStack.fst.json_expected new file mode 100644 index 00000000000..268463b8b3a --- /dev/null +++ b/tests/error-messages/OptionStack.fst.json_expected @@ -0,0 +1,14 @@ +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"OptionStack.fst","start_pos":{"line":21,"col":16},"end_pos":{"line":21,"col":21}},"use":{"file_name":"OptionStack.fst","start_pos":{"line":21,"col":9},"end_pos":{"line":21,"col":15}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let t0`","While typechecking the top-level declaration `[@@expect_failure] let t0`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"OptionStack.fst","start_pos":{"line":24,"col":16},"end_pos":{"line":24,"col":21}},"use":{"file_name":"OptionStack.fst","start_pos":{"line":24,"col":9},"end_pos":{"line":24,"col":15}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let t1`","While typechecking the top-level declaration `[@@expect_failure] let t1`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"OptionStack.fst","start_pos":{"line":27,"col":16},"end_pos":{"line":27,"col":21}},"use":{"file_name":"OptionStack.fst","start_pos":{"line":27,"col":9},"end_pos":{"line":27,"col":15}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let t2`","While typechecking the top-level declaration `[@@expect_failure] let t2`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"OptionStack.fst","start_pos":{"line":39,"col":16},"end_pos":{"line":39,"col":21}},"use":{"file_name":"OptionStack.fst","start_pos":{"line":39,"col":9},"end_pos":{"line":39,"col":15}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let t7`","While typechecking the top-level declaration `[@@expect_failure] let t7`"]} +>>] +Verified module: OptionStack +All verification conditions discharged successfully diff --git a/tests/error-messages/PatAnnot.fst.json_expected b/tests/error-messages/PatAnnot.fst.json_expected new file mode 100644 index 00000000000..81144835ab0 --- /dev/null +++ b/tests/error-messages/PatAnnot.fst.json_expected @@ -0,0 +1,20 @@ +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type Prims.squash Prims.l_False\ngot type Prims.unit","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"PatAnnot.fst","start_pos":{"line":25,"col":19},"end_pos":{"line":25,"col":24}},"use":{"file_name":"PatAnnot.fst","start_pos":{"line":25,"col":8},"end_pos":{"line":25,"col":9}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let whoops`","While typechecking the top-level declaration `[@@expect_failure] let whoops`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details.","Also see: Prims.fst(459,77-459,89)",""],"level":"Error","range":{"def":{"file_name":"PatAnnot.fst","start_pos":{"line":28,"col":0},"end_pos":{"line":30,"col":14}},"use":{"file_name":"PatAnnot.fst","start_pos":{"line":28,"col":0},"end_pos":{"line":30,"col":14}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let whoops2`","While typechecking the top-level declaration `[@@expect_failure] let whoops2`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details.","Also see: Prims.fst(459,77-459,89)",""],"level":"Error","range":{"def":{"file_name":"PatAnnot.fst","start_pos":{"line":33,"col":0},"end_pos":{"line":35,"col":14}},"use":{"file_name":"PatAnnot.fst","start_pos":{"line":33,"col":0},"end_pos":{"line":35,"col":14}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let sub_bv`","While typechecking the top-level declaration `[@@expect_failure] let sub_bv`"]} +>>] +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type Prims.squash Prims.l_False\ngot type Prims.unit","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"PatAnnot.fst","start_pos":{"line":40,"col":26},"end_pos":{"line":40,"col":31}},"use":{"file_name":"PatAnnot.fst","start_pos":{"line":39,"col":10},"end_pos":{"line":39,"col":12}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let s`","While typechecking the top-level declaration `[@@expect_failure] let s`"]} +>>] +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":680,"col":18},"end_pos":{"line":680,"col":24}},"use":{"file_name":"PatAnnot.fst","start_pos":{"line":46,"col":10},"end_pos":{"line":46,"col":11}}},"number":19,"ctx":["While typechecking the top-level declaration `let test1`","While typechecking the top-level declaration `[@@expect_failure] let test1`"]} +>>] +>> Got issues: [ +{"msg":["Type annotation on parameter incompatible with the expected type","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":680,"col":18},"end_pos":{"line":680,"col":24}},"use":{"file_name":"PatAnnot.fst","start_pos":{"line":55,"col":36},"end_pos":{"line":55,"col":39}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let test3`","While typechecking the top-level declaration `[@@expect_failure] let test3`"]} +>>] +Verified module: PatAnnot +All verification conditions discharged successfully diff --git a/tests/error-messages/PatCoerce.fst.json_expected b/tests/error-messages/PatCoerce.fst.json_expected new file mode 100644 index 00000000000..1fcd79b55ff --- /dev/null +++ b/tests/error-messages/PatCoerce.fst.json_expected @@ -0,0 +1,7 @@ +>> Got issues: [ +{"msg":["Type of pattern (Prims.bool) does not match type of scrutinee (Type0)"],"level":"Error","range":{"def":{"file_name":"PatCoerce.fst","start_pos":{"line":25,"col":4},"end_pos":{"line":25,"col":8}},"use":{"file_name":"PatCoerce.fst","start_pos":{"line":25,"col":4},"end_pos":{"line":25,"col":8}}},"number":114,"ctx":["While typechecking the top-level declaration `let bla`","While typechecking the top-level declaration `[@@expect_failure] let bla`"]} +>>] +{"msg":["PatCoerce.bla\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"PatCoerce.fst","start_pos":{"line":20,"col":4},"end_pos":{"line":20,"col":7}},"use":{"file_name":"PatCoerce.fst","start_pos":{"line":20,"col":4},"end_pos":{"line":20,"col":7}}},"number":240,"ctx":["While desugaring module PatCoerce"]} +{"msg":["Missing definitions in module PatCoerce: bla"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"PatCoerce.fst","start_pos":{"line":23,"col":0},"end_pos":{"line":26,"col":14}}},"number":240,"ctx":[]} +Verified module: PatCoerce +All verification conditions discharged successfully diff --git a/tests/error-messages/PatternMatch.fst.json_expected b/tests/error-messages/PatternMatch.fst.json_expected new file mode 100644 index 00000000000..f4e47fbfced --- /dev/null +++ b/tests/error-messages/PatternMatch.fst.json_expected @@ -0,0 +1,44 @@ +>> Got issues: [ +{"msg":["Type ascriptions within patterns are only allowed on variables"],"level":"Error","range":{"def":{"file_name":"PatternMatch.fst","start_pos":{"line":15,"col":27},"end_pos":{"line":15,"col":34}},"use":{"file_name":"PatternMatch.fst","start_pos":{"line":15,"col":27},"end_pos":{"line":15,"col":34}}},"number":178,"ctx":["While desugaring module PatternMatch"]} +>>] +>> Got issues: [ +{"msg":["Type ascriptions within patterns are only allowed on variables"],"level":"Error","range":{"def":{"file_name":"PatternMatch.fst","start_pos":{"line":18,"col":29},"end_pos":{"line":18,"col":48}},"use":{"file_name":"PatternMatch.fst","start_pos":{"line":18,"col":29},"end_pos":{"line":18,"col":48}}},"number":178,"ctx":["While desugaring module PatternMatch"]} +>>] +>> Got issues: [ +{"msg":["Type ascriptions within patterns are only allowed on variables"],"level":"Error","range":{"def":{"file_name":"PatternMatch.fst","start_pos":{"line":41,"col":3},"end_pos":{"line":41,"col":24}},"use":{"file_name":"PatternMatch.fst","start_pos":{"line":41,"col":3},"end_pos":{"line":41,"col":24}}},"number":178,"ctx":["While desugaring module PatternMatch"]} +>>] +>> Got issues: [ +{"msg":["Patterns are incomplete","The SMT solver could not prove the query. Use --query_stats for more details.","Also see: PatternMatch.fst(21,4-21,8)",""],"level":"Error","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___7`","While typechecking the top-level declaration `[@@expect_failure] let uu___6`"]} +>>] +>> Got issues: [ +{"msg":["Patterns are incomplete","The SMT solver could not prove the query. Use --query_stats for more details.","Also see: PatternMatch.fst(24,4-24,11)",""],"level":"Error","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___10`","While typechecking the top-level declaration `[@@expect_failure] let uu___9`"]} +>>] +>> Got issues: [ +{"msg":["Patterns are incomplete","The SMT solver could not prove the query. Use --query_stats for more details.","Also see: PatternMatch.fst(29,4-29,8)",""],"level":"Error","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___17`","While typechecking the top-level declaration `[@@expect_failure] let uu___16`"]} +>>] +>> Got issues: [ +{"msg":["Type of pattern (Prims.bool) does not match type of scrutinee (Prims.int)"],"level":"Error","range":{"def":{"file_name":"PatternMatch.fst","start_pos":{"line":32,"col":4},"end_pos":{"line":32,"col":9}},"use":{"file_name":"PatternMatch.fst","start_pos":{"line":32,"col":4},"end_pos":{"line":32,"col":9}}},"number":114,"ctx":["While typechecking the top-level declaration `let uu___20`","While typechecking the top-level declaration `[@@expect_failure] let uu___19`"]} +>>] +>> Got issues: [ +{"msg":["Type of pattern PatternMatch.ab\ndoes not match type of scrutinee Prims.int","Head mismatch PatternMatch.ab vs Prims.int"],"level":"Error","range":{"def":{"file_name":"PatternMatch.fst","start_pos":{"line":35,"col":4},"end_pos":{"line":35,"col":5}},"use":{"file_name":"PatternMatch.fst","start_pos":{"line":35,"col":4},"end_pos":{"line":35,"col":5}}},"number":114,"ctx":["While typechecking the top-level declaration `let uu___23`","While typechecking the top-level declaration `[@@expect_failure] let uu___22`"]} +>>] +>> Got issues: [ +{"msg":["Patterns are incomplete","The SMT solver could not prove the query. Use --query_stats for more details.","Also see: PatternMatch.fst(38,4-38,5)",""],"level":"Error","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___26`","While typechecking the top-level declaration `[@@expect_failure] let uu___25`"]} +>>] +>> Got issues: [ +{"msg":["Type of pattern (Prims.bool) does not match type of scrutinee (Prims.int)"],"level":"Error","range":{"def":{"file_name":"PatternMatch.fst","start_pos":{"line":55,"col":4},"end_pos":{"line":55,"col":8}},"use":{"file_name":"PatternMatch.fst","start_pos":{"line":55,"col":4},"end_pos":{"line":55,"col":8}}},"number":114,"ctx":["While typechecking the top-level declaration `let uu___54`","While typechecking the top-level declaration `[@@expect_failure] let uu___53`"]} +>>] +>> Got issues: [ +{"msg":["Type of pattern (Prims.bool) does not match type of scrutinee (Prims.int)"],"level":"Error","range":{"def":{"file_name":"PatternMatch.fst","start_pos":{"line":58,"col":4},"end_pos":{"line":58,"col":16}},"use":{"file_name":"PatternMatch.fst","start_pos":{"line":58,"col":4},"end_pos":{"line":58,"col":16}}},"number":114,"ctx":["While typechecking the top-level declaration `let uu___57`","While typechecking the top-level declaration `[@@expect_failure] let uu___56`"]} +>>] +>> Got issues: [ +{"msg":["Patterns are incomplete","The SMT solver could not prove the query. Use --query_stats for more details.","Also see: PatternMatch.fst(61,5-61,12)",""],"level":"Error","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let x`","While typechecking the top-level declaration `[@@expect_failure] let uu___60`"]} +>>] +>> Got issues: [ +{"msg":["Patterns are incomplete","The SMT solver could not prove the query. Use --query_stats for more details.","Also see: PatternMatch.fst(64,5-64,20)",""],"level":"Error","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let x`","While typechecking the top-level declaration `[@@expect_failure] let uu___64`"]} +>>] +>> Got issues: [ +{"msg":["Type of pattern (Prims.bool) does not match type of scrutinee (Prims.int)"],"level":"Error","range":{"def":{"file_name":"PatternMatch.fst","start_pos":{"line":69,"col":5},"end_pos":{"line":69,"col":15}},"use":{"file_name":"PatternMatch.fst","start_pos":{"line":69,"col":5},"end_pos":{"line":69,"col":15}}},"number":114,"ctx":["While typechecking the top-level declaration `let uu___74`","While typechecking the top-level declaration `[@@expect_failure] let uu___73`"]} +>>] +Verified module: PatternMatch +All verification conditions discharged successfully diff --git a/tests/error-messages/QuickTest.fst.json_expected b/tests/error-messages/QuickTest.fst.json_expected new file mode 100644 index 00000000000..ef157695432 --- /dev/null +++ b/tests/error-messages/QuickTest.fst.json_expected @@ -0,0 +1,5 @@ +>> Got issues: [ +{"msg":["","The SMT solver could not prove the query. Use --query_stats for more details.","Also see: QuickTest(1,2-3,4)","Other related locations: QuickTest.fst(116,12-116,20)"],"level":"Error","range":{"def":{"file_name":"QuickTest.fst","start_pos":{"line":131,"col":2},"end_pos":{"line":134,"col":34}},"use":{"file_name":"QuickTest.fst","start_pos":{"line":131,"col":2},"end_pos":{"line":134,"col":34}}},"number":19,"ctx":["While typechecking the top-level declaration `let va_lemma_Test2`","While typechecking the top-level declaration `[@@expect_failure] let va_lemma_Test2`"]} +>>] +Verified module: QuickTest +All verification conditions discharged successfully diff --git a/tests/error-messages/QuickTestNBE.fst.json_expected b/tests/error-messages/QuickTestNBE.fst.json_expected new file mode 100644 index 00000000000..3571367a50b --- /dev/null +++ b/tests/error-messages/QuickTestNBE.fst.json_expected @@ -0,0 +1,5 @@ +>> Got issues: [ +{"msg":["","The SMT solver could not prove the query. Use --query_stats for more details.","Also see: QuickTestNBE(1,2-3,4)","Other related locations: QuickTestNBE.fst(116,16-116,18)"],"level":"Error","range":{"def":{"file_name":"QuickTestNBE.fst","start_pos":{"line":131,"col":2},"end_pos":{"line":134,"col":34}},"use":{"file_name":"QuickTestNBE.fst","start_pos":{"line":131,"col":2},"end_pos":{"line":134,"col":34}}},"number":19,"ctx":["While typechecking the top-level declaration `let va_lemma_Test2`","While typechecking the top-level declaration `[@@expect_failure] let va_lemma_Test2`"]} +>>] +Verified module: QuickTestNBE +All verification conditions discharged successfully diff --git a/tests/error-messages/RecordFields.fst.json_expected b/tests/error-messages/RecordFields.fst.json_expected new file mode 100644 index 00000000000..10b41ba28ce --- /dev/null +++ b/tests/error-messages/RecordFields.fst.json_expected @@ -0,0 +1,11 @@ +>> Got issues: [ +{"msg":["Field 'd' is redundant for type RecordFields.r",""],"level":"Error","range":{"def":{"file_name":"RecordFields.fst","start_pos":{"line":8,"col":29},"end_pos":{"line":8,"col":30}},"use":{"file_name":"RecordFields.fst","start_pos":{"line":8,"col":29},"end_pos":{"line":8,"col":30}}},"number":118,"ctx":["While typechecking the top-level declaration `let t2`","While typechecking the top-level declaration `[@@expect_failure] let t2`"]} +>>] +>> Got issues: [ +{"msg":["Missing fields for record type 'RecordFields.r': 'c'"],"level":"Error","range":{"def":{"file_name":"RecordFields.fst","start_pos":{"line":11,"col":14},"end_pos":{"line":11,"col":22}},"use":{"file_name":"RecordFields.fst","start_pos":{"line":11,"col":14},"end_pos":{"line":11,"col":22}}},"number":118,"ctx":["While typechecking the top-level declaration `let t3`","While typechecking the top-level declaration `[@@expect_failure] let t3`"]} +>>] +>> Got issues: [ +{"msg":["Field 'd' is redundant for type RecordFields.r","Missing fields: 'c'"],"level":"Error","range":{"def":{"file_name":"RecordFields.fst","start_pos":{"line":14,"col":24},"end_pos":{"line":14,"col":25}},"use":{"file_name":"RecordFields.fst","start_pos":{"line":14,"col":24},"end_pos":{"line":14,"col":25}}},"number":118,"ctx":["While typechecking the top-level declaration `let t4`","While typechecking the top-level declaration `[@@expect_failure] let t4`"]} +>>] +Verified module: RecordFields +All verification conditions discharged successfully diff --git a/tests/error-messages/ResolveImplicitsErrorPos.fst.json_expected b/tests/error-messages/ResolveImplicitsErrorPos.fst.json_expected new file mode 100644 index 00000000000..8e20e660adb --- /dev/null +++ b/tests/error-messages/ResolveImplicitsErrorPos.fst.json_expected @@ -0,0 +1,10 @@ +proof-state: State dump @ depth 0 (at the time of failure): +Location: ResolveImplicitsErrorPos.fst(14,13-16,7) +Goal 1/1 (Instantiating meta argument): +(_: Prims.unit) |- _ : Prims.int + +>> Got issues: [ +{"msg":["Tactic failed","oops"],"level":"Error","range":{"def":{"file_name":"ResolveImplicitsErrorPos.fst","start_pos":{"line":15,"col":10},"end_pos":{"line":15,"col":11}},"use":{"file_name":"ResolveImplicitsErrorPos.fst","start_pos":{"line":15,"col":10},"end_pos":{"line":15,"col":11}}},"number":228,"ctx":["While solving implicits with a tactic","While solving deferred constraints","While typechecking the top-level declaration `let test`","While typechecking the top-level declaration `[@@expect_failure] let test`"]} +>>] +Verified module: ResolveImplicitsErrorPos +All verification conditions discharged successfully diff --git a/tests/error-messages/SMTPatSymbols.fst.json_expected b/tests/error-messages/SMTPatSymbols.fst.json_expected new file mode 100644 index 00000000000..257fd50b486 --- /dev/null +++ b/tests/error-messages/SMTPatSymbols.fst.json_expected @@ -0,0 +1,3 @@ +{"msg":["Pattern uses these theory symbols or terms that should not be in an SMT pattern:\n Prims.op_Addition, Prims.op_Subtraction"],"level":"Warning","range":{"def":{"file_name":"SMTPatSymbols.fst","start_pos":{"line":3,"col":34},"end_pos":{"line":3,"col":52}},"use":{"file_name":"SMTPatSymbols.fst","start_pos":{"line":3,"col":34},"end_pos":{"line":3,"col":52}}},"number":271,"ctx":["While typechecking the top-level declaration `val SMTPatSymbols.lem`"]} +Verified module: SMTPatSymbols +All verification conditions discharged successfully diff --git a/tests/error-messages/SeqLit.fst.json_expected b/tests/error-messages/SeqLit.fst.json_expected new file mode 100644 index 00000000000..62ff1d1e16d --- /dev/null +++ b/tests/error-messages/SeqLit.fst.json_expected @@ -0,0 +1,78 @@ +Module after desugaring: +module SeqLit +Declarations: [ +let x = seq![1; 2; 3] +let y = [1; 2; 3] +private +let _ = assert (FStar.Seq.Base.seq_to_list SeqLit.x == SeqLit.y) +private +let _ = [1; 2] @ [3] +private +let _ = [1; 2; 3] +private +let _ = [1; 2; 3] +private +let _ = [1; 2; 3] +private +let _ = FStar.Seq.Base.append seq![1; 2] seq![3] +private +let _ = seq![1; 2; 3] +private +let _ = seq![1; 2; 3] +private +let _ = seq![1; 2; 3] +] + +Module before type checking: +module SeqLit +Declarations: [ +let x = seq![1; 2; 3] +let y = [1; 2; 3] +private +let _ = assert (FStar.Seq.Base.seq_to_list SeqLit.x == SeqLit.y) +private +let _ = [1; 2] @ [3] +private +let _ = [1; 2; 3] +private +let _ = [1; 2; 3] +private +let _ = [1; 2; 3] +private +let _ = FStar.Seq.Base.append seq![1; 2] seq![3] +private +let _ = seq![1; 2; 3] +private +let _ = seq![1; 2; 3] +private +let _ = seq![1; 2; 3] +] + +Module after type checking: +module SeqLit +Declarations: [ +let x = seq![1; 2; 3] +let y = [1; 2; 3] +private +let _ = assert (FStar.Seq.Base.seq_to_list SeqLit.x == SeqLit.y) +private +let _ = [1; 2] @ [3] +private +let _ = [1; 2; 3] +private +let _ = [1; 2; 3] +private +let _ = [1; 2; 3] +private +let _ = FStar.Seq.Base.append seq![1; 2] seq![3] +private +let _ = seq![1; 2; 3] +private +let _ = seq![1; 2; 3] +private +let _ = seq![1; 2; 3] +] + +{"msg":["The operator '@' has been resolved to FStar.List.Tot.append even though\nFStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop\nrelying on this deprecated, special treatment of '@'."],"level":"Warning","range":{"def":{"file_name":"SeqLit.fst","start_pos":{"line":8,"col":17},"end_pos":{"line":8,"col":18}},"use":{"file_name":"SeqLit.fst","start_pos":{"line":8,"col":17},"end_pos":{"line":8,"col":18}}},"number":337,"ctx":["While desugaring module SeqLit"]} +Verified module: SeqLit +All verification conditions discharged successfully diff --git a/tests/error-messages/StableErr.fst.json_expected b/tests/error-messages/StableErr.fst.json_expected new file mode 100644 index 00000000000..b3a9827d236 --- /dev/null +++ b/tests/error-messages/StableErr.fst.json_expected @@ -0,0 +1,5 @@ +>> Got issues: [ +{"msg":["A query could not be solved internally, and --no_smt was given.","Query =\nPrims.l_False"],"level":"Error","range":{"def":{"file_name":"StableErr.fst","start_pos":{"line":26,"col":0},"end_pos":{"line":26,"col":20}},"use":{"file_name":"StableErr.fst","start_pos":{"line":26,"col":0},"end_pos":{"line":26,"col":20}}},"number":298,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]} +>>] +Verified module: StableErr +All verification conditions discharged successfully diff --git a/tests/error-messages/StrictUnfolding.fst.json_expected b/tests/error-messages/StrictUnfolding.fst.json_expected new file mode 100644 index 00000000000..dfaeeb98326 --- /dev/null +++ b/tests/error-messages/StrictUnfolding.fst.json_expected @@ -0,0 +1,25 @@ +proof-state: State dump @ depth 1 (A): +Location: StrictUnfolding.fst(28,8-28,16) +Goal 1/1: +(x: FStar.Pervasives.Native.option (x: FStar.Integers.int{x = 0}) {Some? x}) |- _ : Prims.squash (StrictUnfolding.project x == 0) + +proof-state: State dump @ depth 1 (B): +Location: StrictUnfolding.fst(30,8-30,16) +Goal 1/1: +(x: FStar.Pervasives.Native.option (x: FStar.Integers.int{x = 0}) {Some? x}) |- _ : Prims.squash (StrictUnfolding.project x == 0) + +proof-state: State dump @ depth 1 (A): +Location: StrictUnfolding.fst(35,8-35,16) +Goal 1/1: +(_: Prims.unit), (return_val: x: FStar.Pervasives.Native.option Prims.int {Some? x}), (_: return_val == FStar.Pervasives.Native.Some 0), (any_result: Prims.int), (_: StrictUnfolding.project (FStar.Pervasives.Native.Some 0) == any_result), (any_result'0: Prims.logical), (_: StrictUnfolding.project (FStar.Pervasives.Native.Some 0) == 0 == any_result'0) |- _ : Prims.squash (StrictUnfolding.project (FStar.Pervasives.Native.Some 0) == 0) + +proof-state: State dump @ depth 1 (B): +Location: StrictUnfolding.fst(37,8-37,16) +Goal 1/1: +(_: Prims.unit), (return_val: x: FStar.Pervasives.Native.option Prims.int {Some? x}), (_: return_val == FStar.Pervasives.Native.Some 0), (any_result: Prims.int), (_: StrictUnfolding.project (FStar.Pervasives.Native.Some 0) == any_result), (any_result'0: Prims.logical), (_: StrictUnfolding.project (FStar.Pervasives.Native.Some 0) == 0 == any_result'0) |- _ : Prims.squash (0 == 0) + +>> Got issues: [ +{"msg":["Could not prove goal #1\n","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"StrictUnfolding.fst","start_pos":{"line":50,"col":48},"end_pos":{"line":50,"col":72}},"use":{"file_name":"StrictUnfolding.fst","start_pos":{"line":50,"col":2},"end_pos":{"line":50,"col":8}}},"number":19,"ctx":["While typechecking the top-level declaration `let test_integer_generic_wo_fstar_integers`","While typechecking the top-level declaration `[@@expect_failure] let test_integer_generic_wo_fstar_integers`"]} +>>] +Verified module: StrictUnfolding +All verification conditions discharged successfully diff --git a/tests/error-messages/StringNormalization.fst.json_expected b/tests/error-messages/StringNormalization.fst.json_expected new file mode 100644 index 00000000000..5507d606414 --- /dev/null +++ b/tests/error-messages/StringNormalization.fst.json_expected @@ -0,0 +1,5 @@ +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"StringNormalization.fst","start_pos":{"line":83,"col":9},"end_pos":{"line":83,"col":58}},"use":{"file_name":"StringNormalization.fst","start_pos":{"line":83,"col":2},"end_pos":{"line":83,"col":8}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___34`","While typechecking the top-level declaration `[@@expect_failure] let uu___34`"]} +>>] +Verified module: StringNormalization +All verification conditions discharged successfully diff --git a/tests/error-messages/Test.FunctionalExtensionality.fst.json_expected b/tests/error-messages/Test.FunctionalExtensionality.fst.json_expected new file mode 100644 index 00000000000..8cf2987cd6c --- /dev/null +++ b/tests/error-messages/Test.FunctionalExtensionality.fst.json_expected @@ -0,0 +1,14 @@ +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type Prims.nat ^-> Prims.int\ngot type Prims.int ^-> Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"FStar.FunctionalExtensionality.fsti","start_pos":{"line":102,"col":60},"end_pos":{"line":102,"col":77}},"use":{"file_name":"Test.FunctionalExtensionality.fst","start_pos":{"line":36,"col":49},"end_pos":{"line":36,"col":50}}},"number":19,"ctx":["While typechecking the top-level declaration `let sub_fails`","While typechecking the top-level declaration `[@@expect_failure] let sub_fails`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Test.FunctionalExtensionality.fst","start_pos":{"line":80,"col":9},"end_pos":{"line":80,"col":43}},"use":{"file_name":"Test.FunctionalExtensionality.fst","start_pos":{"line":80,"col":2},"end_pos":{"line":80,"col":8}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let unable_to_extend_equality_to_larger_domains_1`","While typechecking the top-level declaration `[@@expect_failure] let unable_to_extend_equality_to_larger_domains_1`"]} +>>] +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type _: Prims.int -> Prims.int\ngot type Prims.nat ^-> Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":680,"col":18},"end_pos":{"line":680,"col":24}},"use":{"file_name":"Test.FunctionalExtensionality.fst","start_pos":{"line":92,"col":36},"end_pos":{"line":92,"col":47}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let unable_to_extend_equality_to_larger_domains_2`","While typechecking the top-level declaration `[@@expect_failure] let unable_to_extend_equality_to_larger_domains_2`"]} +>>] +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type Prims.int ^-> Prims.int\ngot type Prims.int ^-> Prims.nat","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"FStar.FunctionalExtensionality.fsti","start_pos":{"line":102,"col":60},"end_pos":{"line":102,"col":77}},"use":{"file_name":"Test.FunctionalExtensionality.fst","start_pos":{"line":142,"col":57},"end_pos":{"line":142,"col":58}}},"number":19,"ctx":["While typechecking the top-level declaration `let sub_currently_not`","While typechecking the top-level declaration `[@@expect_failure] let sub_currently_not`"]} +>>] +Verified module: Test.FunctionalExtensionality +All verification conditions discharged successfully diff --git a/tests/error-messages/TestErrorLocations.fst.json_expected b/tests/error-messages/TestErrorLocations.fst.json_expected new file mode 100644 index 00000000000..af547dee013 --- /dev/null +++ b/tests/error-messages/TestErrorLocations.fst.json_expected @@ -0,0 +1,51 @@ +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"TestErrorLocations.fst","start_pos":{"line":20,"col":21},"end_pos":{"line":20,"col":23}},"use":{"file_name":"TestErrorLocations.fst","start_pos":{"line":20,"col":21},"end_pos":{"line":20,"col":23}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let test0`","While typechecking the top-level declaration `[@@expect_failure] let test0`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"TestErrorLocations.fst","start_pos":{"line":24,"col":21},"end_pos":{"line":24,"col":23}},"use":{"file_name":"TestErrorLocations.fst","start_pos":{"line":24,"col":21},"end_pos":{"line":24,"col":23}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let test1`","While typechecking the top-level declaration `[@@expect_failure] let test1`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"TestErrorLocations.fst","start_pos":{"line":27,"col":50},"end_pos":{"line":27,"col":58}},"use":{"file_name":"TestErrorLocations.fst","start_pos":{"line":31,"col":10},"end_pos":{"line":31,"col":19}}},"number":19,"ctx":["While typechecking the top-level declaration `let test2`","While typechecking the top-level declaration `[@@expect_failure] let test2`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"TestErrorLocations.fst","start_pos":{"line":27,"col":50},"end_pos":{"line":27,"col":58}},"use":{"file_name":"TestErrorLocations.fst","start_pos":{"line":37,"col":10},"end_pos":{"line":37,"col":11}}},"number":19,"ctx":["While typechecking the top-level declaration `let test3`","While typechecking the top-level declaration `[@@expect_failure] let test3`"]} +>>] +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":680,"col":18},"end_pos":{"line":680,"col":24}},"use":{"file_name":"TestErrorLocations.fst","start_pos":{"line":43,"col":20},"end_pos":{"line":43,"col":21}}},"number":19,"ctx":["While typechecking the top-level declaration `let test4`","While typechecking the top-level declaration `[@@expect_failure] let test4`"]} +>>] +>> Got issues: [ +{"msg":["Could not prove post-condition","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"TestErrorLocations.fst","start_pos":{"line":46,"col":84},"end_pos":{"line":46,"col":90}},"use":{"file_name":"TestErrorLocations.fst","start_pos":{"line":48,"col":14},"end_pos":{"line":48,"col":19}}},"number":19,"ctx":["While typechecking the top-level declaration `let test5`","While typechecking the top-level declaration `[@@expect_failure] let test5`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":451,"col":90},"end_pos":{"line":451,"col":102}},"use":{"file_name":"TestErrorLocations.fst","start_pos":{"line":58,"col":15},"end_pos":{"line":58,"col":17}}},"number":19,"ctx":["While typechecking the top-level declaration `let test6`","While typechecking the top-level declaration `[@@expect_failure] let test6`"]} +>>] +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":451,"col":90},"end_pos":{"line":451,"col":102}},"use":{"file_name":"TestErrorLocations.fst","start_pos":{"line":62,"col":15},"end_pos":{"line":62,"col":17}}},"number":19,"ctx":["While typechecking the top-level declaration `let test7`","While typechecking the top-level declaration `[@@expect_failure] let test7`"]} +>>] +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":680,"col":18},"end_pos":{"line":680,"col":24}},"use":{"file_name":"TestErrorLocations.fst","start_pos":{"line":66,"col":27},"end_pos":{"line":66,"col":28}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let test8`","While typechecking the top-level declaration `[@@expect_failure] let test8`"]} +>>] +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type Type0\ngot type Type0","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"TestErrorLocations.fst","start_pos":{"line":68,"col":52},"end_pos":{"line":68,"col":66}},"use":{"file_name":"TestErrorLocations.fst","start_pos":{"line":70,"col":25},"end_pos":{"line":70,"col":34}}},"number":19,"ctx":["While typechecking the top-level declaration `val TestErrorLocations.test9`","While typechecking the top-level declaration `[@@expect_failure] val TestErrorLocations.test9`"]} +>>] +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type Prims.squash (exists (x: Prims.nat). x = 0)\ngot type Prims.unit","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"FStar.Classical.Sugar.fsti","start_pos":{"line":66,"col":22},"end_pos":{"line":66,"col":41}},"use":{"file_name":"TestErrorLocations.fst","start_pos":{"line":89,"col":20},"end_pos":{"line":89,"col":36}}},"number":19,"ctx":["While typechecking the top-level declaration `let test_elim_exists`","While typechecking the top-level declaration `[@@expect_failure] let test_elim_exists`"]} +>>] +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type Prims.squash (forall (x: Prims.nat). x = 0)\ngot type Prims.unit","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"TestErrorLocations.fst","start_pos":{"line":97,"col":28},"end_pos":{"line":97,"col":33}},"use":{"file_name":"TestErrorLocations.fst","start_pos":{"line":97,"col":28},"end_pos":{"line":97,"col":33}}},"number":19,"ctx":["While typechecking the top-level declaration `let test_elim_forall`","While typechecking the top-level declaration `[@@expect_failure] let test_elim_forall`"]} +>>] +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type Prims.squash (p /\\ q)\ngot type Prims.unit","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"TestErrorLocations.fst","start_pos":{"line":101,"col":19},"end_pos":{"line":101,"col":20}},"use":{"file_name":"TestErrorLocations.fst","start_pos":{"line":102,"col":12},"end_pos":{"line":102,"col":13}}},"number":19,"ctx":["While typechecking the top-level declaration `let test_elim_and`","While typechecking the top-level declaration `[@@expect_failure] let test_elim_and`"]} +>>] +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type Prims.squash (p /\\ q)\ngot type Prims.unit","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"TestErrorLocations.fst","start_pos":{"line":107,"col":21},"end_pos":{"line":107,"col":22}},"use":{"file_name":"TestErrorLocations.fst","start_pos":{"line":108,"col":17},"end_pos":{"line":108,"col":18}}},"number":19,"ctx":["While typechecking the top-level declaration `let test_elim_and`","While typechecking the top-level declaration `[@@expect_failure] let test_elim_and`"]} +>>] +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type Prims.squash (p \\/ q)\ngot type Prims.unit","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"FStar.Classical.Sugar.fsti","start_pos":{"line":88,"col":21},"end_pos":{"line":88,"col":31}},"use":{"file_name":"TestErrorLocations.fst","start_pos":{"line":114,"col":12},"end_pos":{"line":114,"col":18}}},"number":19,"ctx":["While typechecking the top-level declaration `let test_elim_or`","While typechecking the top-level declaration `[@@expect_failure] let test_elim_or`"]} +>>] +{"msg":["TestErrorLocations.test5\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"TestErrorLocations.fst","start_pos":{"line":46,"col":4},"end_pos":{"line":46,"col":9}},"use":{"file_name":"TestErrorLocations.fst","start_pos":{"line":46,"col":4},"end_pos":{"line":46,"col":9}}},"number":240,"ctx":["While desugaring module TestErrorLocations"]} +{"msg":["TestErrorLocations.test6\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"TestErrorLocations.fst","start_pos":{"line":56,"col":4},"end_pos":{"line":56,"col":9}},"use":{"file_name":"TestErrorLocations.fst","start_pos":{"line":56,"col":4},"end_pos":{"line":56,"col":9}}},"number":240,"ctx":["While desugaring module TestErrorLocations"]} +{"msg":["TestErrorLocations.test7\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"TestErrorLocations.fst","start_pos":{"line":60,"col":4},"end_pos":{"line":60,"col":9}},"use":{"file_name":"TestErrorLocations.fst","start_pos":{"line":60,"col":4},"end_pos":{"line":60,"col":9}}},"number":240,"ctx":["While desugaring module TestErrorLocations"]} +{"msg":["Missing definitions in module TestErrorLocations:\n test5\n test6\n test7"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"TestErrorLocations.fst","start_pos":{"line":113,"col":0},"end_pos":{"line":117,"col":17}}},"number":240,"ctx":[]} +Verified module: TestErrorLocations +All verification conditions discharged successfully diff --git a/tests/error-messages/TestHasEq.fst.json_expected b/tests/error-messages/TestHasEq.fst.json_expected new file mode 100644 index 00000000000..6ee1378b13a --- /dev/null +++ b/tests/error-messages/TestHasEq.fst.json_expected @@ -0,0 +1,11 @@ +>> Got issues: [ +{"msg":["Failed to prove that the type\n'TestHasEq.t3'\nsupports decidable equality because of this argument.","Add either the 'noeq' or 'unopteq' qualifier","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"TestHasEq.fst","start_pos":{"line":57,"col":0},"end_pos":{"line":58,"col":19}},"use":{"file_name":"TestHasEq.fst","start_pos":{"line":58,"col":10},"end_pos":{"line":58,"col":11}}},"number":19,"ctx":["While typechecking the top-level declaration `type TestHasEq.t3`","While typechecking the top-level declaration `[@@expect_failure] type TestHasEq.t3`"]} +>>] +>> Got issues: [ +{"msg":["Subtyping check failed","Expected type Prims.eqtype\ngot type Type0","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"TestHasEq.fst","start_pos":{"line":84,"col":12},"end_pos":{"line":84,"col":22}},"use":{"file_name":"TestHasEq.fst","start_pos":{"line":84,"col":10},"end_pos":{"line":84,"col":70}}},"number":19,"ctx":["While typechecking the top-level declaration `let test`","While typechecking the top-level declaration `[@@expect_failure] let test`"]} +>>] +>> Got issues: [ +{"msg":["The qualifier list\n[unopteq]\nis not permissible for this element","The `unopteq` qualifier is not allowed on erasable inductives since they don't\nhave decidable equality."],"level":"Error","range":{"def":{"file_name":"TestHasEq.fst","start_pos":{"line":88,"col":8},"end_pos":{"line":89,"col":30}},"use":{"file_name":"TestHasEq.fst","start_pos":{"line":88,"col":8},"end_pos":{"line":89,"col":30}}},"number":162,"ctx":["While typechecking the top-level declaration `type TestHasEq.erasable_t2`","While typechecking the top-level declaration `[@@expect_failure] type TestHasEq.erasable_t2`"]} +>>] +Verified module: TestHasEq +All verification conditions discharged successfully diff --git a/tests/error-messages/UnboundOp.fst.json_expected b/tests/error-messages/UnboundOp.fst.json_expected new file mode 100644 index 00000000000..39e8b8263b2 --- /dev/null +++ b/tests/error-messages/UnboundOp.fst.json_expected @@ -0,0 +1,5 @@ +>> Got issues: [ +{"msg":["Unexpected or unbound operator: ^%^"],"level":"Error","range":{"def":{"file_name":"UnboundOp.fst","start_pos":{"line":4,"col":10},"end_pos":{"line":4,"col":13}},"use":{"file_name":"UnboundOp.fst","start_pos":{"line":4,"col":10},"end_pos":{"line":4,"col":13}}},"number":180,"ctx":["While desugaring module UnboundOp"]} +>>] +Verified module: UnboundOp +All verification conditions discharged successfully diff --git a/tests/error-messages/Unit2.fst.json_expected b/tests/error-messages/Unit2.fst.json_expected new file mode 100644 index 00000000000..57a530df15b --- /dev/null +++ b/tests/error-messages/Unit2.fst.json_expected @@ -0,0 +1,5 @@ +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Unit2.fst","start_pos":{"line":37,"col":21},"end_pos":{"line":38,"col":60}},"use":{"file_name":"Unit2.fst","start_pos":{"line":37,"col":21},"end_pos":{"line":38,"col":60}}},"number":19,"ctx":["While typechecking the top-level declaration `let test6`","While typechecking the top-level declaration `[@@expect_failure] let test6`"]} +>>] +Verified module: Unit2 +All verification conditions discharged successfully diff --git a/tests/error-messages/UnresolvedFields.fst.json_expected b/tests/error-messages/UnresolvedFields.fst.json_expected new file mode 100644 index 00000000000..aa597bddf44 --- /dev/null +++ b/tests/error-messages/UnresolvedFields.fst.json_expected @@ -0,0 +1,11 @@ +>> Got issues: [ +{"msg":["Field name c could not be resolved."],"level":"Error","range":{"def":{"file_name":"UnresolvedFields.fst","start_pos":{"line":10,"col":4},"end_pos":{"line":10,"col":5}},"use":{"file_name":"UnresolvedFields.fst","start_pos":{"line":10,"col":4},"end_pos":{"line":10,"col":5}}},"number":360,"ctx":["While typechecking the top-level declaration `let test0`","While typechecking the top-level declaration `[@@expect_failure] let test0`"]} +>>] +>> Got issues: [ +{"msg":["Field 'c' is redundant for type UnresolvedFields.t",""],"level":"Error","range":{"def":{"file_name":"UnresolvedFields.fst","start_pos":{"line":17,"col":4},"end_pos":{"line":17,"col":5}},"use":{"file_name":"UnresolvedFields.fst","start_pos":{"line":17,"col":4},"end_pos":{"line":17,"col":5}}},"number":118,"ctx":["While typechecking the top-level declaration `let test1`","While typechecking the top-level declaration `[@@expect_failure] let test1`"]} +>>] +>> Got issues: [ +{"msg":["Field 'c' is redundant for type UnresolvedFields.t",""],"level":"Error","range":{"def":{"file_name":"UnresolvedFields.fst","start_pos":{"line":26,"col":4},"end_pos":{"line":26,"col":5}},"use":{"file_name":"UnresolvedFields.fst","start_pos":{"line":26,"col":4},"end_pos":{"line":26,"col":5}}},"number":118,"ctx":["While typechecking the top-level declaration `let test2`","While typechecking the top-level declaration `[@@expect_failure] let test2`"]} +>>] +Verified module: UnresolvedFields +All verification conditions discharged successfully diff --git a/tests/error-messages/WPExtensionality.fst.json_expected b/tests/error-messages/WPExtensionality.fst.json_expected new file mode 100644 index 00000000000..75c78a0d750 --- /dev/null +++ b/tests/error-messages/WPExtensionality.fst.json_expected @@ -0,0 +1,5 @@ +>> Got issues: [ +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":451,"col":90},"end_pos":{"line":451,"col":102}},"use":{"file_name":"WPExtensionality.fst","start_pos":{"line":61,"col":3},"end_pos":{"line":61,"col":34}}},"number":19,"ctx":["While typechecking the top-level declaration `let bug`","While typechecking the top-level declaration `[@@expect_failure] let bug`"]} +>>] +Verified module: WPExtensionality +All verification conditions discharged successfully