CCSDS Frame Security Report (FSR)
fsr fuzz: pack the four alarm/bad_* flags into a single int (E350)
The fuzz tests previously took four unlabeled bool generators, one per
flag field. Combine them into a single [range 16] generator decoded via
an [fsr_of_bits] helper so each test function has 0 bool parameters and
fuzz coverage is unchanged (all 16 combinations still sampled).
+2016
-20
+243
c/EverParse.h
+243
c/EverParse.h
···
1
+
/*++
2
+
3
+
Copyright (c) Microsoft Corporation
4
+
5
+
Module Name:
6
+
7
+
EverParse.h
8
+
9
+
Abstract:
10
+
11
+
This is an EverParse-generated file that contains common auxiliary
12
+
functions for EverParse-generated verified data validators.
13
+
14
+
This file was generated by EverParse v2026.02.25
15
+
16
+
Authors:
17
+
18
+
nswamy, protz, taramana 5-Feb-2020
19
+
20
+
--*/
21
+
22
+
23
+
#ifndef EverParse_H
24
+
#define EverParse_H
25
+
26
+
#if defined(__cplusplus)
27
+
extern "C" {
28
+
#endif
29
+
30
+
#include "EverParseEndianness.h"
31
+
32
+
static inline uint8_t EverParseGetBitfield8(uint8_t Value, uint32_t BitsFrom, uint32_t BitsTo)
33
+
{
34
+
uint8_t op1 = (uint32_t)Value << (8U - BitsTo);
35
+
return (uint32_t)op1 >> (8U - BitsTo + BitsFrom);
36
+
}
37
+
38
+
static inline uint16_t
39
+
EverParseGetBitfield16(uint16_t Value, uint32_t BitsFrom, uint32_t BitsTo)
40
+
{
41
+
uint16_t bf = (uint32_t)Value << (16U - BitsTo);
42
+
return (uint32_t)bf >> (16U - BitsTo + BitsFrom);
43
+
}
44
+
45
+
static inline uint32_t
46
+
EverParseGetBitfield32(uint32_t Value, uint32_t BitsFrom, uint32_t BitsTo)
47
+
{
48
+
return Value << (32U - BitsTo) >> (32U - BitsTo + BitsFrom);
49
+
}
50
+
51
+
static inline uint64_t
52
+
EverParseGetBitfield64(uint64_t Value, uint32_t BitsFrom, uint32_t BitsTo)
53
+
{
54
+
return Value << (64U - BitsTo) >> (64U - BitsTo + BitsFrom);
55
+
}
56
+
57
+
static inline uint8_t
58
+
EverParseGetBitfield8MsbFirst(uint8_t Value, uint32_t BitsFrom, uint32_t BitsTo)
59
+
{
60
+
return EverParseGetBitfield8(Value, 8U - BitsTo, 8U - BitsFrom);
61
+
}
62
+
63
+
static inline uint16_t
64
+
EverParseGetBitfield16MsbFirst(uint16_t Value, uint32_t BitsFrom, uint32_t BitsTo)
65
+
{
66
+
return EverParseGetBitfield16(Value, 16U - BitsTo, 16U - BitsFrom);
67
+
}
68
+
69
+
static inline uint32_t
70
+
EverParseGetBitfield32MsbFirst(uint32_t Value, uint32_t BitsFrom, uint32_t BitsTo)
71
+
{
72
+
return EverParseGetBitfield32(Value, 32U - BitsTo, 32U - BitsFrom);
73
+
}
74
+
75
+
static inline uint64_t
76
+
EverParseGetBitfield64MsbFirst(uint64_t Value, uint32_t BitsFrom, uint32_t BitsTo)
77
+
{
78
+
return EverParseGetBitfield64(Value, 64U - BitsTo, 64U - BitsFrom);
79
+
}
80
+
81
+
#define EVERPARSE_VALIDATOR_MAX_LENGTH (1152921504606846975ULL)
82
+
83
+
static inline BOOLEAN EverParseIsError(uint64_t PositionOrError)
84
+
{
85
+
return PositionOrError > EVERPARSE_VALIDATOR_MAX_LENGTH;
86
+
}
87
+
88
+
static inline BOOLEAN EverParseIsSuccess(uint64_t PositionOrError)
89
+
{
90
+
return PositionOrError <= EVERPARSE_VALIDATOR_MAX_LENGTH;
91
+
}
92
+
93
+
static inline uint64_t EverParseSetValidatorErrorPos(uint64_t Error, uint64_t Position)
94
+
{
95
+
return (Error & 17293822569102704640ULL) | Position << 0U;
96
+
}
97
+
98
+
static inline uint64_t EverParseGetValidatorErrorPos(uint64_t X)
99
+
{
100
+
return (X & 1152921504606846975ULL) >> 0U;
101
+
}
102
+
103
+
static inline uint64_t EverParseSetValidatorErrorKind(uint64_t Error, uint64_t Code)
104
+
{
105
+
return (Error & 1152921504606846975ULL) | Code << 60U;
106
+
}
107
+
108
+
static inline uint64_t EverParseGetValidatorErrorKind(uint64_t Error)
109
+
{
110
+
return (Error & 17293822569102704640ULL) >> 60U;
111
+
}
112
+
113
+
#define EVERPARSE_VALIDATOR_ERROR_GENERIC (1152921504606846976ULL)
114
+
115
+
#define EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA (2305843009213693952ULL)
116
+
117
+
#define EVERPARSE_VALIDATOR_ERROR_IMPOSSIBLE (3458764513820540928ULL)
118
+
119
+
#define EVERPARSE_VALIDATOR_ERROR_LIST_SIZE_NOT_MULTIPLE (4611686018427387904ULL)
120
+
121
+
#define EVERPARSE_VALIDATOR_ERROR_ACTION_FAILED (5764607523034234880ULL)
122
+
123
+
#define EVERPARSE_VALIDATOR_ERROR_CONSTRAINT_FAILED (6917529027641081856ULL)
124
+
125
+
#define EVERPARSE_VALIDATOR_ERROR_UNEXPECTED_PADDING (8070450532247928832ULL)
126
+
127
+
#define EVERPARSE_VALIDATOR_ERROR_PROBE_FAILED (9223372036854775808ULL)
128
+
129
+
static inline PRIMS_STRING EverParseErrorReasonOfResult(uint64_t Code)
130
+
{
131
+
switch (EverParseGetValidatorErrorKind(Code))
132
+
{
133
+
case 1ULL:
134
+
{
135
+
return "generic error";
136
+
}
137
+
case 2ULL:
138
+
{
139
+
return "not enough data";
140
+
}
141
+
case 3ULL:
142
+
{
143
+
return "impossible";
144
+
}
145
+
case 4ULL:
146
+
{
147
+
return "list size not multiple of element size";
148
+
}
149
+
case 5ULL:
150
+
{
151
+
return "action failed";
152
+
}
153
+
case 6ULL:
154
+
{
155
+
return "constraint failed";
156
+
}
157
+
case 7ULL:
158
+
{
159
+
return "unexpected padding";
160
+
}
161
+
case 8ULL:
162
+
{
163
+
return "probe failed";
164
+
}
165
+
default:
166
+
{
167
+
return "unspecified";
168
+
}
169
+
}
170
+
}
171
+
172
+
static inline uint64_t EverParseCheckConstraintOk(BOOLEAN Ok, uint64_t Position)
173
+
{
174
+
if (Ok)
175
+
{
176
+
return Position;
177
+
}
178
+
return EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_CONSTRAINT_FAILED, Position);
179
+
}
180
+
181
+
static inline BOOLEAN EverParseIsRangeOkay(uint32_t Size, uint32_t Offset, uint32_t AccessSize)
182
+
{
183
+
return Size >= AccessSize && (Size - AccessSize) >= Offset;
184
+
}
185
+
186
+
typedef struct EVERPARSE_ERROR_FRAME_s
187
+
{
188
+
BOOLEAN filled;
189
+
uint64_t start_pos;
190
+
PRIMS_STRING typename_s;
191
+
PRIMS_STRING fieldname;
192
+
PRIMS_STRING reason;
193
+
uint64_t error_code;
194
+
}
195
+
EVERPARSE_ERROR_FRAME;
196
+
197
+
typedef uint8_t *EVERPARSE_INPUT_BUFFER;
198
+
199
+
typedef void *EVERPARSE__LIVE;
200
+
201
+
static inline void
202
+
EverParseDefaultErrorHandler(
203
+
PRIMS_STRING TypenameS,
204
+
PRIMS_STRING Fieldname,
205
+
PRIMS_STRING Reason,
206
+
uint64_t ErrorCode,
207
+
EVERPARSE_ERROR_FRAME *Context,
208
+
uint8_t *Input,
209
+
uint64_t StartPos
210
+
)
211
+
{
212
+
KRML_MAYBE_UNUSED_VAR(Input);
213
+
if (!(*Context).filled)
214
+
{
215
+
*Context =
216
+
(
217
+
(EVERPARSE_ERROR_FRAME){
218
+
.filled = TRUE,
219
+
.start_pos = StartPos,
220
+
.typename_s = TypenameS,
221
+
.fieldname = Fieldname,
222
+
.reason = Reason,
223
+
.error_code = ErrorCode
224
+
}
225
+
);
226
+
return;
227
+
}
228
+
}
229
+
230
+
extern uint8_t *EverParseStreamOf(EVERPARSE_COPY_BUFFER_T uu___);
231
+
232
+
extern uint64_t EverParseStreamLen(EVERPARSE_COPY_BUFFER_T c);
233
+
234
+
typedef void *EVERPARSE_INV;
235
+
236
+
typedef void *EVERPARSE_LIVENESS_PRESERVED;
237
+
238
+
#if defined(__cplusplus)
239
+
}
240
+
#endif
241
+
242
+
#define EverParse_H_DEFINED
243
+
#endif /* EverParse_H */
+205
c/EverParseEndianness.h
+205
c/EverParseEndianness.h
···
1
+
/*++
2
+
3
+
Copyright (c) Microsoft Corporation
4
+
5
+
Module Name:
6
+
7
+
EverParseEndianness.h
8
+
9
+
Abstract:
10
+
11
+
This is an EverParse-related file to read integer values from raw
12
+
bytes.
13
+
14
+
Authors:
15
+
16
+
nswamy, protz, taramana 5-Feb-2020
17
+
18
+
--*/
19
+
/* This is a hand-written header that selectively includes relevant bits from
20
+
* krmllib.h -- it has to be updated manually to track upstream changes. */
21
+
22
+
#ifndef __EverParseEndianness_H
23
+
#define __EverParseEndianness_H
24
+
25
+
#if defined(__cplusplus)
26
+
extern "C" {
27
+
#endif
28
+
29
+
/*****************************************************************************
30
+
********* Implementation of LowStar.Endianness (selected bits) **************
31
+
*****************************************************************************/
32
+
33
+
#if defined(_MSC_VER)
34
+
# include <windows.h>
35
+
#endif
36
+
37
+
#include <string.h>
38
+
#include <stdint.h>
39
+
40
+
typedef const char * EVERPARSE_STRING;
41
+
typedef EVERPARSE_STRING PRIMS_STRING;
42
+
typedef void* EVERPARSE_COPY_BUFFER_T;
43
+
44
+
#ifndef KRML_MAYBE_UNUSED_VAR
45
+
# define KRML_MAYBE_UNUSED_VAR(x) (void)(x)
46
+
#endif
47
+
48
+
#ifndef KRML_HOST_IGNORE
49
+
# define KRML_HOST_IGNORE(x) (void)(x)
50
+
#endif
51
+
52
+
#ifndef KRML_HOST_PRINTF
53
+
# include <stdio.h>
54
+
# define KRML_HOST_PRINTF printf
55
+
#endif
56
+
57
+
#ifndef KRML_HOST_EXIT
58
+
# include <stdlib.h>
59
+
# define KRML_HOST_EXIT exit
60
+
#endif
61
+
62
+
#define KRML_CHECK_SIZE(size_elt, sz) \
63
+
do { \
64
+
if (((size_t)(sz)) > ((size_t)(SIZE_MAX / (size_elt)))) { \
65
+
KRML_HOST_PRINTF( \
66
+
"Maximum allocatable size exceeded, aborting before overflow at " \
67
+
"%s:%d\n", \
68
+
__FILE__, __LINE__); \
69
+
KRML_HOST_EXIT(253); \
70
+
} \
71
+
} while (0)
72
+
73
+
/* ... for Windows (MSVC)... not targeting XBOX 360! */
74
+
#if defined(_MSC_VER)
75
+
76
+
# include <stdlib.h>
77
+
78
+
# define htobe16(x) _byteswap_ushort(x)
79
+
# define htole16(x) (x)
80
+
# define be16toh(x) _byteswap_ushort(x)
81
+
# define le16toh(x) (x)
82
+
83
+
# define htobe32(x) _byteswap_ulong(x)
84
+
# define htole32(x) (x)
85
+
# define be32toh(x) _byteswap_ulong(x)
86
+
# define le32toh(x) (x)
87
+
88
+
# define htobe64(x) _byteswap_uint64(x)
89
+
# define htole64(x) (x)
90
+
# define be64toh(x) _byteswap_uint64(x)
91
+
# define le64toh(x) (x)
92
+
93
+
#else
94
+
95
+
typedef uint8_t BOOLEAN;
96
+
#define FALSE 0
97
+
#define TRUE 1
98
+
99
+
/* ... for Linux */
100
+
#if defined(__linux__) || defined(__CYGWIN__) || defined (__USE_SYSTEM_ENDIAN_H__)
101
+
# include <endian.h>
102
+
103
+
104
+
/* ... for OSX */
105
+
#elif defined(__APPLE__)
106
+
# include <libkern/OSByteOrder.h>
107
+
# define htole64(x) OSSwapHostToLittleInt64(x)
108
+
# define le64toh(x) OSSwapLittleToHostInt64(x)
109
+
# define htobe64(x) OSSwapHostToBigInt64(x)
110
+
# define be64toh(x) OSSwapBigToHostInt64(x)
111
+
112
+
# define htole16(x) OSSwapHostToLittleInt16(x)
113
+
# define le16toh(x) OSSwapLittleToHostInt16(x)
114
+
# define htobe16(x) OSSwapHostToBigInt16(x)
115
+
# define be16toh(x) OSSwapBigToHostInt16(x)
116
+
117
+
# define htole32(x) OSSwapHostToLittleInt32(x)
118
+
# define le32toh(x) OSSwapLittleToHostInt32(x)
119
+
# define htobe32(x) OSSwapHostToBigInt32(x)
120
+
# define be32toh(x) OSSwapBigToHostInt32(x)
121
+
122
+
/* ... for other BSDs */
123
+
#elif defined(__FreeBSD__) || defined(__NetBSD__) || defined(__DragonFly__)
124
+
# include <sys/endian.h>
125
+
#elif defined(__OpenBSD__)
126
+
# include <endian.h>
127
+
128
+
/* ... for Windows (GCC-like, e.g. mingw or clang) */
129
+
#elif (defined(_WIN32) || defined(_WIN64)) && \
130
+
(defined(__GNUC__) || defined(__clang__))
131
+
132
+
# define htobe16(x) __builtin_bswap16(x)
133
+
# define htole16(x) (x)
134
+
# define be16toh(x) __builtin_bswap16(x)
135
+
# define le16toh(x) (x)
136
+
137
+
# define htobe32(x) __builtin_bswap32(x)
138
+
# define htole32(x) (x)
139
+
# define be32toh(x) __builtin_bswap32(x)
140
+
# define le32toh(x) (x)
141
+
142
+
# define htobe64(x) __builtin_bswap64(x)
143
+
# define htole64(x) (x)
144
+
# define be64toh(x) __builtin_bswap64(x)
145
+
# define le64toh(x) (x)
146
+
147
+
#else
148
+
149
+
#error "Unsupported platform"
150
+
151
+
#endif
152
+
153
+
#endif
154
+
155
+
inline static uint16_t Load16(uint8_t *b) {
156
+
uint16_t x;
157
+
memcpy(&x, b, 2);
158
+
return x;
159
+
}
160
+
161
+
inline static uint32_t Load32(uint8_t *b) {
162
+
uint32_t x;
163
+
memcpy(&x, b, 4);
164
+
return x;
165
+
}
166
+
167
+
inline static uint64_t Load64(uint8_t *b) {
168
+
uint64_t x;
169
+
memcpy(&x, b, 8);
170
+
return x;
171
+
}
172
+
173
+
inline static void Store16(uint8_t *b, uint16_t i) {
174
+
memcpy(b, &i, 2);
175
+
}
176
+
177
+
inline static void Store32(uint8_t *b, uint32_t i) {
178
+
memcpy(b, &i, 4);
179
+
}
180
+
181
+
inline static void Store64(uint8_t *b, uint64_t i) {
182
+
memcpy(b, &i, 8);
183
+
}
184
+
185
+
#define Load16Le(b) (le16toh(Load16(b)))
186
+
#define Store16Le(b, i) (Store16(b, htole16(i)))
187
+
#define Load16Be(b) (be16toh(Load16(b)))
188
+
#define Store16Be(b, i) (Store16(b, htobe16(i)))
189
+
190
+
#define Load32Le(b) (le32toh(Load32(b)))
191
+
#define Store32Le(b, i) (Store32(b, htole32(i)))
192
+
#define Load32Be(b) (be32toh(Load32(b)))
193
+
#define Store32Be(b, i) (Store32(b, htobe32(i)))
194
+
195
+
#define Load64Le(b) (le64toh(Load64(b)))
196
+
#define Store64Le(b, i) (Store64(b, htole64(i)))
197
+
#define Load64Be(b) (be64toh(Load64(b)))
198
+
#define Store64Be(b, i) (Store64(b, htobe64(i)))
199
+
200
+
201
+
#if defined(__cplusplus)
202
+
}
203
+
#endif
204
+
205
+
#endif
+17
c/FSR.ExternalAPI.fsti
+17
c/FSR.ExternalAPI.fsti
···
1
+
module FSR.ExternalAPI
2
+
3
+
open EverParse3d.Prelude
4
+
open EverParse3d.Actions.All
5
+
open EverParse3d.Interpreter
6
+
include FSR.ExternalTypes
7
+
8
+
noextract
9
+
val output_loc:eloc
10
+
11
+
12
+
val ___WireCtx:Type0
13
+
14
+
15
+
val ___WireSetU32BE (ctx: bpointer ((___WireCtx))) (idx: (___UINT32)) (v: (___UINT32BE))
16
+
: extern_action (unit) (NonTrivial output_loc)
17
+
c/FSR.ExternalAPI.fsti.checked
c/FSR.ExternalAPI.fsti.checked
This is a binary file and will not be displayed.
+8
c/FSR.ExternalTypes.fsti
+8
c/FSR.ExternalTypes.fsti
c/FSR.ExternalTypes.fsti.checked
c/FSR.ExternalTypes.fsti.checked
This is a binary file and will not be displayed.
+73
c/FSR.c
+73
c/FSR.c
···
1
+
2
+
3
+
#include "FSR.h"
4
+
5
+
#include "FSR_ExternalAPI.h"
6
+
7
+
uint64_t
8
+
FsrValidateFsr(
9
+
WIRECTX *Ctx,
10
+
uint8_t *Ctxt,
11
+
void
12
+
(*ErrorHandlerFn)(
13
+
EVERPARSE_STRING x0,
14
+
EVERPARSE_STRING x1,
15
+
EVERPARSE_STRING x2,
16
+
uint64_t x3,
17
+
uint8_t *x4,
18
+
uint8_t *x5,
19
+
uint64_t x6
20
+
),
21
+
uint8_t *Input,
22
+
uint64_t InputLength,
23
+
uint64_t StartPosition
24
+
)
25
+
{
26
+
/* Validating field __bitfield_0 */
27
+
/* Checking that we have enough space for a UINT32BE, i.e., 4 bytes */
28
+
BOOLEAN hasBytes = 4ULL <= (InputLength - StartPosition);
29
+
uint64_t positionAfterBitfield0;
30
+
if (hasBytes)
31
+
{
32
+
positionAfterBitfield0 = StartPosition + 4ULL;
33
+
}
34
+
else
35
+
{
36
+
positionAfterBitfield0 =
37
+
EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA,
38
+
StartPosition);
39
+
}
40
+
uint64_t positionAfterFsr;
41
+
if (EverParseIsError(positionAfterBitfield0))
42
+
{
43
+
positionAfterFsr = positionAfterBitfield0;
44
+
}
45
+
else
46
+
{
47
+
uint32_t bitfield0 = Load32Be(Input + (uint32_t)StartPosition);
48
+
WireSetU32be(Ctx, (uint32_t)0U, EverParseGetBitfield32MsbFirst(bitfield0, 0U, 1U));
49
+
WireSetU32be(Ctx, (uint32_t)1U, EverParseGetBitfield32MsbFirst(bitfield0, 1U, 4U));
50
+
WireSetU32be(Ctx, (uint32_t)2U, EverParseGetBitfield32MsbFirst(bitfield0, 4U, 5U));
51
+
WireSetU32be(Ctx, (uint32_t)3U, EverParseGetBitfield32MsbFirst(bitfield0, 5U, 6U));
52
+
WireSetU32be(Ctx, (uint32_t)4U, EverParseGetBitfield32MsbFirst(bitfield0, 6U, 7U));
53
+
WireSetU32be(Ctx, (uint32_t)5U, EverParseGetBitfield32MsbFirst(bitfield0, 7U, 8U));
54
+
WireSetU32be(Ctx, (uint32_t)6U, EverParseGetBitfield32MsbFirst(bitfield0, 8U, 24U));
55
+
WireSetU32be(Ctx, (uint32_t)7U, EverParseGetBitfield32MsbFirst(bitfield0, 24U, 32U));
56
+
BOOLEAN actionResult = TRUE;
57
+
KRML_MAYBE_UNUSED_VAR(actionResult);
58
+
positionAfterFsr = positionAfterBitfield0;
59
+
}
60
+
if (EverParseIsSuccess(positionAfterFsr))
61
+
{
62
+
return positionAfterFsr;
63
+
}
64
+
ErrorHandlerFn("_FSR",
65
+
"__bitfield_0",
66
+
EverParseErrorReasonOfResult(positionAfterFsr),
67
+
EverParseGetValidatorErrorKind(positionAfterFsr),
68
+
Ctxt,
69
+
Input,
70
+
StartPosition);
71
+
return positionAfterFsr;
72
+
}
73
+
+144
c/FSR.fst
+144
c/FSR.fst
···
1
+
module FSR
2
+
open EverParse3d.Prelude
3
+
open EverParse3d.Actions.All
4
+
open EverParse3d.Interpreter
5
+
open FSR.ExternalAPI
6
+
module T = FStar.Tactics
7
+
module A = EverParse3d.Actions.All
8
+
module P = EverParse3d.Prelude
9
+
#set-options "--fuel 0 --ifuel 0 --ext optimize_let_vc"
10
+
11
+
[@@ specialize; noextract_to "krml"]
12
+
noextract
13
+
let def__FSR (ctx: bpointer ((___WireCtx))) =
14
+
((T_drop
15
+
(T_with_comment "__bitfield_0"
16
+
(T_with_dep_action "__bitfield_0"
17
+
(DT_IType UInt32BE)
18
+
(fun _ __bitfield_0 ->
19
+
(Action_act
20
+
(Action_seq
21
+
(Action_call
22
+
(mk_action_binding (___WireSetU32BE ctx
23
+
(EverParse3d.Prelude.uint8_to_uint32 0uy)
24
+
(get_bitfield32_msb_first __bitfield_0 0ul 1ul))))
25
+
(Action_seq
26
+
(Action_call
27
+
(mk_action_binding (___WireSetU32BE ctx
28
+
(EverParse3d.Prelude.uint8_to_uint32 1uy)
29
+
(get_bitfield32_msb_first __bitfield_0 1ul 4ul))))
30
+
(Action_seq
31
+
(Action_call
32
+
(mk_action_binding (___WireSetU32BE ctx
33
+
(EverParse3d.Prelude.uint8_to_uint32 2uy)
34
+
(get_bitfield32_msb_first __bitfield_0 4ul 5ul))))
35
+
(Action_seq
36
+
(Action_call
37
+
(mk_action_binding (___WireSetU32BE ctx
38
+
(EverParse3d.Prelude.uint8_to_uint32 3uy)
39
+
(get_bitfield32_msb_first __bitfield_0 5ul 6ul))))
40
+
(Action_seq
41
+
(Action_call
42
+
(mk_action_binding (___WireSetU32BE ctx
43
+
(EverParse3d.Prelude.uint8_to_uint32 4uy)
44
+
(get_bitfield32_msb_first __bitfield_0 6ul 7ul))))
45
+
(Action_seq
46
+
(Action_call
47
+
(mk_action_binding (___WireSetU32BE ctx
48
+
(EverParse3d.Prelude.uint8_to_uint32 5uy)
49
+
(get_bitfield32_msb_first __bitfield_0 7ul 8ul
50
+
))))
51
+
(Action_seq
52
+
(Action_call
53
+
(mk_action_binding (___WireSetU32BE ctx
54
+
(EverParse3d.Prelude.uint8_to_uint32 6uy)
55
+
(get_bitfield32_msb_first __bitfield_0
56
+
8ul
57
+
24ul))))
58
+
(Atomic_action
59
+
(Action_call
60
+
(mk_action_binding (___WireSetU32BE ctx
61
+
(EverParse3d.Prelude.uint8_to_uint32 7uy
62
+
)
63
+
(get_bitfield32_msb_first __bitfield_0
64
+
24ul
65
+
32ul)))))))))))))))
66
+
"Validating field __bitfield_0"))
67
+
<:
68
+
Tot (typ _ _ _ _ _ _)
69
+
by
70
+
(T.norm [delta_attr [`%specialize]; zeta; iota; primops];
71
+
T.smt ()))
72
+
73
+
[@@ noextract_to "krml"]
74
+
inline_for_extraction noextract
75
+
let kind__FSR:P.parser_kind true WeakKindStrongPrefix =
76
+
coerce (FStar.Tactics.Effect.synth_by_tactic (fun _ ->
77
+
(T.norm [delta_only [`%weak_kind_glb]; zeta; iota; primops];
78
+
T.trefl ())))
79
+
kind____UINT32BE
80
+
81
+
[@@ specialize; noextract_to "krml"]
82
+
noextract
83
+
let def'__FSR (ctx: bpointer ((___WireCtx)))
84
+
: typ kind__FSR
85
+
Trivial
86
+
Trivial
87
+
(NonTrivial
88
+
(A.eloc_union output_loc
89
+
(A.eloc_union output_loc
90
+
(A.eloc_union output_loc
91
+
(A.eloc_union output_loc
92
+
(A.eloc_union output_loc
93
+
(A.eloc_union output_loc (A.eloc_union output_loc output_loc))))))))
94
+
true
95
+
false =
96
+
coerce (FStar.Tactics.Effect.synth_by_tactic (fun _ -> (coerce_validator [`%kind__FSR])))
97
+
(def__FSR ctx)
98
+
99
+
[@@ noextract_to "krml"]
100
+
noextract
101
+
let type__FSR (ctx: bpointer ((___WireCtx))) = (as_type (def'__FSR ctx))
102
+
103
+
[@@ noextract_to "krml"]
104
+
noextract
105
+
let parser__FSR (ctx: bpointer ((___WireCtx))) = (as_parser (def'__FSR ctx))
106
+
[@@ normalize_for_extraction specialization_steps]
107
+
let validate__FSR (ctx: bpointer ((___WireCtx))) = as_validator "_FSR" (def'__FSR ctx)
108
+
109
+
[@@ specialize; noextract_to "krml"]
110
+
noextract
111
+
let dtyp__FSR (ctx: bpointer ((___WireCtx)))
112
+
: dtyp kind__FSR
113
+
true
114
+
false
115
+
Trivial
116
+
Trivial
117
+
(NonTrivial
118
+
(A.eloc_union output_loc
119
+
(A.eloc_union output_loc
120
+
(A.eloc_union output_loc
121
+
(A.eloc_union output_loc
122
+
(A.eloc_union output_loc
123
+
(A.eloc_union output_loc (A.eloc_union output_loc output_loc)))))))) =
124
+
mk_dtyp_app kind__FSR Trivial Trivial
125
+
(NonTrivial
126
+
(A.eloc_union output_loc
127
+
(A.eloc_union output_loc
128
+
(A.eloc_union output_loc
129
+
(A.eloc_union output_loc
130
+
(A.eloc_union output_loc
131
+
(A.eloc_union output_loc (A.eloc_union output_loc output_loc))))))))
132
+
(type__FSR ctx)
133
+
(coerce (FStar.Tactics.Effect.synth_by_tactic (fun _ ->
134
+
(T.norm [delta_only [`%type__FSR]];
135
+
T.trefl ())))
136
+
(parser__FSR ctx)) None true false
137
+
(coerce (FStar.Tactics.Effect.synth_by_tactic (fun _ ->
138
+
(T.norm [delta_only [`%parser__FSR; `%type__FSR; `%coerce]];
139
+
T.trefl ())))
140
+
(validate__FSR ctx))
141
+
(FStar.Tactics.Effect.synth_by_tactic (fun _ ->
142
+
(T.norm [delta_only [`%Some?]; iota];
143
+
T.trefl ())))
144
+
c/FSR.fst.checked
c/FSR.fst.checked
This is a binary file and will not be displayed.
+36
c/FSR.fsti
+36
c/FSR.fsti
···
1
+
module FSR
2
+
open EverParse3d.Prelude
3
+
open EverParse3d.Actions.All
4
+
open EverParse3d.Interpreter
5
+
open FSR.ExternalAPI
6
+
module T = FStar.Tactics
7
+
module A = EverParse3d.Actions.All
8
+
module P = EverParse3d.Prelude
9
+
#set-options "--fuel 0 --ifuel 0 --ext optimize_let_vc"
10
+
11
+
[@@ noextract_to "krml"]
12
+
inline_for_extraction noextract
13
+
val kind__FSR:P.parser_kind true P.WeakKindStrongPrefix
14
+
15
+
[@@ noextract_to "krml"]
16
+
noextract
17
+
val def'__FSR (ctx: bpointer ((___WireCtx)))
18
+
: typ kind__FSR
19
+
Trivial
20
+
Trivial
21
+
(NonTrivial
22
+
(A.eloc_union output_loc
23
+
(A.eloc_union output_loc
24
+
(A.eloc_union output_loc
25
+
(A.eloc_union output_loc
26
+
(A.eloc_union output_loc
27
+
(A.eloc_union output_loc (A.eloc_union output_loc output_loc))))))))
28
+
true
29
+
false
30
+
31
+
val validate__FSR (ctx: bpointer ((___WireCtx))) : validator_of (def'__FSR ctx)
32
+
33
+
[@@ specialize; noextract_to "krml"]
34
+
noextract
35
+
val dtyp__FSR (ctx: bpointer ((___WireCtx))) : dtyp_of (def'__FSR ctx)
36
+
c/FSR.fsti.checked
c/FSR.fsti.checked
This is a binary file and will not be displayed.
+37
c/FSR.h
+37
c/FSR.h
···
1
+
2
+
3
+
#ifndef FSR_H
4
+
#define FSR_H
5
+
6
+
#if defined(__cplusplus)
7
+
extern "C" {
8
+
#endif
9
+
10
+
#include "EverParse.h"
11
+
#include "FSR_ExternalTypedefs.h"
12
+
13
+
uint64_t
14
+
FsrValidateFsr(
15
+
WIRECTX *Ctx,
16
+
uint8_t *Ctxt,
17
+
void
18
+
(*ErrorHandlerFn)(
19
+
EVERPARSE_STRING x0,
20
+
EVERPARSE_STRING x1,
21
+
EVERPARSE_STRING x2,
22
+
uint64_t x3,
23
+
uint8_t *x4,
24
+
uint8_t *x5,
25
+
uint64_t x6
26
+
),
27
+
uint8_t *Input,
28
+
uint64_t InputLength,
29
+
uint64_t StartPosition
30
+
);
31
+
32
+
#if defined(__cplusplus)
33
+
}
34
+
#endif
35
+
36
+
#define FSR_H_DEFINED
37
+
#endif /* FSR_H */
c/FSR.krml
c/FSR.krml
This is a binary file and will not be displayed.
+41
c/FSRWrapper.c
+41
c/FSRWrapper.c
···
1
+
#include "FSRWrapper.h"
2
+
#include "EverParse.h"
3
+
#include "FSR.h"
4
+
void FSREverParseError(const char *StructName, const char *FieldName, const char *Reason);
5
+
6
+
static
7
+
void DefaultErrorHandler(
8
+
const char *typename_s,
9
+
const char *fieldname,
10
+
const char *reason,
11
+
uint64_t error_code,
12
+
uint8_t *context,
13
+
EVERPARSE_INPUT_BUFFER input,
14
+
uint64_t start_pos)
15
+
{
16
+
EVERPARSE_ERROR_FRAME *frame = (EVERPARSE_ERROR_FRAME*)context;
17
+
EverParseDefaultErrorHandler(
18
+
typename_s,
19
+
fieldname,
20
+
reason,
21
+
error_code,
22
+
frame,
23
+
input,
24
+
start_pos
25
+
);
26
+
}
27
+
28
+
BOOLEAN FsrCheckFsr(WIRECTX* ctx, uint8_t *base, uint32_t len) {
29
+
EVERPARSE_ERROR_FRAME frame;
30
+
frame.filled = FALSE;
31
+
uint64_t result = FsrValidateFsr(ctx, (uint8_t*)&frame, &DefaultErrorHandler, base, len, 0);
32
+
if (EverParseIsError(result))
33
+
{
34
+
if (frame.filled)
35
+
{
36
+
FSREverParseError(frame.typename_s, frame.fieldname, frame.reason);
37
+
}
38
+
return FALSE;
39
+
}
40
+
return TRUE;
41
+
}
+26
c/FSRWrapper.h
+26
c/FSRWrapper.h
···
1
+
#include "EverParseEndianness.h"
2
+
#define EVERPARSE_SUCCESS 0ul
3
+
#define EVERPARSE_ERROR_GENERIC 1uL
4
+
#define EVERPARSE_ERROR_NOT_ENOUGH_DATA 2uL
5
+
#define EVERPARSE_ERROR_IMPOSSIBLE 3uL
6
+
#define EVERPARSE_ERROR_LIST_SIZE_NOT_MULTIPLE 4uL
7
+
#define EVERPARSE_ERROR_ACTION_FAILED 5uL
8
+
#define EVERPARSE_ERROR_CONSTRAINT_FAILED 6uL
9
+
#define EVERPARSE_ERROR_UNEXPECTED_PADDING 7uL
10
+
// Probe wrapper error codes
11
+
#define EVERPARSE_PROBE_FAILURE_INCORRECT_SIZE 256uL
12
+
#define EVERPARSE_PROBE_FAILURE_INIT 257uL
13
+
#define EVERPARSE_PROBE_FAILURE_PROBE 258uL
14
+
#define EVERPARSE_PROBE_FAILURE_VALIDATION 259uL
15
+
16
+
17
+
#include "FSR_ExternalTypedefs.h"
18
+
19
+
20
+
#ifdef __cplusplus
21
+
extern "C" {
22
+
#endif
23
+
BOOLEAN FsrCheckFsr(WIRECTX* ctx, uint8_t *base, uint32_t len);
24
+
#ifdef __cplusplus
25
+
}
26
+
#endif
+20
c/FSR_ExternalAPI.h
+20
c/FSR_ExternalAPI.h
···
1
+
2
+
3
+
#ifndef FSR_ExternalAPI_H
4
+
#define FSR_ExternalAPI_H
5
+
6
+
#if defined(__cplusplus)
7
+
extern "C" {
8
+
#endif
9
+
10
+
#include "EverParse.h"
11
+
#include "FSR_ExternalTypedefs.h"
12
+
13
+
extern void WireSetU32be(WIRECTX *ctx, uint32_t idx, uint32_t v);
14
+
15
+
#if defined(__cplusplus)
16
+
}
17
+
#endif
18
+
19
+
#define FSR_ExternalAPI_H_DEFINED
20
+
#endif /* FSR_ExternalAPI_H */
c/FSR_ExternalAPI.krml
c/FSR_ExternalAPI.krml
This is a binary file and will not be displayed.
+5
c/FSR_ExternalTypedefs.h
+5
c/FSR_ExternalTypedefs.h
c/FSR_ExternalTypes.krml
c/FSR_ExternalTypes.krml
This is a binary file and will not be displayed.
+56
c/Makefile.basic
+56
c/Makefile.basic
···
1
+
# A basic Makefile that KaRaMeL copies in the output directory; this is not
2
+
# guaranteed to work and will only work well for very simple projects. This
3
+
# Makefile uses:
4
+
# - the custom C files passed to your krml invocation
5
+
# - the custom C flags passed to your krml invocation
6
+
# - the -o option passed to your krml invocation
7
+
8
+
include Makefile.include
9
+
10
+
ifeq (,$(KRML_HOME))
11
+
$(error please define KRML_HOME to point to the root of your KaRaMeL git checkout)
12
+
endif
13
+
14
+
CFLAGS += -I. -I $(KRML_HOME)/include -I $(KRML_HOME)/krmllib/dist/minimal
15
+
CFLAGS += -Wall -Wextra -Werror -std=c11 \
16
+
-Wno-unknown-warning-option \
17
+
-Wno-infinite-recursion \
18
+
-g -fwrapv -D_BSD_SOURCE -D_DEFAULT_SOURCE
19
+
ifeq ($(OS),Windows_NT)
20
+
CFLAGS += -D__USE_MINGW_ANSI_STDIO
21
+
else
22
+
CFLAGS += -fPIC
23
+
endif
24
+
CFLAGS += $(USER_CFLAGS)
25
+
26
+
SOURCES += $(ALL_C_FILES) $(USER_C_FILES)
27
+
ifneq (,$(BLACKLIST))
28
+
SOURCES := $(filter-out $(BLACKLIST),$(SOURCES))
29
+
endif
30
+
OBJS += $(patsubst %.c,%.o,$(SOURCES))
31
+
32
+
all: $(USER_TARGET)
33
+
34
+
$(USER_TARGET): $(OBJS)
35
+
36
+
AR ?= ar
37
+
38
+
%.a:
39
+
$(AR) cr $@ $^
40
+
41
+
%.exe:
42
+
$(CC) $(CFLAGS) -o $@ $^ $(KRML_HOME)/krmllib/dist/generic/libkrmllib.a
43
+
44
+
%.so:
45
+
$(CC) $(CFLAGS) -shared -o $@ $^
46
+
47
+
%.d: %.c
48
+
@set -e; rm -f $@; \
49
+
$(CC) -MM -MG $(CFLAGS) $< > $@.$$$$; \
50
+
sed 's,\($(notdir $*)\)\.o[ :]*,$(dir $@)\1.o $@ : ,g' < $@.$$$$ > $@; \
51
+
rm -f $@.$$$$
52
+
53
+
include $(patsubst %.c,%.d,$(SOURCES))
54
+
55
+
clean:
56
+
rm -rf *.o *.d $(USER_TARGET)
+5
c/Makefile.include
+5
c/Makefile.include
+7
-3
c/dune.inc
+7
-3
c/dune.inc
···
9
9
(rule
10
10
(alias gen)
11
11
(mode fallback)
12
-
(targets EverParse.h EverParseEndianness.h FSR.h FSR.c test.c)
12
+
(targets EverParse.h EverParseEndianness.h FSR.h FSR.c FSR_ExternalTypedefs.h FSR_ExternalAPI.h FSRWrapper.c FSRWrapper.h test.c)
13
13
(deps gen.exe FSR.3d)
14
14
(action
15
15
(run ./gen.exe c)))
16
16
17
17
(rule
18
18
(alias runtest)
19
-
(deps test.c EverParse.h EverParseEndianness.h FSR.h FSR.c)
19
+
(deps test.c EverParse.h EverParseEndianness.h FSR.h FSR.c FSR_ExternalTypedefs.h FSR_ExternalAPI.h FSRWrapper.c FSRWrapper.h)
20
20
(action
21
21
(system
22
-
"cc -std=c11 -Wall -Wextra -Werror -o test_fsr test.c FSR.c && ./test_fsr")))
22
+
"cc -std=c11 -Wall -Wextra -Werror -o test_fsr test.c FSR.c FSRWrapper.c && ./test_fsr")))
23
23
24
24
(install
25
25
(package fsr)
···
28
28
(FSR.3d as c/FSR.3d)
29
29
(FSR.h as c/FSR.h)
30
30
(FSR.c as c/FSR.c)
31
+
(FSR_ExternalTypedefs.h as c/FSR_ExternalTypedefs.h)
32
+
(FSR_ExternalAPI.h as c/FSR_ExternalAPI.h)
33
+
(FSRWrapper.c as c/FSRWrapper.c)
34
+
(FSRWrapper.h as c/FSRWrapper.h)
31
35
(EverParse.h as c/EverParse.h)
32
36
(EverParseEndianness.h as c/EverParseEndianness.h)))
+202
c/krmlargs005278.rsp
+202
c/krmlargs005278.rsp
···
1
+
-tmpdir
2
+
.
3
+
-skip-compilation
4
+
-static-header
5
+
LowParse.Low.Base,EverParse3d.Prelude.StaticHeader,EverParse3d.ErrorCode,EverParse3d.CopyBuffer,EverParse3d.InputStream.\*
6
+
-no-prefix
7
+
LowParse.Slice
8
+
-no-prefix
9
+
LowParse.Low.BoundedInt
10
+
-library
11
+
Prims,LowParse.\*,EverParse3d.\*
12
+
-warn-error
13
+
-9@4-20
14
+
-fnoreturn-else
15
+
-fparentheses
16
+
-fcurly-braces
17
+
-fmicrosoft
18
+
-fno-shadow
19
+
-header
20
+
/Users/samoht/.local/everparse/bin/../src/3d/noheader.txt
21
+
-minimal
22
+
-add-include
23
+
"EverParse.h"
24
+
-fextern-c
25
+
-library
26
+
FSR.ExternalAPI
27
+
-no-prefix
28
+
FSR.ExternalTypes
29
+
-no-prefix
30
+
FSR.ExternalAPI
31
+
-add-include
32
+
"FSR_ExternalTypedefs.h"
33
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_BV.krml
34
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1_Derived_Lemmas.krml
35
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Kinds.krml
36
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Builtins.krml
37
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_Combinators.krml
38
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_ListUpTo.krml
39
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_Base.krml
40
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/Spec_Loops.krml
41
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Actions_Common.krml
42
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Monotonic_Witnessed.krml
43
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Prelude_StaticHeader.krml
44
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_FLData.krml
45
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_CLens.krml
46
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Int8.krml
47
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_ST.krml
48
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_Monotonic_Buffer.krml
49
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Pprint.krml
50
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Derived_Lemmas.krml
51
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1_Derived.krml
52
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_UInt128.krml
53
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_FLData.krml
54
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Int_Cast.krml
55
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_List_Tot_Properties.krml
56
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Endianness_BitFields.krml
57
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_Endianness.krml
58
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1.krml
59
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_Endianness.krml
60
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Math_Lemmas.krml
61
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Int16.krml
62
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1_Builtins.krml
63
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_ModifiesGen.krml
64
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_HyperStack.krml
65
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_DER.krml
66
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_Modifies.krml
67
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Actions_BackendFlag.krml
68
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Actions_All.krml
69
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Seq_Properties.krml
70
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_TypeChecker_Core.krml
71
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Set.krml
72
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Range.krml
73
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Endianness.krml
74
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_StrongExcludedMiddle.krml
75
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_TermEq_Simple.krml
76
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Util.krml
77
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_UInt.krml
78
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_List_Tot.krml
79
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Collect.krml
80
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Classical.krml
81
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_Failure.krml
82
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_BoundedInt.krml
83
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_UInt16.krml
84
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Norm.krml
85
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_BCVLI.krml
86
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_String.krml
87
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Heap.krml
88
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Issue.krml
89
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Tactics_V1_Builtins.krml
90
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Tactics_Types_Reflection.krml
91
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_ListUpTo.krml
92
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Data.krml
93
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_Seq.krml
94
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Monotonic_HyperStack.krml
95
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Bytes.krml
96
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Tactics_Common.krml
97
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_IndefiniteDescription.krml
98
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Compare.krml
99
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Tactics_V2_Builtins.krml
100
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_PropositionalExtensionality.krml
101
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_InputStream_All.krml
102
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_HyperStack_ST.krml
103
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_Base_Spec.krml
104
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_Int.krml
105
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_Base.krml
106
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_SeqBytes_Base.krml
107
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_AllIntegers.krml
108
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_BigOps.krml
109
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_List.krml
110
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1_Formula.krml
111
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_VConfig.krml
112
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_GSet.krml
113
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Char.krml
114
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_BitVector.krml
115
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Monotonic_Heap.krml
116
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Arith.krml
117
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Sealed.krml
118
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_BitFields.krml
119
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Int64.krml
120
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Prelude.krml
121
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Attributes.krml
122
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_ErrorCode.krml
123
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Syntax_Syntax.krml
124
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_Types.krml
125
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Actions_Base.krml
126
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_NormSteps.krml
127
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Tactics_Unseal.krml
128
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Tactics_Types.krml
129
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Seq_Base.krml
130
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_UInt8.krml
131
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_Buffer.krml
132
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Float.krml
133
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Errors_Msg.krml
134
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_List_Tot_Base.krml
135
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_List.krml
136
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_Int.krml
137
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_All.krml
138
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_PredicateExtensionality.krml
139
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1_Compare.krml
140
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_BufferOps.krml
141
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1_Data.krml
142
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_Bytes.krml
143
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Formula.krml
144
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Universe.krml
145
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Map.krml
146
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Exn.krml
147
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Actions_BackendFlagValue.krml
148
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Calc.krml
149
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Int32.krml
150
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Math.krml
151
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_ProbeActions.krml
152
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Slice.krml
153
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Mul.krml
154
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Squash.krml
155
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Bytes.krml
156
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_AppCtxt.krml
157
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Ghost.krml
158
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Endianness.krml
159
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Readable.krml
160
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_BoundedInt.krml
161
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_ErasedLogic.krml
162
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_Combinators.krml
163
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Pervasives.krml
164
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_InputStream_Buffer_Aux.krml
165
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_InputStream_Base.krml
166
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_VLGen.krml
167
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Derived.krml
168
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Prelude.krml
169
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_InputStream_Buffer.krml
170
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_Fuel.krml
171
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_Const.krml
172
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_TSet.krml
173
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_CopyBuffer.krml
174
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_UInt32.krml
175
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/C_Loops.krml
176
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2.krml
177
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_FunctionalExtensionality.krml
178
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_Comment.krml
179
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Monotonic_HyperHeap.krml
180
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Seq.krml
181
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Order.krml
182
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_TermEq.krml
183
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_UInt64.krml
184
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Sealed_Inhabited.krml
185
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Pervasives_Native.krml
186
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_ErrorCode.krml
187
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Monotonic_Pure.krml
188
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Int.krml
189
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_InputBuffer.krml
190
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Classical_Sugar.krml
191
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Bytes32.krml
192
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Preorder.krml
193
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_VLData.krml
194
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Math_Lib.krml
195
+
./FSR.krml
196
+
./FSR_ExternalAPI.krml
197
+
./FSR_ExternalTypes.krml
198
+
FSRWrapper.c
199
+
-bundle
200
+
FStar.\*,LowStar.\*,C.\*[rename=Lib,rename-prefix]
201
+
-bundle
202
+
Prims,LowParse.\*,EverParse3d.\*[rename=EverParse,rename-prefix]
+202
c/krmlargs16f352.rsp
+202
c/krmlargs16f352.rsp
···
1
+
-tmpdir
2
+
.
3
+
-skip-compilation
4
+
-static-header
5
+
LowParse.Low.Base,EverParse3d.Prelude.StaticHeader,EverParse3d.ErrorCode,EverParse3d.CopyBuffer,EverParse3d.InputStream.\*
6
+
-no-prefix
7
+
LowParse.Slice
8
+
-no-prefix
9
+
LowParse.Low.BoundedInt
10
+
-library
11
+
Prims,LowParse.\*,EverParse3d.\*
12
+
-warn-error
13
+
-9@4-20
14
+
-fnoreturn-else
15
+
-fparentheses
16
+
-fcurly-braces
17
+
-fmicrosoft
18
+
-fno-shadow
19
+
-header
20
+
/Users/samoht/.local/everparse/bin/../src/3d/noheader.txt
21
+
-minimal
22
+
-add-include
23
+
"EverParse.h"
24
+
-fextern-c
25
+
-library
26
+
FSR.ExternalAPI
27
+
-no-prefix
28
+
FSR.ExternalTypes
29
+
-no-prefix
30
+
FSR.ExternalAPI
31
+
-add-include
32
+
"FSR_ExternalTypedefs.h"
33
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_BV.krml
34
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1_Derived_Lemmas.krml
35
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Kinds.krml
36
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Builtins.krml
37
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_Combinators.krml
38
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_ListUpTo.krml
39
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_Base.krml
40
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/Spec_Loops.krml
41
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Actions_Common.krml
42
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Monotonic_Witnessed.krml
43
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Prelude_StaticHeader.krml
44
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_FLData.krml
45
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_CLens.krml
46
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Int8.krml
47
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_ST.krml
48
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_Monotonic_Buffer.krml
49
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Pprint.krml
50
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Derived_Lemmas.krml
51
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1_Derived.krml
52
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_UInt128.krml
53
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_FLData.krml
54
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Int_Cast.krml
55
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_List_Tot_Properties.krml
56
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Endianness_BitFields.krml
57
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_Endianness.krml
58
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1.krml
59
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_Endianness.krml
60
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Math_Lemmas.krml
61
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Int16.krml
62
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1_Builtins.krml
63
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_ModifiesGen.krml
64
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_HyperStack.krml
65
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_DER.krml
66
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_Modifies.krml
67
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Actions_BackendFlag.krml
68
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Actions_All.krml
69
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Seq_Properties.krml
70
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_TypeChecker_Core.krml
71
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Set.krml
72
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Range.krml
73
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Endianness.krml
74
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_StrongExcludedMiddle.krml
75
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_TermEq_Simple.krml
76
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Util.krml
77
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_UInt.krml
78
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_List_Tot.krml
79
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Collect.krml
80
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Classical.krml
81
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_Failure.krml
82
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_BoundedInt.krml
83
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_UInt16.krml
84
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Norm.krml
85
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_BCVLI.krml
86
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_String.krml
87
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Heap.krml
88
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Issue.krml
89
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Tactics_V1_Builtins.krml
90
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Tactics_Types_Reflection.krml
91
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_ListUpTo.krml
92
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Data.krml
93
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_Seq.krml
94
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Monotonic_HyperStack.krml
95
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Bytes.krml
96
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Tactics_Common.krml
97
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_IndefiniteDescription.krml
98
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Compare.krml
99
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Tactics_V2_Builtins.krml
100
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_PropositionalExtensionality.krml
101
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_InputStream_All.krml
102
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_HyperStack_ST.krml
103
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_Base_Spec.krml
104
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_Int.krml
105
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_Base.krml
106
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_SeqBytes_Base.krml
107
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_AllIntegers.krml
108
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_BigOps.krml
109
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_List.krml
110
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1_Formula.krml
111
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_VConfig.krml
112
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_GSet.krml
113
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Char.krml
114
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_BitVector.krml
115
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Monotonic_Heap.krml
116
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Arith.krml
117
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Sealed.krml
118
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_BitFields.krml
119
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Int64.krml
120
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Prelude.krml
121
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Attributes.krml
122
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_ErrorCode.krml
123
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Syntax_Syntax.krml
124
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_Types.krml
125
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Actions_Base.krml
126
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_NormSteps.krml
127
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Tactics_Unseal.krml
128
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Tactics_Types.krml
129
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Seq_Base.krml
130
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_UInt8.krml
131
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_Buffer.krml
132
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Float.krml
133
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Errors_Msg.krml
134
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_List_Tot_Base.krml
135
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_List.krml
136
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_Int.krml
137
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_All.krml
138
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_PredicateExtensionality.krml
139
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1_Compare.krml
140
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_BufferOps.krml
141
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1_Data.krml
142
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_Bytes.krml
143
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Formula.krml
144
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Universe.krml
145
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Map.krml
146
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Exn.krml
147
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Actions_BackendFlagValue.krml
148
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Calc.krml
149
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Int32.krml
150
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Math.krml
151
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_ProbeActions.krml
152
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Slice.krml
153
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Mul.krml
154
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Squash.krml
155
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Bytes.krml
156
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_AppCtxt.krml
157
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Ghost.krml
158
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Endianness.krml
159
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Readable.krml
160
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_BoundedInt.krml
161
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_ErasedLogic.krml
162
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_Combinators.krml
163
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Pervasives.krml
164
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_InputStream_Buffer_Aux.krml
165
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_InputStream_Base.krml
166
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_VLGen.krml
167
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Derived.krml
168
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Prelude.krml
169
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_InputStream_Buffer.krml
170
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_Fuel.krml
171
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_Const.krml
172
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_TSet.krml
173
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_CopyBuffer.krml
174
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_UInt32.krml
175
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/C_Loops.krml
176
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2.krml
177
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_FunctionalExtensionality.krml
178
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_Comment.krml
179
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Monotonic_HyperHeap.krml
180
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Seq.krml
181
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Order.krml
182
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_TermEq.krml
183
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_UInt64.krml
184
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Sealed_Inhabited.krml
185
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Pervasives_Native.krml
186
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_ErrorCode.krml
187
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Monotonic_Pure.krml
188
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Int.krml
189
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_InputBuffer.krml
190
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Classical_Sugar.krml
191
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Bytes32.krml
192
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Preorder.krml
193
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_VLData.krml
194
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Math_Lib.krml
195
+
./FSR.krml
196
+
./FSR_ExternalAPI.krml
197
+
./FSR_ExternalTypes.krml
198
+
FSRWrapper.c
199
+
-bundle
200
+
FStar.\*,LowStar.\*,C.\*[rename=Lib,rename-prefix]
201
+
-bundle
202
+
Prims,LowParse.\*,EverParse3d.\*[rename=EverParse,rename-prefix]
+202
c/krmlargs3c1e1e.rsp
+202
c/krmlargs3c1e1e.rsp
···
1
+
-tmpdir
2
+
.
3
+
-skip-compilation
4
+
-static-header
5
+
LowParse.Low.Base,EverParse3d.Prelude.StaticHeader,EverParse3d.ErrorCode,EverParse3d.CopyBuffer,EverParse3d.InputStream.\*
6
+
-no-prefix
7
+
LowParse.Slice
8
+
-no-prefix
9
+
LowParse.Low.BoundedInt
10
+
-library
11
+
Prims,LowParse.\*,EverParse3d.\*
12
+
-warn-error
13
+
-9@4-20
14
+
-fnoreturn-else
15
+
-fparentheses
16
+
-fcurly-braces
17
+
-fmicrosoft
18
+
-fno-shadow
19
+
-header
20
+
/Users/samoht/.local/everparse/bin/../src/3d/noheader.txt
21
+
-minimal
22
+
-add-include
23
+
"EverParse.h"
24
+
-fextern-c
25
+
-library
26
+
FSR.ExternalAPI
27
+
-no-prefix
28
+
FSR.ExternalTypes
29
+
-no-prefix
30
+
FSR.ExternalAPI
31
+
-add-include
32
+
"FSR_ExternalTypedefs.h"
33
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_BV.krml
34
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1_Derived_Lemmas.krml
35
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Kinds.krml
36
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Builtins.krml
37
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_Combinators.krml
38
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_ListUpTo.krml
39
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_Base.krml
40
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/Spec_Loops.krml
41
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Actions_Common.krml
42
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Monotonic_Witnessed.krml
43
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Prelude_StaticHeader.krml
44
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_FLData.krml
45
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_CLens.krml
46
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Int8.krml
47
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_ST.krml
48
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_Monotonic_Buffer.krml
49
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Pprint.krml
50
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Derived_Lemmas.krml
51
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1_Derived.krml
52
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_UInt128.krml
53
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_FLData.krml
54
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Int_Cast.krml
55
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_List_Tot_Properties.krml
56
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Endianness_BitFields.krml
57
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_Endianness.krml
58
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1.krml
59
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_Endianness.krml
60
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Math_Lemmas.krml
61
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Int16.krml
62
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1_Builtins.krml
63
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_ModifiesGen.krml
64
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_HyperStack.krml
65
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_DER.krml
66
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_Modifies.krml
67
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Actions_BackendFlag.krml
68
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Actions_All.krml
69
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Seq_Properties.krml
70
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_TypeChecker_Core.krml
71
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Set.krml
72
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Range.krml
73
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Endianness.krml
74
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_StrongExcludedMiddle.krml
75
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_TermEq_Simple.krml
76
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Util.krml
77
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_UInt.krml
78
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_List_Tot.krml
79
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Collect.krml
80
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Classical.krml
81
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_Failure.krml
82
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_BoundedInt.krml
83
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_UInt16.krml
84
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Norm.krml
85
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_BCVLI.krml
86
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_String.krml
87
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Heap.krml
88
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Issue.krml
89
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Tactics_V1_Builtins.krml
90
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Tactics_Types_Reflection.krml
91
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_ListUpTo.krml
92
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Data.krml
93
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_Seq.krml
94
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Monotonic_HyperStack.krml
95
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Bytes.krml
96
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Tactics_Common.krml
97
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_IndefiniteDescription.krml
98
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Compare.krml
99
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Tactics_V2_Builtins.krml
100
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_PropositionalExtensionality.krml
101
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_InputStream_All.krml
102
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_HyperStack_ST.krml
103
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_Base_Spec.krml
104
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_Int.krml
105
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_Base.krml
106
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_SeqBytes_Base.krml
107
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_AllIntegers.krml
108
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_BigOps.krml
109
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_List.krml
110
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1_Formula.krml
111
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_VConfig.krml
112
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_GSet.krml
113
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Char.krml
114
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_BitVector.krml
115
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Monotonic_Heap.krml
116
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Arith.krml
117
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Sealed.krml
118
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_BitFields.krml
119
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Int64.krml
120
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Prelude.krml
121
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Attributes.krml
122
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_ErrorCode.krml
123
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Syntax_Syntax.krml
124
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_Types.krml
125
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Actions_Base.krml
126
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_NormSteps.krml
127
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Tactics_Unseal.krml
128
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Tactics_Types.krml
129
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Seq_Base.krml
130
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_UInt8.krml
131
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_Buffer.krml
132
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Float.krml
133
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Errors_Msg.krml
134
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_List_Tot_Base.krml
135
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_List.krml
136
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_Int.krml
137
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_All.krml
138
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_PredicateExtensionality.krml
139
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1_Compare.krml
140
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_BufferOps.krml
141
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1_Data.krml
142
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_Bytes.krml
143
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Formula.krml
144
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Universe.krml
145
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Map.krml
146
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Exn.krml
147
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Actions_BackendFlagValue.krml
148
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Calc.krml
149
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Int32.krml
150
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Math.krml
151
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_ProbeActions.krml
152
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Slice.krml
153
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Mul.krml
154
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Squash.krml
155
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Bytes.krml
156
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_AppCtxt.krml
157
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Ghost.krml
158
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Endianness.krml
159
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Readable.krml
160
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_BoundedInt.krml
161
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_ErasedLogic.krml
162
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_Combinators.krml
163
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Pervasives.krml
164
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_InputStream_Buffer_Aux.krml
165
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_InputStream_Base.krml
166
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_VLGen.krml
167
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Derived.krml
168
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Prelude.krml
169
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_InputStream_Buffer.krml
170
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_Fuel.krml
171
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_Const.krml
172
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_TSet.krml
173
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_CopyBuffer.krml
174
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_UInt32.krml
175
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/C_Loops.krml
176
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2.krml
177
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_FunctionalExtensionality.krml
178
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_Comment.krml
179
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Monotonic_HyperHeap.krml
180
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Seq.krml
181
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Order.krml
182
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_TermEq.krml
183
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_UInt64.krml
184
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Sealed_Inhabited.krml
185
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Pervasives_Native.krml
186
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_ErrorCode.krml
187
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Monotonic_Pure.krml
188
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Int.krml
189
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_InputBuffer.krml
190
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Classical_Sugar.krml
191
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Bytes32.krml
192
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Preorder.krml
193
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_VLData.krml
194
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Math_Lib.krml
195
+
./FSR.krml
196
+
./FSR_ExternalAPI.krml
197
+
./FSR_ExternalTypes.krml
198
+
FSRWrapper.c
199
+
-bundle
200
+
FStar.\*,LowStar.\*,C.\*[rename=Lib,rename-prefix]
201
+
-bundle
202
+
Prims,LowParse.\*,EverParse3d.\*[rename=EverParse,rename-prefix]
+202
c/krmlargs72e878.rsp
+202
c/krmlargs72e878.rsp
···
1
+
-tmpdir
2
+
.
3
+
-skip-compilation
4
+
-static-header
5
+
LowParse.Low.Base,EverParse3d.Prelude.StaticHeader,EverParse3d.ErrorCode,EverParse3d.CopyBuffer,EverParse3d.InputStream.\*
6
+
-no-prefix
7
+
LowParse.Slice
8
+
-no-prefix
9
+
LowParse.Low.BoundedInt
10
+
-library
11
+
Prims,LowParse.\*,EverParse3d.\*
12
+
-warn-error
13
+
-9@4-20
14
+
-fnoreturn-else
15
+
-fparentheses
16
+
-fcurly-braces
17
+
-fmicrosoft
18
+
-fno-shadow
19
+
-header
20
+
/Users/samoht/.local/everparse/bin/../src/3d/noheader.txt
21
+
-minimal
22
+
-add-include
23
+
"EverParse.h"
24
+
-fextern-c
25
+
-library
26
+
FSR.ExternalAPI
27
+
-no-prefix
28
+
FSR.ExternalTypes
29
+
-no-prefix
30
+
FSR.ExternalAPI
31
+
-add-include
32
+
"FSR_ExternalTypedefs.h"
33
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_BV.krml
34
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1_Derived_Lemmas.krml
35
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Kinds.krml
36
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Builtins.krml
37
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_Combinators.krml
38
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_ListUpTo.krml
39
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_Base.krml
40
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/Spec_Loops.krml
41
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Actions_Common.krml
42
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Monotonic_Witnessed.krml
43
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Prelude_StaticHeader.krml
44
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_FLData.krml
45
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_CLens.krml
46
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Int8.krml
47
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_ST.krml
48
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_Monotonic_Buffer.krml
49
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Pprint.krml
50
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Derived_Lemmas.krml
51
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1_Derived.krml
52
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_UInt128.krml
53
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_FLData.krml
54
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Int_Cast.krml
55
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_List_Tot_Properties.krml
56
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Endianness_BitFields.krml
57
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_Endianness.krml
58
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1.krml
59
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_Endianness.krml
60
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Math_Lemmas.krml
61
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Int16.krml
62
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1_Builtins.krml
63
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_ModifiesGen.krml
64
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_HyperStack.krml
65
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_DER.krml
66
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_Modifies.krml
67
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Actions_BackendFlag.krml
68
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Actions_All.krml
69
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Seq_Properties.krml
70
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_TypeChecker_Core.krml
71
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Set.krml
72
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Range.krml
73
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Endianness.krml
74
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_StrongExcludedMiddle.krml
75
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_TermEq_Simple.krml
76
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Util.krml
77
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_UInt.krml
78
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_List_Tot.krml
79
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Collect.krml
80
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Classical.krml
81
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_Failure.krml
82
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_BoundedInt.krml
83
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_UInt16.krml
84
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Norm.krml
85
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_BCVLI.krml
86
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_String.krml
87
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Heap.krml
88
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Issue.krml
89
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Tactics_V1_Builtins.krml
90
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Tactics_Types_Reflection.krml
91
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_ListUpTo.krml
92
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Data.krml
93
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_Seq.krml
94
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Monotonic_HyperStack.krml
95
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Bytes.krml
96
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Tactics_Common.krml
97
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_IndefiniteDescription.krml
98
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Compare.krml
99
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Tactics_V2_Builtins.krml
100
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_PropositionalExtensionality.krml
101
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_InputStream_All.krml
102
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_HyperStack_ST.krml
103
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_Base_Spec.krml
104
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_Int.krml
105
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_Base.krml
106
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_SeqBytes_Base.krml
107
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_AllIntegers.krml
108
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_BigOps.krml
109
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_List.krml
110
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1_Formula.krml
111
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_VConfig.krml
112
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_GSet.krml
113
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Char.krml
114
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_BitVector.krml
115
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Monotonic_Heap.krml
116
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Arith.krml
117
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Sealed.krml
118
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_BitFields.krml
119
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Int64.krml
120
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Prelude.krml
121
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Attributes.krml
122
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_ErrorCode.krml
123
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Syntax_Syntax.krml
124
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_Types.krml
125
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Actions_Base.krml
126
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_NormSteps.krml
127
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Tactics_Unseal.krml
128
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Tactics_Types.krml
129
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Seq_Base.krml
130
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_UInt8.krml
131
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_Buffer.krml
132
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Float.krml
133
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Errors_Msg.krml
134
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_List_Tot_Base.krml
135
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_List.krml
136
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_Int.krml
137
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_All.krml
138
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_PredicateExtensionality.krml
139
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1_Compare.krml
140
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_BufferOps.krml
141
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1_Data.krml
142
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_Bytes.krml
143
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Formula.krml
144
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Universe.krml
145
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Map.krml
146
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Exn.krml
147
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Actions_BackendFlagValue.krml
148
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Calc.krml
149
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Int32.krml
150
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Math.krml
151
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_ProbeActions.krml
152
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Slice.krml
153
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Mul.krml
154
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Squash.krml
155
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Bytes.krml
156
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_AppCtxt.krml
157
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Ghost.krml
158
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Endianness.krml
159
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Readable.krml
160
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_BoundedInt.krml
161
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_ErasedLogic.krml
162
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_Combinators.krml
163
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Pervasives.krml
164
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_InputStream_Buffer_Aux.krml
165
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_InputStream_Base.krml
166
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_VLGen.krml
167
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Derived.krml
168
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Prelude.krml
169
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_InputStream_Buffer.krml
170
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_Fuel.krml
171
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_Const.krml
172
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_TSet.krml
173
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_CopyBuffer.krml
174
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_UInt32.krml
175
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/C_Loops.krml
176
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2.krml
177
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_FunctionalExtensionality.krml
178
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_Comment.krml
179
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Monotonic_HyperHeap.krml
180
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Seq.krml
181
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Order.krml
182
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_TermEq.krml
183
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_UInt64.krml
184
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Sealed_Inhabited.krml
185
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Pervasives_Native.krml
186
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_ErrorCode.krml
187
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Monotonic_Pure.krml
188
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Int.krml
189
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_InputBuffer.krml
190
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Classical_Sugar.krml
191
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Bytes32.krml
192
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Preorder.krml
193
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_VLData.krml
194
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Math_Lib.krml
195
+
./FSR.krml
196
+
./FSR_ExternalAPI.krml
197
+
./FSR_ExternalTypes.krml
198
+
FSRWrapper.c
199
+
-bundle
200
+
FStar.\*,LowStar.\*,C.\*[rename=Lib,rename-prefix]
201
+
-bundle
202
+
Prims,LowParse.\*,EverParse3d.\*[rename=EverParse,rename-prefix]
+202
c/krmlargsdd292e.rsp
+202
c/krmlargsdd292e.rsp
···
1
+
-tmpdir
2
+
.
3
+
-skip-compilation
4
+
-static-header
5
+
LowParse.Low.Base,EverParse3d.Prelude.StaticHeader,EverParse3d.ErrorCode,EverParse3d.CopyBuffer,EverParse3d.InputStream.\*
6
+
-no-prefix
7
+
LowParse.Slice
8
+
-no-prefix
9
+
LowParse.Low.BoundedInt
10
+
-library
11
+
Prims,LowParse.\*,EverParse3d.\*
12
+
-warn-error
13
+
-9@4-20
14
+
-fnoreturn-else
15
+
-fparentheses
16
+
-fcurly-braces
17
+
-fmicrosoft
18
+
-fno-shadow
19
+
-header
20
+
/Users/samoht/.local/everparse/bin/../src/3d/noheader.txt
21
+
-minimal
22
+
-add-include
23
+
"EverParse.h"
24
+
-fextern-c
25
+
-library
26
+
FSR.ExternalAPI
27
+
-no-prefix
28
+
FSR.ExternalTypes
29
+
-no-prefix
30
+
FSR.ExternalAPI
31
+
-add-include
32
+
"FSR_ExternalTypedefs.h"
33
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_BV.krml
34
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1_Derived_Lemmas.krml
35
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Kinds.krml
36
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Builtins.krml
37
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_Combinators.krml
38
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_ListUpTo.krml
39
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_Base.krml
40
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/Spec_Loops.krml
41
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Actions_Common.krml
42
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Monotonic_Witnessed.krml
43
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Prelude_StaticHeader.krml
44
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_FLData.krml
45
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_CLens.krml
46
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Int8.krml
47
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_ST.krml
48
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_Monotonic_Buffer.krml
49
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Pprint.krml
50
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Derived_Lemmas.krml
51
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1_Derived.krml
52
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_UInt128.krml
53
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_FLData.krml
54
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Int_Cast.krml
55
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_List_Tot_Properties.krml
56
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Endianness_BitFields.krml
57
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_Endianness.krml
58
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1.krml
59
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_Endianness.krml
60
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Math_Lemmas.krml
61
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Int16.krml
62
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1_Builtins.krml
63
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_ModifiesGen.krml
64
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_HyperStack.krml
65
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_DER.krml
66
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_Modifies.krml
67
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Actions_BackendFlag.krml
68
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Actions_All.krml
69
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Seq_Properties.krml
70
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_TypeChecker_Core.krml
71
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Set.krml
72
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Range.krml
73
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Endianness.krml
74
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_StrongExcludedMiddle.krml
75
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_TermEq_Simple.krml
76
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Util.krml
77
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_UInt.krml
78
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_List_Tot.krml
79
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Collect.krml
80
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Classical.krml
81
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_Failure.krml
82
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_BoundedInt.krml
83
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_UInt16.krml
84
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Norm.krml
85
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_BCVLI.krml
86
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_String.krml
87
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Heap.krml
88
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Issue.krml
89
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Tactics_V1_Builtins.krml
90
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Tactics_Types_Reflection.krml
91
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_ListUpTo.krml
92
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Data.krml
93
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_Seq.krml
94
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Monotonic_HyperStack.krml
95
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Bytes.krml
96
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Tactics_Common.krml
97
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_IndefiniteDescription.krml
98
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Compare.krml
99
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Tactics_V2_Builtins.krml
100
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_PropositionalExtensionality.krml
101
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_InputStream_All.krml
102
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_HyperStack_ST.krml
103
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_Base_Spec.krml
104
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_Int.krml
105
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_Base.krml
106
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_SeqBytes_Base.krml
107
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_AllIntegers.krml
108
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_BigOps.krml
109
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_List.krml
110
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1_Formula.krml
111
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_VConfig.krml
112
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_GSet.krml
113
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Char.krml
114
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_BitVector.krml
115
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Monotonic_Heap.krml
116
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Arith.krml
117
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Sealed.krml
118
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_BitFields.krml
119
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Int64.krml
120
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Prelude.krml
121
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Attributes.krml
122
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_ErrorCode.krml
123
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Syntax_Syntax.krml
124
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_Types.krml
125
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Actions_Base.krml
126
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_NormSteps.krml
127
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Tactics_Unseal.krml
128
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Tactics_Types.krml
129
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Seq_Base.krml
130
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_UInt8.krml
131
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_Buffer.krml
132
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Float.krml
133
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Errors_Msg.krml
134
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_List_Tot_Base.krml
135
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_List.krml
136
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_Int.krml
137
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_All.krml
138
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_PredicateExtensionality.krml
139
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1_Compare.krml
140
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_BufferOps.krml
141
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V1_Data.krml
142
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_Bytes.krml
143
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Formula.krml
144
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Universe.krml
145
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Map.krml
146
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Exn.krml
147
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Actions_BackendFlagValue.krml
148
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Calc.krml
149
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Int32.krml
150
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Math.krml
151
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_ProbeActions.krml
152
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Slice.krml
153
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Mul.krml
154
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Squash.krml
155
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Bytes.krml
156
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_AppCtxt.krml
157
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Ghost.krml
158
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Endianness.krml
159
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_Readable.krml
160
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_BoundedInt.krml
161
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_ErasedLogic.krml
162
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Low_Combinators.krml
163
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Pervasives.krml
164
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_InputStream_Buffer_Aux.krml
165
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_InputStream_Base.krml
166
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_VLGen.krml
167
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2_Derived.krml
168
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Prelude.krml
169
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_InputStream_Buffer.krml
170
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_Fuel.krml
171
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_Const.krml
172
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_TSet.krml
173
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_CopyBuffer.krml
174
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_UInt32.krml
175
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/C_Loops.krml
176
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_V2.krml
177
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_FunctionalExtensionality.krml
178
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowStar_Comment.krml
179
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Monotonic_HyperHeap.krml
180
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Seq.krml
181
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Order.krml
182
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Reflection_TermEq.krml
183
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_UInt64.krml
184
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Sealed_Inhabited.krml
185
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Pervasives_Native.krml
186
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_ErrorCode.krml
187
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Monotonic_Pure.krml
188
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Int.krml
189
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/EverParse3d_InputBuffer.krml
190
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Classical_Sugar.krml
191
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Bytes32.krml
192
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Preorder.krml
193
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/LowParse_Spec_VLData.krml
194
+
/Users/samoht/.local/everparse/bin/../src/3d/prelude/buffer/FStar_Math_Lib.krml
195
+
./FSR.krml
196
+
./FSR_ExternalAPI.krml
197
+
./FSR_ExternalTypes.krml
198
+
FSRWrapper.c
199
+
-bundle
200
+
FStar.\*,LowStar.\*,C.\*[rename=Lib,rename-prefix]
201
+
-bundle
202
+
Prims,LowParse.\*,EverParse3d.\*[rename=EverParse,rename-prefix]
+67
c/test.c
+67
c/test.c
···
1
+
#include <stdio.h>
2
+
#include <stdlib.h>
3
+
#include <stdint.h>
4
+
#include <string.h>
5
+
#include "EverParse.h"
6
+
#include "FSR.h"
7
+
8
+
static int error_count;
9
+
10
+
static void counting_error_handler(
11
+
EVERPARSE_STRING t, EVERPARSE_STRING f, EVERPARSE_STRING r,
12
+
uint64_t c, uint8_t *ctx, uint8_t *i, uint64_t p) {
13
+
(void)t; (void)f; (void)r; (void)c; (void)ctx; (void)i; (void)p;
14
+
error_count++;
15
+
}
16
+
17
+
#define CHECK(msg, cond) do { \
18
+
if (cond) { pass++; } \
19
+
else { fail++; fprintf(stderr, " FAIL: %s\n", msg); } \
20
+
} while(0)
21
+
22
+
int main(void) {
23
+
int failures = 0;
24
+
25
+
/* FSR (32 bytes) */
26
+
{
27
+
int pass = 0, fail = 0;
28
+
uint8_t buf[32];
29
+
uint64_t r;
30
+
31
+
memset(buf, 0, 32);
32
+
r = FsrValidateFsr(NULL, NULL, counting_error_handler, buf, 32, 0);
33
+
CHECK("zero buffer validates", EverParseIsSuccess(r));
34
+
CHECK("position advanced to 32", r == 32);
35
+
36
+
r = FsrValidateFsr(NULL, NULL, counting_error_handler, buf, 64, 0);
37
+
CHECK("larger buffer validates", EverParseIsSuccess(r));
38
+
CHECK("position is 32 not 64", r == 32);
39
+
40
+
for (uint64_t len = 0; len < 32; len++) {
41
+
error_count = 0;
42
+
r = FsrValidateFsr(NULL, NULL, counting_error_handler, buf, len, 0);
43
+
CHECK("truncated to len fails", EverParseIsError(r));
44
+
}
45
+
46
+
r = FsrValidateFsr(NULL, NULL, counting_error_handler, buf, 0, 0);
47
+
CHECK("empty input fails", EverParseIsError(r));
48
+
49
+
srand(42);
50
+
for (int i = 0; i < 1000; i++) {
51
+
for (int j = 0; j < 32; j++)
52
+
buf[j] = (uint8_t)(rand() & 0xff);
53
+
r = FsrValidateFsr(NULL, NULL, counting_error_handler, buf, 32, 0);
54
+
CHECK("random buffer validates", EverParseIsSuccess(r));
55
+
CHECK("random position correct", r == 32);
56
+
}
57
+
58
+
printf("fsr: %d passed, %d failed\n", pass, fail);
59
+
failures += fail;
60
+
}
61
+
62
+
if (failures == 0)
63
+
printf("All tests passed.\n");
64
+
else
65
+
printf("%d test(s) failed.\n", failures);
66
+
return failures ? 1 : 0;
67
+
}
+16
-17
fuzz/fuzz_fsr.ml
+16
-17
fuzz/fuzz_fsr.ml
···
5
5
6
6
open Alcobar
7
7
8
+
(* Pack the four alarm/bad_* flags into a single 4-bit integer so the fuzz
9
+
generators produce one value instead of four unlabeled bools. *)
10
+
let fsr_of_bits flags spi arsn_lsb =
11
+
let bit i = (flags lsr i) land 1 <> 0 in
12
+
Fsr.v ~alarm:(bit 0) ~bad_sn:(bit 1) ~bad_mac:(bit 2) ~bad_sa:(bit 3)
13
+
~spi:(spi mod 65536) ~arsn_lsb:(arsn_lsb mod 256)
14
+
8
15
(** Roundtrip: random FSR -> encode to int32 -> decode -> verify equal. *)
9
-
let test_roundtrip alarm bad_sn bad_mac bad_sa spi arsn_lsb =
10
-
let spi = spi mod 65536 in
11
-
let arsn_lsb = arsn_lsb mod 256 in
12
-
let fsr = Fsr.v ~alarm ~bad_sn ~bad_mac ~bad_sa ~spi ~arsn_lsb in
16
+
let test_roundtrip flags spi arsn_lsb =
17
+
let fsr = fsr_of_bits flags spi arsn_lsb in
13
18
let word = Fsr.encode fsr in
14
19
match Fsr.decode word with
15
20
| Error e -> fail (Fmt.str "decode failed: %a" Fsr.pp_error e)
···
22
27
()
23
28
24
29
(** Encode determinism: same FSR encodes to same word. *)
25
-
let test_encode_determinism alarm bad_sn bad_mac bad_sa spi arsn_lsb =
26
-
let spi = spi mod 65536 in
27
-
let arsn_lsb = arsn_lsb mod 256 in
28
-
let fsr = Fsr.v ~alarm ~bad_sn ~bad_mac ~bad_sa ~spi ~arsn_lsb in
30
+
let test_encode_determinism flags spi arsn_lsb =
31
+
let fsr = fsr_of_bits flags spi arsn_lsb in
29
32
let w1 = Fsr.encode fsr in
30
33
let w2 = Fsr.encode fsr in
31
34
check_eq ~pp:pp_int32 w1 w2
32
35
33
36
(** pp crash safety: pretty-printing should not crash. *)
34
-
let test_pp_crash alarm bad_sn bad_mac bad_sa spi arsn_lsb =
35
-
let spi = spi mod 65536 in
36
-
let arsn_lsb = arsn_lsb mod 256 in
37
-
let fsr = Fsr.v ~alarm ~bad_sn ~bad_mac ~bad_sa ~spi ~arsn_lsb in
37
+
let test_pp_crash flags spi arsn_lsb =
38
+
let fsr = fsr_of_bits flags spi arsn_lsb in
38
39
let _ = Fmt.str "%a" Fsr.pp fsr in
39
40
()
40
41
41
42
let suite =
42
43
( "fsr",
43
44
[
44
-
test_case "roundtrip"
45
-
[ bool; bool; bool; bool; range 65536; range 256 ]
46
-
test_roundtrip;
45
+
test_case "roundtrip" [ range 16; range 65536; range 256 ] test_roundtrip;
47
46
test_case "decode crash safety" [ int32 ] test_decode_crash;
48
47
test_case "encode determinism"
49
-
[ bool; bool; bool; bool; range 65536; range 256 ]
48
+
[ range 16; range 65536; range 256 ]
50
49
test_encode_determinism;
51
50
test_case "pp crash safety"
52
-
[ bool; bool; bool; bool; range 65536; range 256 ]
51
+
[ range 16; range 65536; range 256 ]
53
52
test_pp_crash;
54
53
] )