diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-12-01 10:20:03 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-12-01 10:20:03 +0100 |
| commit | 114b2b5634a97e60e2590d20eac072594d846206 (patch) | |
| tree | aa1820e0befd4fba78cf418acb6a5b70e0e06583 /checklink | |
| parent | c3b615f875ed2cf8418453c79c4621d2dc61b0a0 (diff) | |
| download | compcert-114b2b5634a97e60e2590d20eac072594d846206.tar.gz compcert-114b2b5634a97e60e2590d20eac072594d846206.zip | |
Changed the comparison of jumptables.
Diffstat (limited to 'checklink')
| -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 = |