Mark the (deprecated) alloc/free for Array and Ref as private #411
Annotations
10 warnings
|
Pulse.Syntax.Base.fst#L293
(290) * Warning 290 at /__w/pulse/pulse/pulse/src/checker/Pulse.Syntax.Base.fst(293,15-293,17):
- In the decreases clause for this function, the SMT solver may not be able to
prove that the types of
b1 (bound in Pulse.Syntax.Base.fst(293,15-293,17))
and q1 (bound in Pulse.Syntax.Base.fst(298,14-298,16))
are equal.
- The type of the first term is: Pulse.Syntax.Base.branch
- The type of the second term is: Pulse.Syntax.Base.qualifier
- If the proof fails, try annotating these with the same type.
|
|
Pulse.Syntax.Base.fst#L293
(290) * Warning 290 at /__w/pulse/pulse/pulse/src/checker/Pulse.Syntax.Base.fst(293,15-293,17):
- In the decreases clause for this function, the SMT solver may not be able to
prove that the types of
b1 (bound in Pulse.Syntax.Base.fst(293,15-293,17))
and t1 (bound in Pulse.Syntax.Base.fst(171,20-171,22))
are equal.
- The type of the first term is: Pulse.Syntax.Base.branch
- The type of the second term is: Pulse.Syntax.Base.st_term
- If the proof fails, try annotating these with the same type.
|
|
Pulse.Syntax.Base.fst#L139
(290) * Warning 290 at /__w/pulse/pulse/pulse/src/checker/Pulse.Syntax.Base.fst(139,16-139,19):
- In the decreases clause for this function, the SMT solver may not be able to
prove that the types of
pb1 (bound in Pulse.Syntax.Base.fst(139,16-139,19))
and p1 (bound in Pulse.Syntax.Base.fst(123,20-123,22))
are equal.
- The type of the first term is: Pulse.Syntax.Base.pattern & Prims.bool
- The type of the second term is: Pulse.Syntax.Base.pattern
- If the proof fails, try annotating these with the same type.
|
|
Pulse.Syntax.Base.fst#L123
(290) * Warning 290 at /__w/pulse/pulse/pulse/src/checker/Pulse.Syntax.Base.fst(123,20-123,22):
- In the decreases clause for this function, the SMT solver may not be able to
prove that the types of
p1 (bound in Pulse.Syntax.Base.fst(123,20-123,22))
and pb1 (bound in Pulse.Syntax.Base.fst(139,16-139,19))
are equal.
- The type of the first term is: Pulse.Syntax.Base.pattern
- The type of the second term is: Pulse.Syntax.Base.pattern & Prims.bool
- If the proof fails, try annotating these with the same type.
|
|
PulseSyntaxExtension.Desugar.fst#L879
(328) * Warning 328 at /__w/pulse/pulse/pulse/src/syntax_extension/PulseSyntaxExtension.Desugar.fst(879,4-879,16):
- Global binding
'PulseSyntaxExtension.Desugar.desugar_decl'
is recursive but not used in its body
|
|
Pulse.Common.fst#L84
(337) * Warning 337 at /__w/pulse/pulse/pulse/src/checker/Pulse.Common.fst(84,11-84,12):
- The operator '@' has been resolved to FStar.List.Tot.append even though
FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop
relying on this deprecated, special treatment of '@'.
|
|
PulseSyntaxExtension.Sugar.fst#L627
(337) * Warning 337 at /__w/pulse/pulse/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst(627,47-627,48):
- The operator '@' has been resolved to FStar.List.Tot.append even though
FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop
relying on this deprecated, special treatment of '@'.
|
|
PulseSyntaxExtension.Sugar.fst#L626
(337) * Warning 337 at /__w/pulse/pulse/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst(626,47-626,48):
- The operator '@' has been resolved to FStar.List.Tot.append even though
FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop
relying on this deprecated, special treatment of '@'.
|
|
PulseSyntaxExtension.Sugar.fst#L518
(328) * Warning 328 at /__w/pulse/pulse/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst(518,8-518,17):
- Global binding
'PulseSyntaxExtension.Sugar.scan_decl'
is recursive but not used in its body
|
|
PulseSyntaxExtension.Sugar.fst#L370
(328) * Warning 328 at /__w/pulse/pulse/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst(370,8-370,15):
- Global binding
'PulseSyntaxExtension.Sugar.eq_decl'
is recursive but not used in its body
|
The logs for this run have expired and are no longer available.
Loading