CCSDS File Delivery Protocol (CCSDS 727.0-B-5) for space file transfer
irmin: rewrite proof.mli — concise, precise, no research notes
+25
-15
+25
-15
lib/cfdp.ml
+25
-15
lib/cfdp.ml
···
1020
1020
let src_len = String.length meta.source_filename in
1021
1021
let dst_len = String.length meta.dest_filename in
1022
1022
let total = 1 + fss_len + 1 + src_len + 1 + dst_len in
1023
-
let packed =
1024
-
{
1025
-
pm_closure = (if meta.closure_requested then 1 else 0);
1026
-
pm_reserved = 0;
1027
-
pm_checksum_type = int_of_checksum_type meta.checksum_type;
1028
-
pm_file_size = int64_to_be_bytes fss_len meta.file_size;
1029
-
pm_src_len = src_len;
1030
-
pm_src_name = meta.source_filename;
1031
-
pm_dst_len = dst_len;
1032
-
pm_dst_name = meta.dest_filename;
1033
-
}
1034
-
in
1035
-
let payload = Bytes.create total in
1036
-
Wire.Codec.encode metadata_codec packed payload 0;
1037
1023
let code = String.make 1 (Char.chr (int_of_directive_code Dir_metadata)) in
1038
-
code ^ Bytes.to_string payload
1024
+
(* Encode manually: the Wire codec does not support parameterised encoding,
1025
+
so variable-size FSS fields must be laid out by hand. *)
1026
+
let buf = Bytes.create total in
1027
+
let off = ref 0 in
1028
+
(* closure(1) | reserved(3) | checksum_type(4) *)
1029
+
let byte0 =
1030
+
((if meta.closure_requested then 1 else 0) lsl 6)
1031
+
lor int_of_checksum_type meta.checksum_type
1032
+
in
1033
+
Bytes.set_uint8 buf !off byte0;
1034
+
incr off;
1035
+
(* file size (FSS) *)
1036
+
let fss = int64_to_be_bytes fss_len meta.file_size in
1037
+
Bytes.blit_string fss 0 buf !off fss_len;
1038
+
off := !off + fss_len;
1039
+
(* source filename LV *)
1040
+
Bytes.set_uint8 buf !off src_len;
1041
+
incr off;
1042
+
Bytes.blit_string meta.source_filename 0 buf !off src_len;
1043
+
off := !off + src_len;
1044
+
(* dest filename LV *)
1045
+
Bytes.set_uint8 buf !off dst_len;
1046
+
incr off;
1047
+
Bytes.blit_string meta.dest_filename 0 buf !off dst_len;
1048
+
code ^ Bytes.to_string buf
1039
1049
1040
1050
let encode_nak ~large_file nak_pdu =
1041
1051
let fss_len = if large_file then 8 else 4 in