Using Z3 4.15.3 #969
Annotations
3 errors and 10 warnings
|
Run tests, without forcing a build
The operation was canceled.
|
|
Run tests, without forcing a build:
Sec2.HIFC.fst#L167
(19) * Error 19 at Sec2.HIFC.fst(842,4-842,56):
- Assertion failed
- See also Sec2.HIFC.fst(167,65-167,125)
|
|
|
|
Run tests, without forcing a build:
dummy#L0
(274) * Warning 274:
- Implicitly opening namespace 'fstar.tactics.' shadows module 'typeclasses'
in file "Typeclasses.fst".
- Rename "Typeclasses.fst" to avoid conflicts.
|
|
Run tests, without forcing a build:
dummy#L0
(274) * Warning 274:
- Implicitly opening namespace 'fstar.list.' shadows module 'pure' in file
"Pure.fst".
- Rename "Pure.fst" to avoid conflicts.
|
|
Run tests, without forcing a build:
dummy#L0
(274) * Warning 274:
- Implicitly opening namespace 'fstar.' shadows module 'uint32' in file
"UInt32.fsti, UInt32.fst".
- Rename "UInt32.fsti, UInt32.fst" to avoid conflicts.
|
|
Run tests, without forcing a build:
dummy#L0
(361) * Warning 361 at AlexOpaque.fst(103,0-125,5):
- Some #push-options have not been popped. Current depth is 2.
|
|
Run tests, without forcing a build:
Test.fst#L21
(272) * Warning 272 at Test.fst(21,0-21,31):
- Top-level let-bindings must be total; this term may have effects
|
|
Run tests, without forcing a build:
dummy#L0
(274) * Warning 274:
- Implicitly opening namespace 'fstar.' shadows module 'uint32' in file
"UInt32.fsti, UInt32.fst".
- Rename "UInt32.fsti, UInt32.fst" to avoid conflicts.
|
|
Run tests, without forcing a build:
Hello.fst#L5
(272) * Warning 272 at Hello.fst(5,0-5,34):
- Top-level let-bindings must be total; this term may have effects
|
|
Run tests, without forcing a build:
dummy#L0
(274) * Warning 274:
- Implicitly opening namespace 'fstar.tactics.' shadows module 'typeclasses'
in file "Typeclasses.fst".
- Rename "Typeclasses.fst" to avoid conflicts.
|
|
Run tests, without forcing a build:
dummy#L0
(274) * Warning 274:
- Implicitly opening namespace 'fstar.list.' shadows module 'pure' in file
"Pure.fst".
- Rename "Pure.fst" to avoid conflicts.
|
|
Run tests, without forcing a build:
dummy#L0
(274) * Warning 274:
- Implicitly opening namespace 'fstar.' shadows module 'uint32' in file
"UInt32.fsti, UInt32.fst".
- Rename "UInt32.fsti, UInt32.fst" to avoid conflicts.
|
Loading