Add some tests

tests/bug-reports/Bug3232a.fst

@@ -0,0 +1,7 @@
+module Bug3232a
+
+inline_for_extraction noextract
+val f (x:int) : unit
+
+noextract inline_for_extraction
+let f x = ()

tests/error-messages/Bug3232b.fst

@@ -0,0 +1,8 @@
+module Bug3232b
+
+inline_for_extraction
+val f (x:int) : unit
+
+[@@expect_failure]
+noextract inline_for_extraction
+let f x = ()

tests/error-messages/Bug3232b.fst.expected

@@ -0,0 +1,16 @@
+>> Got issues: [
+* Error 93 at Bug3232b.fst(8,0-8,12):
+  - Inconsistent qualifier annotations on Bug3232b.f
+  - Expected '[inline_for_extraction]' got '[noextract, inline_for_extraction]'
+  - Only in definition: '[noextract]'
+
+>>]
+* Warning 240 at Bug3232b.fst(4,4-4,5):
+  - Bug3232b.f is declared but no definition was found
+  - Add an 'assume' if this is intentional
+
+* Warning 240 at Bug3232b.fst(8,0-8,12):
+  - Missing definitions in module Bug3232b: f
+
+Verified module: Bug3232b
+All verification conditions discharged successfully

tests/error-messages/Bug3232b.fst.json_expected

@@ -0,0 +1,7 @@
+>> Got issues: [
+{"msg":["Inconsistent qualifier annotations on\nBug3232b.f","Expected '[inline_for_extraction]'\ngot '[noextract, inline_for_extraction]'","","Only in definition: '[noextract]'"],"level":"Error","range":{"def":{"file_name":"Bug3232b.fst","start_pos":{"line":8,"col":0},"end_pos":{"line":8,"col":12}},"use":{"file_name":"Bug3232b.fst","start_pos":{"line":8,"col":0},"end_pos":{"line":8,"col":12}}},"number":93,"ctx":["While typechecking the top-level declaration `let f`","While typechecking the top-level declaration `[@@expect_failure] let f`"]}
+>>]
+{"msg":["Bug3232b.f\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"Bug3232b.fst","start_pos":{"line":4,"col":4},"end_pos":{"line":4,"col":5}},"use":{"file_name":"Bug3232b.fst","start_pos":{"line":4,"col":4},"end_pos":{"line":4,"col":5}}},"number":240,"ctx":["While desugaring module Bug3232b"]}
+{"msg":["Missing definitions in module Bug3232b: f"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"Bug3232b.fst","start_pos":{"line":8,"col":0},"end_pos":{"line":8,"col":12}}},"number":240,"ctx":[]}
+Verified module: Bug3232b
+All verification conditions discharged successfully

tests/error-messages/Bug3232c.fst

@@ -0,0 +1,8 @@
+module Bug3232c
+
+inline_for_extraction noextract
+val f (x:int) : unit
+
+[@@expect_failure]
+noextract
+let f x = ()

tests/error-messages/Bug3232c.fst.expected

@@ -0,0 +1,16 @@
+>> Got issues: [
+* Error 93 at Bug3232c.fst(8,0-8,12):
+  - Inconsistent qualifier annotations on Bug3232c.f
+  - Expected '[inline_for_extraction, noextract]' got '[noextract]'
+  - Only in declaration: '[inline_for_extraction]'
+
+>>]
+* Warning 240 at Bug3232c.fst(4,4-4,5):
+  - Bug3232c.f is declared but no definition was found
+  - Add an 'assume' if this is intentional
+
+* Warning 240 at Bug3232c.fst(8,0-8,12):
+  - Missing definitions in module Bug3232c: f
+
+Verified module: Bug3232c
+All verification conditions discharged successfully

tests/error-messages/Bug3232c.fst.json_expected

@@ -0,0 +1,7 @@
+>> Got issues: [
+{"msg":["Inconsistent qualifier annotations on\nBug3232c.f","Expected '[inline_for_extraction, noextract]'\ngot '[noextract]'","Only in declaration: '[inline_for_extraction]'",""],"level":"Error","range":{"def":{"file_name":"Bug3232c.fst","start_pos":{"line":8,"col":0},"end_pos":{"line":8,"col":12}},"use":{"file_name":"Bug3232c.fst","start_pos":{"line":8,"col":0},"end_pos":{"line":8,"col":12}}},"number":93,"ctx":["While typechecking the top-level declaration `let f`","While typechecking the top-level declaration `[@@expect_failure] let f`"]}
+>>]
+{"msg":["Bug3232c.f\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"Bug3232c.fst","start_pos":{"line":4,"col":4},"end_pos":{"line":4,"col":5}},"use":{"file_name":"Bug3232c.fst","start_pos":{"line":4,"col":4},"end_pos":{"line":4,"col":5}}},"number":240,"ctx":["While desugaring module Bug3232c"]}
+{"msg":["Missing definitions in module Bug3232c: f"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"Bug3232c.fst","start_pos":{"line":8,"col":0},"end_pos":{"line":8,"col":12}}},"number":240,"ctx":[]}
+Verified module: Bug3232c
+All verification conditions discharged successfully

tests/error-messages/Bug3232d.fst

@@ -0,0 +1,8 @@
+module Bug3232d
+
+inline_for_extraction
+val f (x:int) : unit
+
+[@@expect_failure]
+noextract
+let f x = ()

tests/error-messages/Bug3232d.fst.expected

@@ -0,0 +1,17 @@
+>> Got issues: [
+* Error 93 at Bug3232d.fst(8,0-8,12):
+  - Inconsistent qualifier annotations on Bug3232d.f
+  - Expected '[inline_for_extraction]' got '[noextract]'
+  - Only in declaration: '[inline_for_extraction]'
+  - Only in definition: '[noextract]'
+
+>>]
+* Warning 240 at Bug3232d.fst(4,4-4,5):
+  - Bug3232d.f is declared but no definition was found
+  - Add an 'assume' if this is intentional
+
+* Warning 240 at Bug3232d.fst(8,0-8,12):
+  - Missing definitions in module Bug3232d: f
+
+Verified module: Bug3232d
+All verification conditions discharged successfully

tests/error-messages/Bug3232d.fst.json_expected

@@ -0,0 +1,7 @@
+>> Got issues: [
+{"msg":["Inconsistent qualifier annotations on\nBug3232d.f","Expected '[inline_for_extraction]'\ngot '[noextract]'","Only in declaration: '[inline_for_extraction]'","Only in definition: '[noextract]'"],"level":"Error","range":{"def":{"file_name":"Bug3232d.fst","start_pos":{"line":8,"col":0},"end_pos":{"line":8,"col":12}},"use":{"file_name":"Bug3232d.fst","start_pos":{"line":8,"col":0},"end_pos":{"line":8,"col":12}}},"number":93,"ctx":["While typechecking the top-level declaration `let f`","While typechecking the top-level declaration `[@@expect_failure] let f`"]}
+>>]
+{"msg":["Bug3232d.f\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"Bug3232d.fst","start_pos":{"line":4,"col":4},"end_pos":{"line":4,"col":5}},"use":{"file_name":"Bug3232d.fst","start_pos":{"line":4,"col":4},"end_pos":{"line":4,"col":5}}},"number":240,"ctx":["While desugaring module Bug3232d"]}
+{"msg":["Missing definitions in module Bug3232d: f"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"Bug3232d.fst","start_pos":{"line":8,"col":0},"end_pos":{"line":8,"col":12}}},"number":240,"ctx":[]}
+Verified module: Bug3232d
+All verification conditions discharged successfully