diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-12-02 17:24:06 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-12-02 17:24:06 +0100 |
| commit | 5435a0ac12625b356ecbd9faba1c7ec67f2477a7 (patch) | |
| tree | 758223ef60c6f0f263fce9d90e947bf00db3b464 | |
| parent | e62820c430e52fa72edd6f1c21bd867eb0f3c467 (diff) | |
| parent | 114b2b5634a97e60e2590d20eac072594d846206 (diff) | |
| download | compcert-5435a0ac12625b356ecbd9faba1c7ec67f2477a7.tar.gz compcert-5435a0ac12625b356ecbd9faba1c7ec67f2477a7.zip | |
Merge branch 'master' into dwarf
| -rw-r--r-- | checklink/Check.ml | 21 |
1 files changed, 7 insertions, 14 deletions
diff --git a/checklink/Check.ml b/checklink/Check.ml index 5213b266..0876f881 100644 --- a/checklink/Check.ml +++ b/checklink/Check.ml @@ -556,21 +556,14 @@ let rec match_jmptbl lbllist vaddr size ffw = ) in let elf = ffw.sf.ef.elf in - begin match section_at_vaddr elf vaddr with + begin match bitstring_at_vaddr elf vaddr size with | None -> ERR("No section for the jumptable") - | Some(sndx) -> - begin match bitstring_at_vaddr elf vaddr size with - | None -> ERR("") - | Some(bs, pofs, psize) -> - ffw - >>> (ff_sf ^%= - match_sections_name jmptbl_section elf.e_shdra.(sndx).sh_name - ) - >>> match_jmptbl_aux lbllist bs - >>^ (ff_ef ^%= - add_range pofs psize 0 Jumptable - ) - end + | Some(bs, pofs, psize) -> + ffw + >>> match_jmptbl_aux lbllist bs + >>^ (ff_ef ^%= + add_range pofs psize 0 Jumptable + ) end let match_bo_bt_bool bo = |