CCSDS File Delivery Protocol (CCSDS 727.0-B-5) for space file transfer
regenerate EverParse C files with wire 0.9.0
Wire_3d now generates ExternalTypedefs.h, ExternalAPI.h, Wrapper,
and Fields files for schemas using WireCtx. Bitfield padding is
fixed so .3d structs match the OCaml codec wire_size. Test.c passes
NULL for the WIRECTX parameter and links per-schema Field stubs.
Affected: ax25, cfdp, fsr, ltp, mbr, pid1, pus, rpmsg, sdls,
spacefibre, squashfs, tcpcl, udpcl, spacewire, and others via @gen.
+1400
-17
+6
-6
c/CfdpAck.3d
+6
-6
c/CfdpAck.3d
···
1
1
extern typedef struct _WireCtx WireCtx
2
2
3
-
extern unit WireSetU8(mutable WireCtx *ctx, UINT32 idx, UINT8 v)
3
+
extern unit CfdpAckSetU8(mutable WireCtx *ctx, UINT32 idx, UINT8 v)
4
4
5
5
entrypoint
6
6
typedef struct _CfdpAck(mutable WireCtx *ctx)
7
7
{
8
-
UINT8 subtype : 4 {:act WireSetU8(ctx, (UINT32) 1, subtype); };
9
-
UINT8 directive : 4 {:act WireSetU8(ctx, (UINT32) 0, directive); };
10
-
UINT8 tx_status : 2 {:act WireSetU8(ctx, (UINT32) 4, tx_status); };
11
-
UINT8 spare : 2 {:act WireSetU8(ctx, (UINT32) 3, spare); };
12
-
UINT8 condition : 4 {:act WireSetU8(ctx, (UINT32) 2, condition); };
8
+
UINT8 subtype : 4 {:act CfdpAckSetU8(ctx, (UINT32) 1, subtype); };
9
+
UINT8 directive : 4 {:act CfdpAckSetU8(ctx, (UINT32) 0, directive); };
10
+
UINT8 tx_status : 2 {:act CfdpAckSetU8(ctx, (UINT32) 4, tx_status); };
11
+
UINT8 spare : 2 {:act CfdpAckSetU8(ctx, (UINT32) 3, spare); };
12
+
UINT8 condition : 4 {:act CfdpAckSetU8(ctx, (UINT32) 2, condition); };
13
13
} CfdpAck;
14
14
15
15
+116
c/CfdpAck.c
+116
c/CfdpAck.c
···
1
+
2
+
3
+
#include "CfdpAck.h"
4
+
5
+
#include "CfdpAck_ExternalAPI.h"
6
+
7
+
uint64_t
8
+
CfdpAckValidateCfdpAck(
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 UINT8, i.e., 1 byte */
28
+
BOOLEAN hasBytes0 = 1ULL <= (InputLength - StartPosition);
29
+
uint64_t positionAfterBitfield0;
30
+
if (hasBytes0)
31
+
{
32
+
positionAfterBitfield0 = StartPosition + 1ULL;
33
+
}
34
+
else
35
+
{
36
+
positionAfterBitfield0 =
37
+
EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA,
38
+
StartPosition);
39
+
}
40
+
uint64_t positionAfterCfdpAck;
41
+
if (EverParseIsError(positionAfterBitfield0))
42
+
{
43
+
positionAfterCfdpAck = positionAfterBitfield0;
44
+
}
45
+
else
46
+
{
47
+
uint8_t bitfield0 = Input[(uint32_t)StartPosition];
48
+
CfdpAckSetU8(Ctx, (uint32_t)1U, EverParseGetBitfield8(bitfield0, 0U, 4U));
49
+
CfdpAckSetU8(Ctx, (uint32_t)0U, EverParseGetBitfield8(bitfield0, 4U, 8U));
50
+
BOOLEAN actionResult = TRUE;
51
+
KRML_MAYBE_UNUSED_VAR(actionResult);
52
+
positionAfterCfdpAck = positionAfterBitfield0;
53
+
}
54
+
uint64_t positionAfterBitfield00;
55
+
if (EverParseIsSuccess(positionAfterCfdpAck))
56
+
{
57
+
positionAfterBitfield00 = positionAfterCfdpAck;
58
+
}
59
+
else
60
+
{
61
+
ErrorHandlerFn("_CfdpAck",
62
+
"__bitfield_0",
63
+
EverParseErrorReasonOfResult(positionAfterCfdpAck),
64
+
EverParseGetValidatorErrorKind(positionAfterCfdpAck),
65
+
Ctxt,
66
+
Input,
67
+
StartPosition);
68
+
positionAfterBitfield00 = positionAfterCfdpAck;
69
+
}
70
+
if (EverParseIsError(positionAfterBitfield00))
71
+
{
72
+
return positionAfterBitfield00;
73
+
}
74
+
/* Validating field __bitfield_1 */
75
+
/* Checking that we have enough space for a UINT8, i.e., 1 byte */
76
+
BOOLEAN hasBytes = 1ULL <= (InputLength - positionAfterBitfield00);
77
+
uint64_t positionAfterBitfield1;
78
+
if (hasBytes)
79
+
{
80
+
positionAfterBitfield1 = positionAfterBitfield00 + 1ULL;
81
+
}
82
+
else
83
+
{
84
+
positionAfterBitfield1 =
85
+
EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA,
86
+
positionAfterBitfield00);
87
+
}
88
+
uint64_t positionAfterCfdpAck0;
89
+
if (EverParseIsError(positionAfterBitfield1))
90
+
{
91
+
positionAfterCfdpAck0 = positionAfterBitfield1;
92
+
}
93
+
else
94
+
{
95
+
uint8_t bitfield1 = Input[(uint32_t)positionAfterBitfield00];
96
+
CfdpAckSetU8(Ctx, (uint32_t)4U, EverParseGetBitfield8(bitfield1, 0U, 2U));
97
+
CfdpAckSetU8(Ctx, (uint32_t)3U, EverParseGetBitfield8(bitfield1, 2U, 4U));
98
+
CfdpAckSetU8(Ctx, (uint32_t)2U, EverParseGetBitfield8(bitfield1, 4U, 8U));
99
+
BOOLEAN actionResult = TRUE;
100
+
KRML_MAYBE_UNUSED_VAR(actionResult);
101
+
positionAfterCfdpAck0 = positionAfterBitfield1;
102
+
}
103
+
if (EverParseIsSuccess(positionAfterCfdpAck0))
104
+
{
105
+
return positionAfterCfdpAck0;
106
+
}
107
+
ErrorHandlerFn("_CfdpAck",
108
+
"__bitfield_1",
109
+
EverParseErrorReasonOfResult(positionAfterCfdpAck0),
110
+
EverParseGetValidatorErrorKind(positionAfterCfdpAck0),
111
+
Ctxt,
112
+
Input,
113
+
positionAfterBitfield00);
114
+
return positionAfterCfdpAck0;
115
+
}
116
+
+37
c/CfdpAck.h
+37
c/CfdpAck.h
···
1
+
2
+
3
+
#ifndef CfdpAck_H
4
+
#define CfdpAck_H
5
+
6
+
#if defined(__cplusplus)
7
+
extern "C" {
8
+
#endif
9
+
10
+
#include "EverParse.h"
11
+
#include "CfdpAck_ExternalTypedefs.h"
12
+
13
+
uint64_t
14
+
CfdpAckValidateCfdpAck(
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 CfdpAck_H_DEFINED
37
+
#endif /* CfdpAck_H */
+41
c/CfdpAckWrapper.c
+41
c/CfdpAckWrapper.c
···
1
+
#include "CfdpAckWrapper.h"
2
+
#include "EverParse.h"
3
+
#include "CfdpAck.h"
4
+
void CfdpAckEverParseError(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 CfdpAckCheckCfdpAck(WIRECTX* ctx, uint8_t *base, uint32_t len) {
29
+
EVERPARSE_ERROR_FRAME frame;
30
+
frame.filled = FALSE;
31
+
uint64_t result = CfdpAckValidateCfdpAck(ctx, (uint8_t*)&frame, &DefaultErrorHandler, base, len, 0);
32
+
if (EverParseIsError(result))
33
+
{
34
+
if (frame.filled)
35
+
{
36
+
CfdpAckEverParseError(frame.typename_s, frame.fieldname, frame.reason);
37
+
}
38
+
return FALSE;
39
+
}
40
+
return TRUE;
41
+
}
+26
c/CfdpAckWrapper.h
+26
c/CfdpAckWrapper.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 "CfdpAck_ExternalTypedefs.h"
18
+
19
+
20
+
#ifdef __cplusplus
21
+
extern "C" {
22
+
#endif
23
+
BOOLEAN CfdpAckCheckCfdpAck(WIRECTX* ctx, uint8_t *base, uint32_t len);
24
+
#ifdef __cplusplus
25
+
}
26
+
#endif
+20
c/CfdpAck_ExternalAPI.h
+20
c/CfdpAck_ExternalAPI.h
···
1
+
2
+
3
+
#ifndef CfdpAck_ExternalAPI_H
4
+
#define CfdpAck_ExternalAPI_H
5
+
6
+
#if defined(__cplusplus)
7
+
extern "C" {
8
+
#endif
9
+
10
+
#include "EverParse.h"
11
+
#include "CfdpAck_ExternalTypedefs.h"
12
+
13
+
extern void CfdpAckSetU8(WIRECTX *ctx, uint32_t idx, uint8_t v);
14
+
15
+
#if defined(__cplusplus)
16
+
}
17
+
#endif
18
+
19
+
#define CfdpAck_ExternalAPI_H_DEFINED
20
+
#endif /* CfdpAck_ExternalAPI_H */
+4
c/CfdpAck_ExternalTypedefs.h
+4
c/CfdpAck_ExternalTypedefs.h
+17
c/CfdpAck_Fields.c
+17
c/CfdpAck_Fields.c
···
1
+
#include <stdint.h>
2
+
#include "CfdpAck_Fields.h"
3
+
#include "CfdpAck_ExternalTypedefs.h"
4
+
#include "CfdpAck_ExternalAPI.h"
5
+
6
+
void CfdpAckSetU8(WIRECTX *ctx, uint32_t idx, uint8_t v) {
7
+
CfdpAckFields *f = (CfdpAckFields *) ctx;
8
+
switch (idx) {
9
+
case 0: f->directive = (uint8_t) v; break;
10
+
case 1: f->subtype = (uint8_t) v; break;
11
+
case 2: f->condition = (uint8_t) v; break;
12
+
case 3: f->spare = (uint8_t) v; break;
13
+
case 4: f->tx_status = (uint8_t) v; break;
14
+
default: (void) f; (void) v; break;
15
+
}
16
+
}
17
+
+22
c/CfdpAck_Fields.h
+22
c/CfdpAck_Fields.h
···
1
+
#ifndef CFDPACK_FIELDS_H
2
+
#define CFDPACK_FIELDS_H
3
+
#include <stdint.h>
4
+
5
+
/* Field indices -- use with the schema's WireSet* callbacks in a
6
+
custom [WIRECTX] if you only want to capture a subset. */
7
+
#define CFDPACK_IDX_DIRECTIVE 0
8
+
#define CFDPACK_IDX_SUBTYPE 1
9
+
#define CFDPACK_IDX_CONDITION 2
10
+
#define CFDPACK_IDX_SPARE 3
11
+
#define CFDPACK_IDX_TX_STATUS 4
12
+
13
+
/* Default plug: one typed member per named field. Pass a pointer to
14
+
[CfdpAckFields] as [WIRECTX *] when you want every field populated. */
15
+
typedef struct CfdpAckFields {
16
+
uint8_t directive;
17
+
uint8_t subtype;
18
+
uint8_t condition;
19
+
uint8_t spare;
20
+
uint8_t tx_status;
21
+
} CfdpAckFields;
22
+
#endif
+5
-5
c/CfdpFinished.3d
+5
-5
c/CfdpFinished.3d
···
1
1
extern typedef struct _WireCtx WireCtx
2
2
3
-
extern unit WireSetU8(mutable WireCtx *ctx, UINT32 idx, UINT8 v)
3
+
extern unit CfdpFinishedSetU8(mutable WireCtx *ctx, UINT32 idx, UINT8 v)
4
4
5
5
entrypoint
6
6
typedef struct _CfdpFinished(mutable WireCtx *ctx)
7
7
{
8
-
UINT8 file_status : 2 {:act WireSetU8(ctx, (UINT32) 3, file_status); };
9
-
UINT8 delivery : 1 {:act WireSetU8(ctx, (UINT32) 2, delivery); };
10
-
UINT8 spare : 1 {:act WireSetU8(ctx, (UINT32) 1, spare); };
11
-
UINT8 condition : 4 {:act WireSetU8(ctx, (UINT32) 0, condition); };
8
+
UINT8 file_status : 2 {:act CfdpFinishedSetU8(ctx, (UINT32) 3, file_status); };
9
+
UINT8 delivery : 1 {:act CfdpFinishedSetU8(ctx, (UINT32) 2, delivery); };
10
+
UINT8 spare : 1 {:act CfdpFinishedSetU8(ctx, (UINT32) 1, spare); };
11
+
UINT8 condition : 4 {:act CfdpFinishedSetU8(ctx, (UINT32) 0, condition); };
12
12
} CfdpFinished;
13
13
14
14
+69
c/CfdpFinished.c
+69
c/CfdpFinished.c
···
1
+
2
+
3
+
#include "CfdpFinished.h"
4
+
5
+
#include "CfdpFinished_ExternalAPI.h"
6
+
7
+
uint64_t
8
+
CfdpFinishedValidateCfdpFinished(
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 UINT8, i.e., 1 byte */
28
+
BOOLEAN hasBytes = 1ULL <= (InputLength - StartPosition);
29
+
uint64_t positionAfterBitfield0;
30
+
if (hasBytes)
31
+
{
32
+
positionAfterBitfield0 = StartPosition + 1ULL;
33
+
}
34
+
else
35
+
{
36
+
positionAfterBitfield0 =
37
+
EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA,
38
+
StartPosition);
39
+
}
40
+
uint64_t positionAfterCfdpFinished;
41
+
if (EverParseIsError(positionAfterBitfield0))
42
+
{
43
+
positionAfterCfdpFinished = positionAfterBitfield0;
44
+
}
45
+
else
46
+
{
47
+
uint8_t bitfield0 = Input[(uint32_t)StartPosition];
48
+
CfdpFinishedSetU8(Ctx, (uint32_t)3U, EverParseGetBitfield8(bitfield0, 0U, 2U));
49
+
CfdpFinishedSetU8(Ctx, (uint32_t)2U, EverParseGetBitfield8(bitfield0, 2U, 3U));
50
+
CfdpFinishedSetU8(Ctx, (uint32_t)1U, EverParseGetBitfield8(bitfield0, 3U, 4U));
51
+
CfdpFinishedSetU8(Ctx, (uint32_t)0U, EverParseGetBitfield8(bitfield0, 4U, 8U));
52
+
BOOLEAN actionResult = TRUE;
53
+
KRML_MAYBE_UNUSED_VAR(actionResult);
54
+
positionAfterCfdpFinished = positionAfterBitfield0;
55
+
}
56
+
if (EverParseIsSuccess(positionAfterCfdpFinished))
57
+
{
58
+
return positionAfterCfdpFinished;
59
+
}
60
+
ErrorHandlerFn("_CfdpFinished",
61
+
"__bitfield_0",
62
+
EverParseErrorReasonOfResult(positionAfterCfdpFinished),
63
+
EverParseGetValidatorErrorKind(positionAfterCfdpFinished),
64
+
Ctxt,
65
+
Input,
66
+
StartPosition);
67
+
return positionAfterCfdpFinished;
68
+
}
69
+
+37
c/CfdpFinished.h
+37
c/CfdpFinished.h
···
1
+
2
+
3
+
#ifndef CfdpFinished_H
4
+
#define CfdpFinished_H
5
+
6
+
#if defined(__cplusplus)
7
+
extern "C" {
8
+
#endif
9
+
10
+
#include "EverParse.h"
11
+
#include "CfdpFinished_ExternalTypedefs.h"
12
+
13
+
uint64_t
14
+
CfdpFinishedValidateCfdpFinished(
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 CfdpFinished_H_DEFINED
37
+
#endif /* CfdpFinished_H */
+41
c/CfdpFinishedWrapper.c
+41
c/CfdpFinishedWrapper.c
···
1
+
#include "CfdpFinishedWrapper.h"
2
+
#include "EverParse.h"
3
+
#include "CfdpFinished.h"
4
+
void CfdpFinishedEverParseError(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 CfdpFinishedCheckCfdpFinished(WIRECTX* ctx, uint8_t *base, uint32_t len) {
29
+
EVERPARSE_ERROR_FRAME frame;
30
+
frame.filled = FALSE;
31
+
uint64_t result = CfdpFinishedValidateCfdpFinished(ctx, (uint8_t*)&frame, &DefaultErrorHandler, base, len, 0);
32
+
if (EverParseIsError(result))
33
+
{
34
+
if (frame.filled)
35
+
{
36
+
CfdpFinishedEverParseError(frame.typename_s, frame.fieldname, frame.reason);
37
+
}
38
+
return FALSE;
39
+
}
40
+
return TRUE;
41
+
}
+26
c/CfdpFinishedWrapper.h
+26
c/CfdpFinishedWrapper.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 "CfdpFinished_ExternalTypedefs.h"
18
+
19
+
20
+
#ifdef __cplusplus
21
+
extern "C" {
22
+
#endif
23
+
BOOLEAN CfdpFinishedCheckCfdpFinished(WIRECTX* ctx, uint8_t *base, uint32_t len);
24
+
#ifdef __cplusplus
25
+
}
26
+
#endif
+20
c/CfdpFinished_ExternalAPI.h
+20
c/CfdpFinished_ExternalAPI.h
···
1
+
2
+
3
+
#ifndef CfdpFinished_ExternalAPI_H
4
+
#define CfdpFinished_ExternalAPI_H
5
+
6
+
#if defined(__cplusplus)
7
+
extern "C" {
8
+
#endif
9
+
10
+
#include "EverParse.h"
11
+
#include "CfdpFinished_ExternalTypedefs.h"
12
+
13
+
extern void CfdpFinishedSetU8(WIRECTX *ctx, uint32_t idx, uint8_t v);
14
+
15
+
#if defined(__cplusplus)
16
+
}
17
+
#endif
18
+
19
+
#define CfdpFinished_ExternalAPI_H_DEFINED
20
+
#endif /* CfdpFinished_ExternalAPI_H */
+4
c/CfdpFinished_ExternalTypedefs.h
+4
c/CfdpFinished_ExternalTypedefs.h
+16
c/CfdpFinished_Fields.c
+16
c/CfdpFinished_Fields.c
···
1
+
#include <stdint.h>
2
+
#include "CfdpFinished_Fields.h"
3
+
#include "CfdpFinished_ExternalTypedefs.h"
4
+
#include "CfdpFinished_ExternalAPI.h"
5
+
6
+
void CfdpFinishedSetU8(WIRECTX *ctx, uint32_t idx, uint8_t v) {
7
+
CfdpFinishedFields *f = (CfdpFinishedFields *) ctx;
8
+
switch (idx) {
9
+
case 0: f->condition = (uint8_t) v; break;
10
+
case 1: f->spare = (uint8_t) v; break;
11
+
case 2: f->delivery = (uint8_t) v; break;
12
+
case 3: f->file_status = (uint8_t) v; break;
13
+
default: (void) f; (void) v; break;
14
+
}
15
+
}
16
+
+20
c/CfdpFinished_Fields.h
+20
c/CfdpFinished_Fields.h
···
1
+
#ifndef CFDPFINISHED_FIELDS_H
2
+
#define CFDPFINISHED_FIELDS_H
3
+
#include <stdint.h>
4
+
5
+
/* Field indices -- use with the schema's WireSet* callbacks in a
6
+
custom [WIRECTX] if you only want to capture a subset. */
7
+
#define CFDPFINISHED_IDX_CONDITION 0
8
+
#define CFDPFINISHED_IDX_SPARE 1
9
+
#define CFDPFINISHED_IDX_DELIVERY 2
10
+
#define CFDPFINISHED_IDX_FILE_STATUS 3
11
+
12
+
/* Default plug: one typed member per named field. Pass a pointer to
13
+
[CfdpFinishedFields] as [WIRECTX *] when you want every field populated. */
14
+
typedef struct CfdpFinishedFields {
15
+
uint8_t condition;
16
+
uint8_t spare;
17
+
uint8_t delivery;
18
+
uint8_t file_status;
19
+
} CfdpFinishedFields;
20
+
#endif
+3
-3
c/CfdpPrompt.3d
+3
-3
c/CfdpPrompt.3d
···
1
1
extern typedef struct _WireCtx WireCtx
2
2
3
-
extern unit WireSetU8(mutable WireCtx *ctx, UINT32 idx, UINT8 v)
3
+
extern unit CfdpPromptSetU8(mutable WireCtx *ctx, UINT32 idx, UINT8 v)
4
4
5
5
entrypoint
6
6
typedef struct _CfdpPrompt(mutable WireCtx *ctx)
7
7
{
8
-
UINT8 spare : 7 {:act WireSetU8(ctx, (UINT32) 1, spare); };
9
-
UINT8 response : 1 {:act WireSetU8(ctx, (UINT32) 0, response); };
8
+
UINT8 spare : 7 {:act CfdpPromptSetU8(ctx, (UINT32) 1, spare); };
9
+
UINT8 response : 1 {:act CfdpPromptSetU8(ctx, (UINT32) 0, response); };
10
10
} CfdpPrompt;
11
11
12
12
+67
c/CfdpPrompt.c
+67
c/CfdpPrompt.c
···
1
+
2
+
3
+
#include "CfdpPrompt.h"
4
+
5
+
#include "CfdpPrompt_ExternalAPI.h"
6
+
7
+
uint64_t
8
+
CfdpPromptValidateCfdpPrompt(
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 UINT8, i.e., 1 byte */
28
+
BOOLEAN hasBytes = 1ULL <= (InputLength - StartPosition);
29
+
uint64_t positionAfterBitfield0;
30
+
if (hasBytes)
31
+
{
32
+
positionAfterBitfield0 = StartPosition + 1ULL;
33
+
}
34
+
else
35
+
{
36
+
positionAfterBitfield0 =
37
+
EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA,
38
+
StartPosition);
39
+
}
40
+
uint64_t positionAfterCfdpPrompt;
41
+
if (EverParseIsError(positionAfterBitfield0))
42
+
{
43
+
positionAfterCfdpPrompt = positionAfterBitfield0;
44
+
}
45
+
else
46
+
{
47
+
uint8_t bitfield0 = Input[(uint32_t)StartPosition];
48
+
CfdpPromptSetU8(Ctx, (uint32_t)1U, EverParseGetBitfield8(bitfield0, 0U, 7U));
49
+
CfdpPromptSetU8(Ctx, (uint32_t)0U, EverParseGetBitfield8(bitfield0, 7U, 8U));
50
+
BOOLEAN actionResult = TRUE;
51
+
KRML_MAYBE_UNUSED_VAR(actionResult);
52
+
positionAfterCfdpPrompt = positionAfterBitfield0;
53
+
}
54
+
if (EverParseIsSuccess(positionAfterCfdpPrompt))
55
+
{
56
+
return positionAfterCfdpPrompt;
57
+
}
58
+
ErrorHandlerFn("_CfdpPrompt",
59
+
"__bitfield_0",
60
+
EverParseErrorReasonOfResult(positionAfterCfdpPrompt),
61
+
EverParseGetValidatorErrorKind(positionAfterCfdpPrompt),
62
+
Ctxt,
63
+
Input,
64
+
StartPosition);
65
+
return positionAfterCfdpPrompt;
66
+
}
67
+
+37
c/CfdpPrompt.h
+37
c/CfdpPrompt.h
···
1
+
2
+
3
+
#ifndef CfdpPrompt_H
4
+
#define CfdpPrompt_H
5
+
6
+
#if defined(__cplusplus)
7
+
extern "C" {
8
+
#endif
9
+
10
+
#include "EverParse.h"
11
+
#include "CfdpPrompt_ExternalTypedefs.h"
12
+
13
+
uint64_t
14
+
CfdpPromptValidateCfdpPrompt(
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 CfdpPrompt_H_DEFINED
37
+
#endif /* CfdpPrompt_H */
+41
c/CfdpPromptWrapper.c
+41
c/CfdpPromptWrapper.c
···
1
+
#include "CfdpPromptWrapper.h"
2
+
#include "EverParse.h"
3
+
#include "CfdpPrompt.h"
4
+
void CfdpPromptEverParseError(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 CfdpPromptCheckCfdpPrompt(WIRECTX* ctx, uint8_t *base, uint32_t len) {
29
+
EVERPARSE_ERROR_FRAME frame;
30
+
frame.filled = FALSE;
31
+
uint64_t result = CfdpPromptValidateCfdpPrompt(ctx, (uint8_t*)&frame, &DefaultErrorHandler, base, len, 0);
32
+
if (EverParseIsError(result))
33
+
{
34
+
if (frame.filled)
35
+
{
36
+
CfdpPromptEverParseError(frame.typename_s, frame.fieldname, frame.reason);
37
+
}
38
+
return FALSE;
39
+
}
40
+
return TRUE;
41
+
}
+26
c/CfdpPromptWrapper.h
+26
c/CfdpPromptWrapper.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 "CfdpPrompt_ExternalTypedefs.h"
18
+
19
+
20
+
#ifdef __cplusplus
21
+
extern "C" {
22
+
#endif
23
+
BOOLEAN CfdpPromptCheckCfdpPrompt(WIRECTX* ctx, uint8_t *base, uint32_t len);
24
+
#ifdef __cplusplus
25
+
}
26
+
#endif
+20
c/CfdpPrompt_ExternalAPI.h
+20
c/CfdpPrompt_ExternalAPI.h
···
1
+
2
+
3
+
#ifndef CfdpPrompt_ExternalAPI_H
4
+
#define CfdpPrompt_ExternalAPI_H
5
+
6
+
#if defined(__cplusplus)
7
+
extern "C" {
8
+
#endif
9
+
10
+
#include "EverParse.h"
11
+
#include "CfdpPrompt_ExternalTypedefs.h"
12
+
13
+
extern void CfdpPromptSetU8(WIRECTX *ctx, uint32_t idx, uint8_t v);
14
+
15
+
#if defined(__cplusplus)
16
+
}
17
+
#endif
18
+
19
+
#define CfdpPrompt_ExternalAPI_H_DEFINED
20
+
#endif /* CfdpPrompt_ExternalAPI_H */
+4
c/CfdpPrompt_ExternalTypedefs.h
+4
c/CfdpPrompt_ExternalTypedefs.h
+14
c/CfdpPrompt_Fields.c
+14
c/CfdpPrompt_Fields.c
···
1
+
#include <stdint.h>
2
+
#include "CfdpPrompt_Fields.h"
3
+
#include "CfdpPrompt_ExternalTypedefs.h"
4
+
#include "CfdpPrompt_ExternalAPI.h"
5
+
6
+
void CfdpPromptSetU8(WIRECTX *ctx, uint32_t idx, uint8_t v) {
7
+
CfdpPromptFields *f = (CfdpPromptFields *) ctx;
8
+
switch (idx) {
9
+
case 0: f->response = (uint8_t) v; break;
10
+
case 1: f->spare = (uint8_t) v; break;
11
+
default: (void) f; (void) v; break;
12
+
}
13
+
}
14
+
+16
c/CfdpPrompt_Fields.h
+16
c/CfdpPrompt_Fields.h
···
1
+
#ifndef CFDPPROMPT_FIELDS_H
2
+
#define CFDPPROMPT_FIELDS_H
3
+
#include <stdint.h>
4
+
5
+
/* Field indices -- use with the schema's WireSet* callbacks in a
6
+
custom [WIRECTX] if you only want to capture a subset. */
7
+
#define CFDPPROMPT_IDX_RESPONSE 0
8
+
#define CFDPPROMPT_IDX_SPARE 1
9
+
10
+
/* Default plug: one typed member per named field. Pass a pointer to
11
+
[CfdpPromptFields] as [WIRECTX *] when you want every field populated. */
12
+
typedef struct CfdpPromptFields {
13
+
uint8_t response;
14
+
uint8_t spare;
15
+
} CfdpPromptFields;
16
+
#endif
+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
+21
-3
c/dune.inc
+21
-3
c/dune.inc
···
9
9
(rule
10
10
(alias gen)
11
11
(mode fallback)
12
-
(targets EverParse.h EverParseEndianness.h CfdpFinished.h CfdpFinished.c CfdpAck.h CfdpAck.c CfdpPrompt.h CfdpPrompt.c test.c)
12
+
(targets EverParse.h EverParseEndianness.h CfdpFinished.h CfdpFinished.c CfdpAck.h CfdpAck.c CfdpPrompt.h CfdpPrompt.c CfdpFinished_ExternalTypedefs.h CfdpFinished_ExternalAPI.h CfdpFinishedWrapper.c CfdpFinishedWrapper.h CfdpFinished_Fields.h CfdpFinished_Fields.c CfdpAck_ExternalTypedefs.h CfdpAck_ExternalAPI.h CfdpAckWrapper.c CfdpAckWrapper.h CfdpAck_Fields.h CfdpAck_Fields.c CfdpPrompt_ExternalTypedefs.h CfdpPrompt_ExternalAPI.h CfdpPromptWrapper.c CfdpPromptWrapper.h CfdpPrompt_Fields.h CfdpPrompt_Fields.c test.c)
13
13
(deps gen.exe CfdpFinished.3d CfdpAck.3d CfdpPrompt.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 CfdpFinished.h CfdpFinished.c CfdpAck.h CfdpAck.c CfdpPrompt.h CfdpPrompt.c)
19
+
(deps test.c EverParse.h EverParseEndianness.h CfdpFinished.h CfdpFinished.c CfdpAck.h CfdpAck.c CfdpPrompt.h CfdpPrompt.c CfdpFinished_ExternalTypedefs.h CfdpFinished_ExternalAPI.h CfdpFinishedWrapper.c CfdpFinishedWrapper.h CfdpFinished_Fields.h CfdpFinished_Fields.c CfdpAck_ExternalTypedefs.h CfdpAck_ExternalAPI.h CfdpAckWrapper.c CfdpAckWrapper.h CfdpAck_Fields.h CfdpAck_Fields.c CfdpPrompt_ExternalTypedefs.h CfdpPrompt_ExternalAPI.h CfdpPromptWrapper.c CfdpPromptWrapper.h CfdpPrompt_Fields.h CfdpPrompt_Fields.c)
20
20
(action
21
21
(system
22
-
"cc -std=c11 -Wall -Wextra -Werror -o test_cfdp test.c CfdpFinished.c CfdpAck.c CfdpPrompt.c && ./test_cfdp")))
22
+
"cc -std=c99 -Wall -Wextra -Werror -Wpedantic -Wstrict-prototypes -Wmissing-prototypes -Wshadow -Wcast-qual -o test_cfdp test.c CfdpFinished.c CfdpAck.c CfdpPrompt.c CfdpFinished_Fields.c CfdpAck_Fields.c CfdpPrompt_Fields.c && ./test_cfdp")))
23
23
24
24
(install
25
25
(package cfdp)
···
34
34
(CfdpAck.c as c/CfdpAck.c)
35
35
(CfdpPrompt.h as c/CfdpPrompt.h)
36
36
(CfdpPrompt.c as c/CfdpPrompt.c)
37
+
(CfdpFinished_ExternalTypedefs.h as c/CfdpFinished_ExternalTypedefs.h)
38
+
(CfdpFinished_ExternalAPI.h as c/CfdpFinished_ExternalAPI.h)
39
+
(CfdpFinishedWrapper.c as c/CfdpFinishedWrapper.c)
40
+
(CfdpFinishedWrapper.h as c/CfdpFinishedWrapper.h)
41
+
(CfdpFinished_Fields.h as c/CfdpFinished_Fields.h)
42
+
(CfdpFinished_Fields.c as c/CfdpFinished_Fields.c)
43
+
(CfdpAck_ExternalTypedefs.h as c/CfdpAck_ExternalTypedefs.h)
44
+
(CfdpAck_ExternalAPI.h as c/CfdpAck_ExternalAPI.h)
45
+
(CfdpAckWrapper.c as c/CfdpAckWrapper.c)
46
+
(CfdpAckWrapper.h as c/CfdpAckWrapper.h)
47
+
(CfdpAck_Fields.h as c/CfdpAck_Fields.h)
48
+
(CfdpAck_Fields.c as c/CfdpAck_Fields.c)
49
+
(CfdpPrompt_ExternalTypedefs.h as c/CfdpPrompt_ExternalTypedefs.h)
50
+
(CfdpPrompt_ExternalAPI.h as c/CfdpPrompt_ExternalAPI.h)
51
+
(CfdpPromptWrapper.c as c/CfdpPromptWrapper.c)
52
+
(CfdpPromptWrapper.h as c/CfdpPromptWrapper.h)
53
+
(CfdpPrompt_Fields.h as c/CfdpPrompt_Fields.h)
54
+
(CfdpPrompt_Fields.c as c/CfdpPrompt_Fields.c)
37
55
(EverParse.h as c/EverParse.h)
38
56
(EverParseEndianness.h as c/EverParseEndianness.h)))
+176
c/test.c
+176
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 "CfdpFinished.h"
7
+
#include "CfdpFinished_Fields.h"
8
+
#include "CfdpAck.h"
9
+
#include "CfdpAck_Fields.h"
10
+
#include "CfdpPrompt.h"
11
+
#include "CfdpPrompt_Fields.h"
12
+
13
+
static int error_count;
14
+
15
+
static void counting_error_handler(
16
+
EVERPARSE_STRING t, EVERPARSE_STRING f, EVERPARSE_STRING r,
17
+
uint64_t c, uint8_t *ctx, uint8_t *i, uint64_t p) {
18
+
(void)t; (void)f; (void)r; (void)c; (void)ctx; (void)i; (void)p;
19
+
error_count++;
20
+
}
21
+
22
+
#define CHECK(msg, cond) do { \
23
+
if (cond) { pass++; } \
24
+
else { fail++; fprintf(stderr, " FAIL: %s\n", msg); } \
25
+
} while(0)
26
+
27
+
int main(void) {
28
+
int failures = 0;
29
+
30
+
/* CfdpFinished (1 bytes) */
31
+
{
32
+
int pass = 0, fail = 0;
33
+
uint8_t buf[1];
34
+
uint64_t r;
35
+
CfdpFinishedFields ctx = {0};
36
+
37
+
memset(buf, 0, 1);
38
+
r = CfdpFinishedValidateCfdpFinished((WIRECTX *) &ctx, NULL, counting_error_handler, buf, 1, 0);
39
+
if (!EverParseIsSuccess(r) || r != 1) {
40
+
fprintf(stderr,
41
+
"FATAL: CfdpFinished wire_size mismatch -- codec declared 1 bytes, "
42
+
"EverParse validator returned %llu. Fix the OCaml codec's "
43
+
"wire_size or the .3d projection.\n",
44
+
(unsigned long long) r);
45
+
return 2;
46
+
}
47
+
CHECK("zero buffer validates", EverParseIsSuccess(r));
48
+
CHECK("position advanced to 1", r == 1);
49
+
50
+
r = CfdpFinishedValidateCfdpFinished((WIRECTX *) &ctx, NULL, counting_error_handler, buf, 2, 0);
51
+
CHECK("larger buffer validates", EverParseIsSuccess(r));
52
+
CHECK("position is 1 not 2", r == 1);
53
+
54
+
for (uint64_t len = 0; len < 1; len++) {
55
+
error_count = 0;
56
+
r = CfdpFinishedValidateCfdpFinished((WIRECTX *) &ctx, NULL, counting_error_handler, buf, len, 0);
57
+
CHECK("truncated to len fails", EverParseIsError(r));
58
+
}
59
+
60
+
r = CfdpFinishedValidateCfdpFinished((WIRECTX *) &ctx, NULL, counting_error_handler, buf, 0, 0);
61
+
CHECK("empty input fails", EverParseIsError(r));
62
+
63
+
srand(42);
64
+
for (int i = 0; i < 1000; i++) {
65
+
for (int j = 0; j < 1; j++)
66
+
buf[j] = (uint8_t)(rand() & 0xff);
67
+
r = CfdpFinishedValidateCfdpFinished((WIRECTX *) &ctx, NULL, counting_error_handler, buf, 1, 0);
68
+
CHECK("random buffer validates", EverParseIsSuccess(r));
69
+
CHECK("random position correct", r == 1);
70
+
}
71
+
72
+
(void) ctx;
73
+
printf("cfdpfinished: %d passed, %d failed\n", pass, fail);
74
+
failures += fail;
75
+
}
76
+
77
+
/* CfdpAck (2 bytes) */
78
+
{
79
+
int pass = 0, fail = 0;
80
+
uint8_t buf[2];
81
+
uint64_t r;
82
+
CfdpAckFields ctx = {0};
83
+
84
+
memset(buf, 0, 2);
85
+
r = CfdpAckValidateCfdpAck((WIRECTX *) &ctx, NULL, counting_error_handler, buf, 2, 0);
86
+
if (!EverParseIsSuccess(r) || r != 2) {
87
+
fprintf(stderr,
88
+
"FATAL: CfdpAck wire_size mismatch -- codec declared 2 bytes, "
89
+
"EverParse validator returned %llu. Fix the OCaml codec's "
90
+
"wire_size or the .3d projection.\n",
91
+
(unsigned long long) r);
92
+
return 2;
93
+
}
94
+
CHECK("zero buffer validates", EverParseIsSuccess(r));
95
+
CHECK("position advanced to 2", r == 2);
96
+
97
+
r = CfdpAckValidateCfdpAck((WIRECTX *) &ctx, NULL, counting_error_handler, buf, 4, 0);
98
+
CHECK("larger buffer validates", EverParseIsSuccess(r));
99
+
CHECK("position is 2 not 4", r == 2);
100
+
101
+
for (uint64_t len = 0; len < 2; len++) {
102
+
error_count = 0;
103
+
r = CfdpAckValidateCfdpAck((WIRECTX *) &ctx, NULL, counting_error_handler, buf, len, 0);
104
+
CHECK("truncated to len fails", EverParseIsError(r));
105
+
}
106
+
107
+
r = CfdpAckValidateCfdpAck((WIRECTX *) &ctx, NULL, counting_error_handler, buf, 0, 0);
108
+
CHECK("empty input fails", EverParseIsError(r));
109
+
110
+
srand(42);
111
+
for (int i = 0; i < 1000; i++) {
112
+
for (int j = 0; j < 2; j++)
113
+
buf[j] = (uint8_t)(rand() & 0xff);
114
+
r = CfdpAckValidateCfdpAck((WIRECTX *) &ctx, NULL, counting_error_handler, buf, 2, 0);
115
+
CHECK("random buffer validates", EverParseIsSuccess(r));
116
+
CHECK("random position correct", r == 2);
117
+
}
118
+
119
+
(void) ctx;
120
+
printf("cfdpack: %d passed, %d failed\n", pass, fail);
121
+
failures += fail;
122
+
}
123
+
124
+
/* CfdpPrompt (1 bytes) */
125
+
{
126
+
int pass = 0, fail = 0;
127
+
uint8_t buf[1];
128
+
uint64_t r;
129
+
CfdpPromptFields ctx = {0};
130
+
131
+
memset(buf, 0, 1);
132
+
r = CfdpPromptValidateCfdpPrompt((WIRECTX *) &ctx, NULL, counting_error_handler, buf, 1, 0);
133
+
if (!EverParseIsSuccess(r) || r != 1) {
134
+
fprintf(stderr,
135
+
"FATAL: CfdpPrompt wire_size mismatch -- codec declared 1 bytes, "
136
+
"EverParse validator returned %llu. Fix the OCaml codec's "
137
+
"wire_size or the .3d projection.\n",
138
+
(unsigned long long) r);
139
+
return 2;
140
+
}
141
+
CHECK("zero buffer validates", EverParseIsSuccess(r));
142
+
CHECK("position advanced to 1", r == 1);
143
+
144
+
r = CfdpPromptValidateCfdpPrompt((WIRECTX *) &ctx, NULL, counting_error_handler, buf, 2, 0);
145
+
CHECK("larger buffer validates", EverParseIsSuccess(r));
146
+
CHECK("position is 1 not 2", r == 1);
147
+
148
+
for (uint64_t len = 0; len < 1; len++) {
149
+
error_count = 0;
150
+
r = CfdpPromptValidateCfdpPrompt((WIRECTX *) &ctx, NULL, counting_error_handler, buf, len, 0);
151
+
CHECK("truncated to len fails", EverParseIsError(r));
152
+
}
153
+
154
+
r = CfdpPromptValidateCfdpPrompt((WIRECTX *) &ctx, NULL, counting_error_handler, buf, 0, 0);
155
+
CHECK("empty input fails", EverParseIsError(r));
156
+
157
+
srand(42);
158
+
for (int i = 0; i < 1000; i++) {
159
+
for (int j = 0; j < 1; j++)
160
+
buf[j] = (uint8_t)(rand() & 0xff);
161
+
r = CfdpPromptValidateCfdpPrompt((WIRECTX *) &ctx, NULL, counting_error_handler, buf, 1, 0);
162
+
CHECK("random buffer validates", EverParseIsSuccess(r));
163
+
CHECK("random position correct", r == 1);
164
+
}
165
+
166
+
(void) ctx;
167
+
printf("cfdpprompt: %d passed, %d failed\n", pass, fail);
168
+
failures += fail;
169
+
}
170
+
171
+
if (failures == 0)
172
+
printf("All tests passed.\n");
173
+
else
174
+
printf("%d test(s) failed.\n", failures);
175
+
return failures ? 1 : 0;
176
+
}