Fix --use_nbe_for_extraction option#4179
Draft
mtzguido wants to merge 1 commit into
Draft
Annotations
10 warnings
|
FStarC.BaseTypes.fsti#L23
(239) * Warning 239 at /__w/FStar/FStar/FStar/src/basic/FStarC.BaseTypes.fsti(23,5-23,10):
- Adding an implicit 'assume new' qualifier on FStarC.BaseTypes.float
|
|
FStar.UInt.fsti#L436
(271) * Warning 271 at /__w/FStar/FStar/FStar/stage0/out/lib/fstar/ulib/FStar.UInt.fsti(436,8-436,51):
- Pattern uses these theory symbols or terms that should not be in an SMT
pattern:
Prims.op_Subtraction
|
|
FStarC.PIMap.fsti#L7
(239) * Warning 239 at /__w/FStar/FStar/FStar/src/data/FStarC.PIMap.fsti(7,5-7,6):
- Adding an implicit 'assume new' qualifier on FStarC.PIMap.t
|
|
FStarC.IMap.fsti#L7
(239) * Warning 239 at /__w/FStar/FStar/FStar/src/data/FStarC.IMap.fsti(7,5-7,6):
- Adding an implicit 'assume new' qualifier on FStarC.IMap.t
|
|
FStarC.Unionfind.fsti#L21
(239) * Warning 239 at /__w/FStar/FStar/FStar/src/basic/FStarC.Unionfind.fsti(21,5-21,11):
- Adding an implicit 'assume new' qualifier on FStarC.Unionfind.p_uvar
|
|
FStarC.Unionfind.fsti#L20
(239) * Warning 239 at /__w/FStar/FStar/FStar/src/basic/FStarC.Unionfind.fsti(20,5-20,8):
- Adding an implicit 'assume new' qualifier on FStarC.Unionfind.puf
|
|
FStarC.Hash.fsti#L4
(239) * Warning 239 at /__w/FStar/FStar/FStar/src/basic/FStarC.Hash.fsti(4,5-4,14):
- Adding an implicit 'assume new' qualifier on FStarC.Hash.hash_code
|
|
FStarC.Timing.fsti#L20
(239) * Warning 239 at /__w/FStar/FStar/FStar/src/basic/FStarC.Timing.fsti(20,5-20,12):
- Adding an implicit 'assume new' qualifier on FStarC.Timing.time_ns
|
|
FStarC.SMap.fsti#L7
(239) * Warning 239 at /__w/FStar/FStar/FStar/src/data/FStarC.SMap.fsti(7,5-7,6):
- Adding an implicit 'assume new' qualifier on FStarC.SMap.t
|
|
FStarC.PSMap.fsti#L7
(239) * Warning 239 at /__w/FStar/FStar/FStar/src/data/FStarC.PSMap.fsti(7,5-7,6):
- Adding an implicit 'assume new' qualifier on FStarC.PSMap.t
|
The logs for this run have expired and are no longer available.
Loading