checklink: first import of Valentin Robert's validator for asm and link

cparser: renamed Errors to Cerrors; removed packing into Cparser.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1856 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 32 insertions, 0 deletions

diff --git a/checklink/PPC_utils.ml b/checklink/PPC_utils.ml
new file mode 100644
index 0000000..086d1c2
--- /dev/null
+++ b/checklink/PPC_utils.ml
@@ -0,0 +1,32 @@
+open ELF_types
+open ELF_utils
+open Library
+open PPC_parsers
+open PPC_types
+
+let code_at_vaddr (e: elf) (vaddr: int32) (nb_instr: int): ecode option =
+  match section_at_vaddr e vaddr with
+  | None -> None
+  | Some(sndx) ->
+      let code_bs =
+        bitstring_at_vaddr e sndx vaddr (32 * nb_instr) in
+      Some (parse_code_as_list code_bs)
+
+let code_of_sym_ndx (e: elf) (ndx: int): ecode option =
+  let sym = e.e_symtab.(ndx) in
+  match sym.st_type with
+  | STT_FUNC ->
+      let sym_vaddr = sym.st_value in
+      let sym_size = 8 * (int32_int sym.st_size) in
+      let sym_sndx = sym.st_shndx in
+      let code_bs =
+        bitstring_at_vaddr e sym_sndx sym_vaddr sym_size in
+      Some (parse_code_as_list code_bs)
+  | _ -> None
+
+let code_of_sym_name (e: elf) (name: string): ecode option =
+  match ndx_of_sym_name e name with
+  | Some ndx -> code_of_sym_ndx e ndx
+  | None     -> None
+
+