Allow checking of PC in postcondition

Can be used to check the following properties:
- code finalsied correctly: END_P#
- code finalised in the fault ahndler: FH_END_P#
- code finalised in an infinite loop: loop label

Author: diaolo01

herd/AArch64Arch_herd.ml

@@ -512,6 +512,7 @@ module Make (C:Arch_herd.Config)(V:Value.AArch64) =
           let endian = endian
 
           type arch_reg = reg
+          let pc_reg = Some PC
           let pp_reg = pp_reg
           let reg_compare = reg_compare
 

herd/ARMArch_herd.ml

@@ -135,6 +135,7 @@ module Make (C:Arch_herd.Config) (V:Value.S) =
           let endian = endian
 
           type arch_reg = reg
+          let pc_reg = None
           let pp_reg = pp_reg
           let reg_compare = reg_compare
 

herd/ASLExtra.ml

@@ -51,6 +51,7 @@ module Make (B : ArchBaseHerd) (C : Arch_herd.Config) (V : Value.S) = struct
 
         type arch_reg = reg
 
+        let pc_reg = None
         let endian = endian
         let pp_reg = pp_reg
         let reg_compare = reg_compare

herd/BPFArch_herd.ml

@@ -94,6 +94,7 @@ struct
 
         type arch_reg = reg
 
+        let pc_reg = None
         let pp_reg = pp_reg
         let reg_compare = reg_compare
         let fromto_of_instr _ = None

herd/BellArch_herd.ml

@@ -46,6 +46,7 @@ module Make
         let endian = endian
 
         type arch_reg = reg
+        let pc_reg = None
         let pp_reg = pp_reg
         let reg_compare = reg_compare
 

herd/CArch_herd.ml

@@ -40,6 +40,7 @@ module Make (C:Arch_herd.Config) (V:Value.S) = struct
         let endian = endian
 
         type arch_reg = reg
+        let pc_reg = None
         let pp_reg = pp_reg
         let reg_compare = reg_compare
 

herd/JavaArch_herd.ml

@@ -38,6 +38,7 @@ module Make (C:Arch_herd.Config) (V:Value.S) = struct
         module V = V
         let endian            = endian
         type arch_reg         = reg
+        let pc_reg            = None
         let pp_reg            = pp_reg
         let reg_compare       = reg_compare
         let fromto_of_instr _ = None

herd/MIPSArch_herd.ml

@@ -68,9 +68,10 @@ module Make
 
           let endian = endian
 
-	  type arch_reg = reg
-	  let pp_reg = pp_reg
-	  let reg_compare = reg_compare
+          type arch_reg = reg
+          let pc_reg = None
+          let pp_reg = pp_reg
+          let reg_compare = reg_compare
 
           let fromto_of_instr _ = None
 

herd/PPCArch_herd.ml

@@ -92,6 +92,7 @@ module Make (C:Arch_herd.Config) (V:Value.S)
           let endian = endian
 
           type arch_reg = reg
+          let pc_reg = None
           let pp_reg = pp_reg
           let reg_compare = reg_compare
 

herd/RISCVArch_herd.ml

@@ -131,6 +131,7 @@ module Make (C:Arch_herd.Config) (V:Value.S) =
           let endian = endian
 
           type arch_reg = reg
+          let pc_reg = None
           let pp_reg = pp_reg
           let reg_compare = reg_compare