From 396039a7307bb9569e71fc23628f3e1e2ce852dc Mon Sep 17 00:00:00 2001 From: Alejandro Gomez-Londono Date: Fri, 28 Apr 2017 22:21:59 +1000 Subject: [PATCH] arm-hyp crefine: fixes get_gic_vcpu_ctrl_lr machine op + others * others: fix arg name in get_gic_vcpu_ctrl_eisr0 get_gic_vcpu_ctrl_eisr1 and get_gic_vcpu_ctrl_misr --- proof/crefine/ARM_HYP/Machine_C.thy | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/proof/crefine/ARM_HYP/Machine_C.thy b/proof/crefine/ARM_HYP/Machine_C.thy index 67a2cfc87..2de0806cc 100644 --- a/proof/crefine/ARM_HYP/Machine_C.thy +++ b/proof/crefine/ARM_HYP/Machine_C.thy @@ -324,13 +324,13 @@ assumes get_gic_vcpu_ctrl_vtr_ccorres: "ccorres (op =) ret__unsigned_long_' \ UNIV [] (doMachineOp get_gic_vcpu_ctrl_vtr) (Call get_gic_vcpu_ctrl_vtr_'proc)" assumes get_gic_vcpu_ctrl_eisr0_ccorres: - "ccorres (op =) ret__unsigned_long_' \ UNIV [] + "ccorres (op =) ret__unsigned_' \ UNIV [] (doMachineOp get_gic_vcpu_ctrl_eisr0) (Call get_gic_vcpu_ctrl_eisr0_'proc)" assumes get_gic_vcpu_ctrl_eisr1_ccorres: - "ccorres (op =) ret__unsigned_long_' \ UNIV [] + "ccorres (op =) ret__unsigned_' \ UNIV [] (doMachineOp get_gic_vcpu_ctrl_eisr1) (Call get_gic_vcpu_ctrl_eisr1_'proc)" assumes get_gic_vcpu_ctrl_misr_ccorres: - "ccorres (op =) ret__unsigned_long_' \ UNIV [] + "ccorres (op =) ret__unsigned_' \ UNIV [] (doMachineOp get_gic_vcpu_ctrl_misr) (Call get_gic_vcpu_ctrl_misr_'proc)" assumes set_gic_vcpu_ctrl_hcr_ccorres: @@ -348,7 +348,7 @@ assumes set_gic_vcpu_ctrl_lr_ccorres: (doMachineOp (set_gic_vcpu_ctrl_lr n lr)) (Call set_gic_vcpu_ctrl_lr_'proc)" assumes get_gic_vcpu_ctrl_lr_ccorres: - "ccorres (op =) ret__unsigned_long_' \ (\\num = scast n \) [] + "ccorres (\v virq. virq = virq_C (FCP (\_. v))) ret__struct_virq_C_' \ (\\num = scast n \) hs (doMachineOp (get_gic_vcpu_ctrl_lr n)) (Call get_gic_vcpu_ctrl_lr_'proc)" (* The following are fastpath specific assumptions.