package linksem
A formalisation of the core ELF and DWARF file formats written in Lem
Install
Dune Dependency
Authors
Maintainers
Sources
0.8.tar.gz
md5=2075c56715539b3b8f54ae65cc808b8c
sha512=f7c16e4036a1440a6a8d13707a43f0f9f9db0c68489215f948cc300b6a164dba5bf852e58f89503e9d9f38180ee658d9478156ca1a1ef64d6861eec5f9cf43d2
doc/src/linksem_zarith/byte_pattern_extra.ml.html
Source file byte_pattern_extra.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100
(*Generated by Lem from byte_pattern_extra.lem.*) open Lem_basic_classes open Lem_string open Lem_maybe open Lem_num open Lem_bool open Byte_pattern open Missing_pervasives open Show type byte_pattern_compare_result = | BytePatternMatch | BytePatternMismatch of (Nat_big_num.num * string) let rec compare_byte_pattern' dict_Basic_classes_Eq_a dict_Show_Show_a offset core_bp binary_bp:byte_pattern_compare_result= ((match (core_bp, binary_bp) with | (_, []) -> BytePatternMatch | ((Some core_b)::core_bp, (Some binary_b)::binary_bp) -> if dict_Basic_classes_Eq_a.isInequal_method core_b binary_b then let err_msg = ("compare_byte_pattern: mismatch at offset 0x" ^ ((hex_string_of_natural offset) ^ (": byte " ^ (( dict_Show_Show_a.show_method core_b) ^ (" vs. " ^ ( dict_Show_Show_a.show_method binary_b)))))) in BytePatternMismatch (offset, err_msg) else compare_byte_pattern' dict_Basic_classes_Eq_a dict_Show_Show_a ( Nat_big_num.add offset( (Nat_big_num.of_int 1))) core_bp binary_bp | (_::core_bp, None::binary_bp) -> compare_byte_pattern' dict_Basic_classes_Eq_a dict_Show_Show_a ( Nat_big_num.add offset( (Nat_big_num.of_int 1))) core_bp binary_bp | (maybe_core_b::_, maybe_binary_b::_) -> let err_msg = ("compare_byte_pattern: mismatch at offset 0x" ^ ((hex_string_of_natural offset) ^ (": " ^ ((string_of_maybe dict_Show_Show_a maybe_core_b) ^ (" vs. " ^ (string_of_maybe dict_Show_Show_a maybe_binary_b)))))) in BytePatternMismatch (offset, err_msg) | (_, _) -> let err_msg = ("compare_byte_pattern: mismatch at offset 0x" ^ ((hex_string_of_natural offset) ^ ": length mismatch")) in BytePatternMismatch (offset, err_msg) )) (*val compare_byte_pattern : byte_pattern -> byte_pattern -> byte_pattern_compare_result*) let compare_byte_pattern:((char)option)list ->((char)option)list ->byte_pattern_compare_result= (compare_byte_pattern' instance_Basic_classes_Eq_var_dict instance_Show_Show_Missing_pervasives_byte_dict( (Nat_big_num.of_int 0))) (*val print_byte_pattern_line' : natural -> natural -> byte_pattern -> unit*) let rec print_byte_pattern_line' offset len bp:unit= (if Nat_big_num.equal len( (Nat_big_num.of_int 0)) then () else let (s, bp) = ((match bp with | [] -> (" ", []) | maybe_b::bp -> let s = ((match maybe_b with | None -> "--" | Some b -> hex_string_of_byte b )) in (s, bp) )) in let s = (if Nat_big_num.equal (Nat_big_num.modulus offset( (Nat_big_num.of_int 2)))( (Nat_big_num.of_int 1)) && Nat_big_num.greater ( Nat_big_num.sub_nat len( (Nat_big_num.of_int 1)))( (Nat_big_num.of_int 0)) then s ^ " " else s) in let _ = (prerr_string s) in print_byte_pattern_line' ( Nat_big_num.add offset( (Nat_big_num.of_int 1))) ( Nat_big_num.sub_nat len( (Nat_big_num.of_int 1))) bp) (*val print_byte_pattern_line : natural -> byte_pattern -> unit*) let print_byte_pattern_line:Nat_big_num.num ->byte_pattern ->unit= (print_byte_pattern_line'( (Nat_big_num.of_int 0))) (*val fixed_hex_string_of_natural : natural -> natural -> string*) let rec fixed_hex_string_of_natural len n:string= (if Nat_big_num.equal len( (Nat_big_num.of_int 0)) then "" else (fixed_hex_string_of_natural ( Nat_big_num.sub_nat len( (Nat_big_num.of_int 1))) ( Nat_big_num.div n( (Nat_big_num.of_int 16)))) ^ (Xstring.implode [Missing_pervasives.hex_char_of_nibble ( Nat_big_num.modulus n( (Nat_big_num.of_int 16)))])) let print_byte_pattern_addr_size : Nat_big_num.num= ( (Nat_big_num.of_int 12)) let print_byte_pattern_line_size : Nat_big_num.num= ( (Nat_big_num.of_int 16)) (*val print_byte_pattern : natural -> byte_pattern -> unit*) let rec print_byte_pattern start bp:unit= (if (Lem_list.listEqualBy (Lem.option_equal (=)) bp []) then () else let _ = (prerr_string ((fixed_hex_string_of_natural print_byte_pattern_addr_size start) ^ " ")) in let (line, bp) = (Lem_list.split_at (Nat_big_num.to_int print_byte_pattern_line_size) bp) in let _ = (print_byte_pattern_line print_byte_pattern_line_size line) in let _ = (prerr_string "\n") in print_byte_pattern ( Nat_big_num.add start print_byte_pattern_line_size) bp) (*val print_two_byte_patterns : natural -> byte_pattern -> byte_pattern -> unit*) let rec print_two_byte_patterns start bp1 bp2:unit= (if (Lem_list.listEqualBy (Lem.option_equal (=)) bp1 []) && (Lem_list.listEqualBy (Lem.option_equal (=)) bp2 []) then () else let was_bp1_empty = (Lem_list.listEqualBy (Lem.option_equal (=)) bp1 []) in (* If only bp1 is empty, print one extra line *) let _ = (prerr_string ((fixed_hex_string_of_natural print_byte_pattern_addr_size start) ^ " | ")) in let (line1, bp1) = (Lem_list.split_at (Nat_big_num.to_int print_byte_pattern_line_size) bp1) in let (line2, bp2) = (Lem_list.split_at (Nat_big_num.to_int print_byte_pattern_line_size) bp2) in let _ = (print_byte_pattern_line print_byte_pattern_line_size line1) in let _ = (prerr_string " | ") in let _ = (print_byte_pattern_line print_byte_pattern_line_size line2) in let _ = ((match compare_byte_pattern line2 line1 with | BytePatternMatch -> () | BytePatternMismatch (_, err_msg) -> prerr_string " X" (* Missing_pervasives.errs (" " ^ err_msg) *) )) in let _ = (prerr_string "\n") in if was_bp1_empty then prerr_endline " | | […] " else print_two_byte_patterns ( Nat_big_num.add start print_byte_pattern_line_size) bp1 bp2)
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>