Skip to content

Commit f1bf278

Browse files
gebnergebner
committed
Fix tests.
1 parent d41589f commit f1bf278

File tree

2 files changed

+12
-12
lines changed

2 files changed

+12
-12
lines changed

‎tests/error-messages/Bug2899.fst.json_output.expected

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
{"msg":["Expected failure:","Tactic failed","Tactic got stuck!","Reduction stopped at:\n FStar.Stubs.Tactics.Result.Success (Prims.admit ()) \"(((proofstate)))\"","The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?"],"level":"Info","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":200,"col":48},"end_pos":{"line":200,"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`"]}
2-
{"msg":["Expected failure:","Tactic failed","Tactic got stuck!","Reduction stopped at: Prims.admit ()","The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?"],"level":"Info","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":200,"col":48},"end_pos":{"line":200,"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`"]}
3-
{"msg":["Expected failure:","Tactic failed","Tactic got stuck!","Reduction stopped at:\n FStar.Stubs.Tactics.V2.Builtins.dump (Prims.admit ()) \"(((proofstate)))\"","The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?"],"level":"Info","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":200,"col":48},"end_pos":{"line":200,"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`"]}
4-
{"msg":["Expected failure:","Tactic failed","Tactic got stuck!","Reduction stopped at: reify (tac ()) \"(((proofstate)))\"",""],"level":"Info","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":200,"col":48},"end_pos":{"line":200,"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`"]}
1+
{"msg":["Expected failure:","Tactic failed","Tactic got stuck!","Reduction stopped at: Prims.admit ()","The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?"],"level":"Info","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":198,"col":48},"end_pos":{"line":198,"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`"]}
2+
{"msg":["Expected failure:","Tactic failed","Tactic got stuck!","Reduction stopped at: Prims.admit ()","The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?"],"level":"Info","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":198,"col":48},"end_pos":{"line":198,"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`"]}
3+
{"msg":["Expected failure:","Tactic failed","Tactic got stuck!","Reduction stopped at:\n FStar.Stubs.Tactics.V2.Builtins.dump (Prims.admit ()) \"(((ref proofstate)))\"","The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?"],"level":"Info","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":198,"col":48},"end_pos":{"line":198,"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`"]}
4+
{"msg":["Expected failure:","Tactic failed","Tactic got stuck!","Reduction stopped at: reify (tac ()) \"(((ref proofstate)))\"",""],"level":"Info","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":198,"col":48},"end_pos":{"line":198,"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`"]}

‎tests/error-messages/Bug2899.fst.output.expected

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -2,32 +2,32 @@
22
- Expected failure:
33
- Tactic failed
44
- Tactic got stuck!
5-
- Reduction stopped at:
6-
FStar.Stubs.Tactics.Result.Success (Prims.admit ()) "(((proofstate)))"
5+
- Reduction stopped at: Prims.admit ()
76
- The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?
8-
- See also FStar.Tactics.Effect.fsti(200,48-200,58)
7+
- See also FStar.Tactics.Effect.fsti(198,48-198,58)
98

109
* Info at Bug2899.fst(10,12-10,18):
1110
- Expected failure:
1211
- Tactic failed
1312
- Tactic got stuck!
1413
- Reduction stopped at: Prims.admit ()
1514
- The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?
16-
- See also FStar.Tactics.Effect.fsti(200,48-200,58)
15+
- See also FStar.Tactics.Effect.fsti(198,48-198,58)
1716

1817
* Info at Bug2899.fst(13,12-13,18):
1918
- Expected failure:
2019
- Tactic failed
2120
- Tactic got stuck!
2221
- Reduction stopped at:
23-
FStar.Stubs.Tactics.V2.Builtins.dump (Prims.admit ()) "(((proofstate)))"
22+
FStar.Stubs.Tactics.V2.Builtins.dump (Prims.admit ())
23+
"(((ref proofstate)))"
2424
- The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?
25-
- See also FStar.Tactics.Effect.fsti(200,48-200,58)
25+
- See also FStar.Tactics.Effect.fsti(198,48-198,58)
2626

2727
* Info at Bug2899.fst(17,50-17,66):
2828
- Expected failure:
2929
- Tactic failed
3030
- Tactic got stuck!
31-
- Reduction stopped at: reify (tac ()) "(((proofstate)))"
32-
- See also FStar.Tactics.Effect.fsti(200,48-200,58)
31+
- Reduction stopped at: reify (tac ()) "(((ref proofstate)))"
32+
- See also FStar.Tactics.Effect.fsti(198,48-198,58)
3333

0 commit comments

Comments
 (0)