remove old elf sources

1 files changed, 0 insertions, 147 deletions

diff --git a/src/elf_model/elf_file1.lem b/src/elf_model/elf_file1.lem
deleted file mode 100644
index 16ad63a3..00000000
--- a/src/elf_model/elf_file1.lem
+++ /dev/null
@@ -1,147 +0,0 @@
-open import Basic_classes
-open import Bool
-open import String
-
-open import Endianness
-
-open import Elf_header
-open import Elf_types
-
-open import Bitstring
-open import Error
-open import Missing_pervasives
-open import Show
-
-(** Type [elf32_file1] represents the first lazy unfolding of the structure
-  * of an ELF file, wherein the ELF header is populated and all other data
-  * is left uninterpreted.
-  *)
-type elf32_file1 =
-  <| elf32_file1_header : elf32_header (** The ELF header (mandatory) *)
-   ; elf32_file1_body   : bitstring    (** Uninterpreted data *)
-   |>
-
-class (HasElf32File1 'a)
-  val get_elf32_file1 : 'a -> elf32_file1
-end
-
-instance (HasElf32File1 elf32_file1)
-  let get_elf32_file1 f1 = f1
-end
-
-instance (HasElf32Header elf32_file1)
-  let get_elf32_header file1 = file1.elf32_file1_header
-end
-
-(** Type [elf64_file1] represents the first lazy unfolding of the structure
-  * of an ELF file, wherein the ELF header is populated and all other data
-  * is left uninterpreted.
-  *)
-type elf64_file1 =
-  <| elf64_file1_header : elf64_header (** The ELF header (mandatory) *)
-   ; elf64_file1_body   : bitstring    (** Uninterpreted data *)
-   |>
-
-class (HasElf64File1 'a)
-  val get_elf64_file1 : 'a -> elf64_file1
-end
-
-instance (HasElf64File1 elf64_file1)
-  let get_elf64_file1 f1 = f1
-end
-
-instance (HasElf64Header elf64_file1)
-  let get_elf64_header file1 = file1.elf64_file1_header
-end
-
-val string_of_elf32_file1 : hdr_print_bundle -> elf32_file1 -> string
-let string_of_elf32_file1 hdr_bdl f1 =
-  unlines [
-    "\n*Type elf32_file1:"
-  ; "**Header:"
-  ; string_of_elf32_header hdr_bdl f1.elf32_file1_header
-  ; "Body:"
-  ; "\tUninterpreted data of length " ^ show (Bitstring.length f1.elf32_file1_body)
-  ]
-
-val string_of_elf64_file1 : hdr_print_bundle -> elf64_file1 -> string
-let string_of_elf64_file1 hdr_bdl f1 =
-  unlines [
-    "\n*Type elf64_file1:"
-  ; "**Header:"
-  ; string_of_elf64_header hdr_bdl f1.elf64_file1_header
-  ; "Body:"
-  ; "\tUninterpreted data of length " ^ show (Bitstring.length f1.elf64_file1_body)
-  ]
-
-(** [is_executable_efl32_file1] tests whether the ELF file is an executable
-  * file type.
-  *)
-val is_executable_elf32_file1 : elf32_file1 -> bool
-let is_executable_elf32_file1 f1 =
-  nat_of_elf32_half f1.elf32_file1_header.elf32_type = elf_ft_exec
-
-(** [is_executable_efl64_file1] tests whether the ELF file is an executable
-  * file type.
-  *)
-val is_executable_elf64_file1 : elf64_file1 -> bool
-let is_executable_elf64_file1 f1 =
-  nat_of_elf64_half f1.elf64_file1_header.elf64_type = elf_ft_exec
-
-(** [is_shared_object_elf32_file1] tests whether the ELF file is a shared object
-  * file type.
-  *)
-val is_shared_object_elf32_file1 : elf32_file1 -> bool
-let is_shared_object_elf32_file1 f1 =
-  nat_of_elf32_half f1.elf32_file1_header.elf32_type = elf_ft_dyn
-
-(** [is_shared_object_elf64_file1] tests whether the ELF file is a shared object
-* file type.
-*)
-val is_shared_object_elf64_file1 : elf64_file1 -> bool
-let is_shared_object_elf64_file1 f1 =
-  nat_of_elf64_half f1.elf64_file1_header.elf64_type = elf_ft_dyn
-
-(** [is_relocatable_elf32_file1] tests whether the ELF file is a relocatable
-* file type.
-*)
-val is_relocatable_elf32_file1 : elf32_file1 -> bool
-let is_relocatable_elf32_file1 f1 =
-  nat_of_elf32_half f1.elf32_file1_header.elf32_type = elf_ft_rel
-
-(** [is_relocatable_elf64_file1] tests whether the ELF file is a relocatable
-* file type.
-*)
-val is_relocatable_elf64_file1 : elf64_file1 -> bool
-let is_relocatable_elf64_file1 f1 =
-  nat_of_elf64_half f1.elf64_file1_header.elf64_type = elf_ft_rel
-
-(** [is_linkable_elf32_file1] tests whether the ELF file is a linkable (shared
-  * object or relocatable) file type.
-  *)
-val is_linkable_elf32_file1 : elf32_file1 -> bool
-let is_linkable_elf32_file1 f1 =
-  is_shared_object_elf32_file1 f1 || is_relocatable_elf32_file1 f1
-
-(** [is_linkable_elf64_file1] tests whether the ELF file is a linkable (shared
-  * object or relocatable) file type.
-  *)
-val is_linkable_elf64_file1 : elf64_file1 -> bool
-let is_linkable_elf64_file1 f1 =
-  is_shared_object_elf64_file1 f1 || is_relocatable_elf64_file1 f1
-
-(** [read_elf32_file1 bs] lazily unfolds [bs] revealing the ELF file's header,
-  * leaving all other data uninterpreted.
-  *)
-val read_elf32_file1 : bitstring -> error elf32_file1
-let read_elf32_file1 bs0 =
-  read_elf32_header bs0 >>= fun (hdr, bs1) ->
-  return <| elf32_file1_header = hdr; elf32_file1_body = bs0 |>
-
-(** [read_elf64_file1 bs] lazily unfolds [bs] revealing the ELF file's header,
-  * leaving all other data uninterpreted.
-  *)
-val read_elf64_file1 : bitstring -> error elf64_file1
-let read_elf64_file1 bs0 =
-  read_elf64_header bs0 >>= fun (hdr, bs1) ->
-  return <| elf64_file1_header = hdr; elf64_file1_body = bs0 |>
\ No newline at end of file