Use generated actual decoders for ARM table:

src/trusted/validator_arm/armv7.table

Index: src/trusted/validator_arm/armv7.table
===================================================================
--- src/trusted/validator_arm/armv7.table	(revision 10736)
+++ src/trusted/validator_arm/armv7.table	(working copy)
@@ -1780,7 +1780,7 @@
   { cond(31:28), W(21), Rn(19:16), register_list(15:0) }
   registers := RegisterList(register_list); wback := W=1;
   base := Rn;
-  small_imm_base_wb := true;
+  small_imm_base_wb := wback;
   safety := Rn == Pc | NumGPRs(registers) < 1 => UNPREDICTABLE;
 *LdRnRegs *RnRegs
   baseline := LoadRegisterList;
@@ -1803,7 +1803,7 @@
   defs := {Pc};
   uses := {Pc};
   relative := true;
-  relative_offset := imm32;
+  relative_offset := imm32 + 8;  # r15 is 8 bytes ahead of instruction address.

[JF, 2013/02/11 19:40:38]

I'd change the comment to be the same as other places in the code that do this:

The ARM manual states that "PC reads as the address of the current instruction
plus 8".

[Karl, 2013/02/11 22:12:43]

Done.

   safety := true => MAY_BE_SAFE;
 *BranchLink *Branch
   defs := {Pc, Lr};