Adding tests for --message_format json

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)
 

tests/error-messages/.gitignore

@@ -1,2 +1,5 @@
 *.output
+*.json_output
 *.check
+*.human_check
+*.json_check

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

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

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

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

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

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

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

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

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

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