refactor(lib): restore COMPILER_ASSERT for CBMC
COMPILER_ASSERT is a useful tool for CBMC to detect issues that can
lead to assert failures. A previous commit completely turned off
COMPILER_ASSERT because some alignment and structure size requirements
are not fulfilled by the CBMC configuration.
This commit introduces a new macro COMPILER_ASSERT_NO_CBMC to be used
when an assertion is only valid in regular build, but not in CBMC build.
Change-Id: I20cd80bd5ca86ee92407c92e26ac2c99698a3e05
Signed-off-by: Mate Toth-Pal <mate.toth-pal@arm.com>
diff --git a/docs/process/coding-standard.rst b/docs/process/coding-standard.rst
index 28800bf..1c39113 100644
--- a/docs/process/coding-standard.rst
+++ b/docs/process/coding-standard.rst
@@ -372,6 +372,14 @@
10 | COMPILER_ASSERT(MY_STRUCT_SIZE == sizeof(struct my_struct));
| ^~~~~~~~~~~~~~~
+.. note::
+
+ For CBMC analysis some of the compile assertions are not valid (for example
+ due to the missing padding from certain structures, or due to smaller
+ ``GRANULE_SIZE``). In this case the macro ``COMPILER_ASSERT_NO_CBMC`` should
+ be used which behaves as ``COMPILER_ASSERT`` for regular builds, and always
+ passes for CBMC build.
+
Data types, structures and typedefs
-----------------------------------
diff --git a/lib/arch/include/simd.h b/lib/arch/include/simd.h
index bed7065..109b3d5 100644
--- a/lib/arch/include/simd.h
+++ b/lib/arch/include/simd.h
@@ -178,10 +178,10 @@
* TODO: Auto generate header file simd-asm-offsets.h during build and use it
* in assembly routines.
*/
-COMPILER_ASSERT((U(offsetof(struct fpu_regs, q))) == FPU_REGS_OFFSET_Q);
-COMPILER_ASSERT((U(offsetof(struct sve_regs, z))) == SVE_REGS_OFFSET_Z);
-COMPILER_ASSERT((U(offsetof(struct sve_regs, p))) == SVE_REGS_OFFSET_P);
-COMPILER_ASSERT((U(offsetof(struct sve_regs, ffr))) == SVE_REGS_OFFSET_FFR);
+COMPILER_ASSERT_NO_CBMC((U(offsetof(struct fpu_regs, q))) == FPU_REGS_OFFSET_Q);
+COMPILER_ASSERT_NO_CBMC((U(offsetof(struct sve_regs, z))) == SVE_REGS_OFFSET_Z);
+COMPILER_ASSERT_NO_CBMC((U(offsetof(struct sve_regs, p))) == SVE_REGS_OFFSET_P);
+COMPILER_ASSERT_NO_CBMC((U(offsetof(struct sve_regs, ffr))) == SVE_REGS_OFFSET_FFR);
/* Initialize SIMD layer based on CPU support for FPU or SVE */
void simd_init(void);
diff --git a/lib/common/include/utils_def.h b/lib/common/include/utils_def.h
index 89d8272..8628b66 100644
--- a/lib/common/include/utils_def.h
+++ b/lib/common/include/utils_def.h
@@ -106,7 +106,6 @@
(_a)[_i] = (_v); \
})
-#ifndef CBMC
#define COMPILER_ASSERT(_condition) \
extern char compiler_assert[(_condition) ? 1 : -1]
@@ -125,10 +124,10 @@
#define CHECK_TYPE_IS_ARRAY(_v) \
COMPILER_ASSERT_ZERO(!__builtin_types_compatible_p(typeof(_v), \
typeof(&((_v)[0]))))
+#ifdef CBMC
+#define COMPILER_ASSERT_NO_CBMC(_condition) COMPILER_ASSERT(0 == 0)
#else /* CBMC */
-#define COMPILER_ASSERT(_condition) extern char disabled_compiler_assert[1]
-#define COMPILER_ASSERT_ZERO(_expr) extern char disabled_compiler_assert[1]
-#define CHECK_TYPE_IS_ARRAY(_v) 1
+#define COMPILER_ASSERT_NO_CBMC(_condition) COMPILER_ASSERT(_condition)
#endif /* CBMC */
#define IS_POWER_OF_TWO(x) \
diff --git a/lib/measurement/src/measurement_descs.h b/lib/measurement/src/measurement_descs.h
index caac98b..5cc126f 100644
--- a/lib/measurement/src/measurement_descs.h
+++ b/lib/measurement/src/measurement_descs.h
@@ -27,14 +27,14 @@
*/
SET_MEMBER(unsigned char content[MAX_MEASUREMENT_SIZE], 0x60, 0x100);
};
-COMPILER_ASSERT(sizeof(struct measurement_desc_data) == 0x100UL);
+COMPILER_ASSERT_NO_CBMC(sizeof(struct measurement_desc_data) == 0x100UL);
-COMPILER_ASSERT(U(offsetof(struct measurement_desc_data, desc_type)) == 0x0U);
-COMPILER_ASSERT(U(offsetof(struct measurement_desc_data, len)) == 0x8U);
-COMPILER_ASSERT(U(offsetof(struct measurement_desc_data, rim)) == 0x10U);
-COMPILER_ASSERT(U(offsetof(struct measurement_desc_data, ipa)) == 0x50U);
-COMPILER_ASSERT(U(offsetof(struct measurement_desc_data, flags)) == 0x58U);
-COMPILER_ASSERT(U(offsetof(struct measurement_desc_data, content)) == 0x60U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct measurement_desc_data, desc_type)) == 0x0U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct measurement_desc_data, len)) == 0x8U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct measurement_desc_data, rim)) == 0x10U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct measurement_desc_data, ipa)) == 0x50U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct measurement_desc_data, flags)) == 0x58U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct measurement_desc_data, content)) == 0x60U);
/* RmmMeasurementDescriptorRec type as per RMM spec */
struct measurement_desc_rec {
@@ -47,12 +47,12 @@
/* Hash of 4KB page which contains REC parameters data structure */
SET_MEMBER(unsigned char content[MAX_MEASUREMENT_SIZE], 0x50, 0x100);
};
-COMPILER_ASSERT(sizeof(struct measurement_desc_rec) == 0x100UL);
+COMPILER_ASSERT_NO_CBMC(sizeof(struct measurement_desc_rec) == 0x100UL);
-COMPILER_ASSERT(U(offsetof(struct measurement_desc_rec, desc_type)) == 0x0U);
-COMPILER_ASSERT(U(offsetof(struct measurement_desc_rec, len)) == 0x8U);
-COMPILER_ASSERT(U(offsetof(struct measurement_desc_rec, rim)) == 0x10U);
-COMPILER_ASSERT(U(offsetof(struct measurement_desc_rec, content)) == 0x50U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct measurement_desc_rec, desc_type)) == 0x0U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct measurement_desc_rec, len)) == 0x8U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct measurement_desc_rec, rim)) == 0x10U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct measurement_desc_rec, content)) == 0x50U);
/* RmmMeasurementDescriptorRipas type as per RMM spec */
struct measurement_desc_ripas {
@@ -67,12 +67,12 @@
/* Top IPA at which the RIPAS change occurred */
SET_MEMBER(unsigned long top, 0x58, 0x100);
};
-COMPILER_ASSERT(sizeof(struct measurement_desc_ripas) == 0x100UL);
+COMPILER_ASSERT_NO_CBMC(sizeof(struct measurement_desc_ripas) == 0x100UL);
-COMPILER_ASSERT(U(offsetof(struct measurement_desc_ripas, desc_type)) == 0x0U);
-COMPILER_ASSERT(U(offsetof(struct measurement_desc_ripas, len)) == 0x8U);
-COMPILER_ASSERT(U(offsetof(struct measurement_desc_ripas, rim)) == 0x10U);
-COMPILER_ASSERT(U(offsetof(struct measurement_desc_ripas, base)) == 0x50U);
-COMPILER_ASSERT(U(offsetof(struct measurement_desc_ripas, top)) == 0x58U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct measurement_desc_ripas, desc_type)) == 0x0U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct measurement_desc_ripas, len)) == 0x8U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct measurement_desc_ripas, rim)) == 0x10U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct measurement_desc_ripas, base)) == 0x50U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct measurement_desc_ripas, top)) == 0x58U);
#endif /* MEASUREMENT_DESCS_H */
diff --git a/lib/rmm_el3_ifc/include/rmm_el3_ifc.h b/lib/rmm_el3_ifc/include/rmm_el3_ifc.h
index f00edf8..ac5d907 100644
--- a/lib/rmm_el3_ifc/include/rmm_el3_ifc.h
+++ b/lib/rmm_el3_ifc/include/rmm_el3_ifc.h
@@ -206,10 +206,10 @@
struct console_list plat_console; /* Platform console list (from 0.3) */
};
-COMPILER_ASSERT(U(offsetof(struct rmm_core_manifest, version)) == 0U);
-COMPILER_ASSERT(U(offsetof(struct rmm_core_manifest, plat_data)) == 8U);
-COMPILER_ASSERT(U(offsetof(struct rmm_core_manifest, plat_dram)) == 16U);
-COMPILER_ASSERT(U(offsetof(struct rmm_core_manifest, plat_console)) == 40U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmm_core_manifest, version)) == 0U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmm_core_manifest, plat_data)) == 8U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmm_core_manifest, plat_dram)) == 16U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmm_core_manifest, plat_console)) == 40U);
/*
* Accessors to the Boot Manifest data
diff --git a/lib/smc/src/smc-rmi-offsets.c b/lib/smc/src/smc-rmi-offsets.c
index 9eb41d3..c273f48 100644
--- a/lib/smc/src/smc-rmi-offsets.c
+++ b/lib/smc/src/smc-rmi-offsets.c
@@ -6,53 +6,53 @@
#include <smc-rmi.h>
#include <stddef.h>
-COMPILER_ASSERT(sizeof(struct rmi_realm_params) == 0x1000UL);
-COMPILER_ASSERT(U(offsetof(struct rmi_realm_params, flags)) == 0U);
-COMPILER_ASSERT(U(offsetof(struct rmi_realm_params, s2sz)) == 0x8U);
-COMPILER_ASSERT(U(offsetof(struct rmi_realm_params, sve_vl)) == 0x10U);
-COMPILER_ASSERT(U(offsetof(struct rmi_realm_params, num_bps)) == 0x18U);
-COMPILER_ASSERT(U(offsetof(struct rmi_realm_params, num_wps)) == 0x20U);
-COMPILER_ASSERT(U(offsetof(struct rmi_realm_params, pmu_num_ctrs)) == 0x28U);
-COMPILER_ASSERT(U(offsetof(struct rmi_realm_params, algorithm)) == 0x30U);
-COMPILER_ASSERT(U(offsetof(struct rmi_realm_params, rpv)) == 0x400U);
-COMPILER_ASSERT(U(offsetof(struct rmi_realm_params, vmid)) == 0x800U);
-COMPILER_ASSERT(U(offsetof(struct rmi_realm_params, rtt_base)) == 0x808U);
-COMPILER_ASSERT(U(offsetof(struct rmi_realm_params, rtt_level_start)) == 0x810U);
-COMPILER_ASSERT(U(offsetof(struct rmi_realm_params, rtt_num_start)) == 0x818U);
+COMPILER_ASSERT_NO_CBMC(sizeof(struct rmi_realm_params) == 0x1000UL);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_realm_params, flags)) == 0U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_realm_params, s2sz)) == 0x8U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_realm_params, sve_vl)) == 0x10U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_realm_params, num_bps)) == 0x18U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_realm_params, num_wps)) == 0x20U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_realm_params, pmu_num_ctrs)) == 0x28U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_realm_params, algorithm)) == 0x30U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_realm_params, rpv)) == 0x400U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_realm_params, vmid)) == 0x800U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_realm_params, rtt_base)) == 0x808U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_realm_params, rtt_level_start)) == 0x810U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_realm_params, rtt_num_start)) == 0x818U);
-COMPILER_ASSERT(sizeof(struct rmi_rec_params) == 0x1000UL);
-COMPILER_ASSERT(U(offsetof(struct rmi_rec_params, flags)) == 0U);
-COMPILER_ASSERT(U(offsetof(struct rmi_rec_params, mpidr)) == 0x100U);
-COMPILER_ASSERT(U(offsetof(struct rmi_rec_params, pc)) == 0x200U);
-COMPILER_ASSERT(U(offsetof(struct rmi_rec_params, gprs)) == 0x300U);
-COMPILER_ASSERT(U(offsetof(struct rmi_rec_params, num_aux)) == 0x800U);
-COMPILER_ASSERT(U(offsetof(struct rmi_rec_params, aux)) == 0x808U);
+COMPILER_ASSERT_NO_CBMC(sizeof(struct rmi_rec_params) == 0x1000UL);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_rec_params, flags)) == 0U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_rec_params, mpidr)) == 0x100U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_rec_params, pc)) == 0x200U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_rec_params, gprs)) == 0x300U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_rec_params, num_aux)) == 0x800U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_rec_params, aux)) == 0x808U);
-COMPILER_ASSERT(sizeof(struct rmi_rec_enter) == 0x800UL);
-COMPILER_ASSERT(U(offsetof(struct rmi_rec_enter, flags)) == 0U);
-COMPILER_ASSERT(U(offsetof(struct rmi_rec_enter, gprs)) == 0x200U);
-COMPILER_ASSERT(U(offsetof(struct rmi_rec_enter, gicv3_hcr)) == 0x300U);
-COMPILER_ASSERT(U(offsetof(struct rmi_rec_enter, gicv3_lrs)) == 0x308U);
+COMPILER_ASSERT_NO_CBMC(sizeof(struct rmi_rec_enter) == 0x800UL);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_rec_enter, flags)) == 0U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_rec_enter, gprs)) == 0x200U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_rec_enter, gicv3_hcr)) == 0x300U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_rec_enter, gicv3_lrs)) == 0x308U);
-COMPILER_ASSERT(U(offsetof(struct rmi_rec_exit, exit_reason)) == 0U);
-COMPILER_ASSERT(U(offsetof(struct rmi_rec_exit, esr)) == 0x100U);
-COMPILER_ASSERT(U(offsetof(struct rmi_rec_exit, far)) == 0x108U);
-COMPILER_ASSERT(U(offsetof(struct rmi_rec_exit, hpfar)) == 0x110U);
-COMPILER_ASSERT(U(offsetof(struct rmi_rec_exit, gprs)) == 0x200U);
-COMPILER_ASSERT(U(offsetof(struct rmi_rec_exit, gicv3_hcr)) == 0x300U);
-COMPILER_ASSERT(U(offsetof(struct rmi_rec_exit, gicv3_lrs)) == 0x308U);
-COMPILER_ASSERT(U(offsetof(struct rmi_rec_exit, gicv3_misr)) == 0x388U);
-COMPILER_ASSERT(U(offsetof(struct rmi_rec_exit, gicv3_vmcr)) == 0x390U);
-COMPILER_ASSERT(U(offsetof(struct rmi_rec_exit, cntp_ctl)) == 0x400U);
-COMPILER_ASSERT(U(offsetof(struct rmi_rec_exit, cntp_cval)) == 0x408U);
-COMPILER_ASSERT(U(offsetof(struct rmi_rec_exit, cntv_ctl)) == 0x410U);
-COMPILER_ASSERT(U(offsetof(struct rmi_rec_exit, cntv_cval)) == 0x418U);
-COMPILER_ASSERT(U(offsetof(struct rmi_rec_exit, ripas_base)) == 0x500U);
-COMPILER_ASSERT(U(offsetof(struct rmi_rec_exit, ripas_top)) == 0x508U);
-COMPILER_ASSERT(U(offsetof(struct rmi_rec_exit, ripas_value)) == 0x510U);
-COMPILER_ASSERT(U(offsetof(struct rmi_rec_exit, imm)) == 0x600U);
-COMPILER_ASSERT(U(offsetof(struct rmi_rec_exit, pmu_ovf_status)) == 0x700U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_rec_exit, exit_reason)) == 0U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_rec_exit, esr)) == 0x100U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_rec_exit, far)) == 0x108U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_rec_exit, hpfar)) == 0x110U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_rec_exit, gprs)) == 0x200U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_rec_exit, gicv3_hcr)) == 0x300U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_rec_exit, gicv3_lrs)) == 0x308U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_rec_exit, gicv3_misr)) == 0x388U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_rec_exit, gicv3_vmcr)) == 0x390U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_rec_exit, cntp_ctl)) == 0x400U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_rec_exit, cntp_cval)) == 0x408U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_rec_exit, cntv_ctl)) == 0x410U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_rec_exit, cntv_cval)) == 0x418U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_rec_exit, ripas_base)) == 0x500U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_rec_exit, ripas_top)) == 0x508U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_rec_exit, ripas_value)) == 0x510U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_rec_exit, imm)) == 0x600U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_rec_exit, pmu_ovf_status)) == 0x700U);
COMPILER_ASSERT(sizeof(struct rmi_rec_run) <= GRANULE_SIZE);
-COMPILER_ASSERT(U(offsetof(struct rmi_rec_run, enter)) == 0U);
-COMPILER_ASSERT(U(offsetof(struct rmi_rec_run, exit)) == 0x800U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_rec_run, enter)) == 0U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rmi_rec_run, exit)) == 0x800U);
diff --git a/lib/smc/src/smc-rsi-offsets.c b/lib/smc/src/smc-rsi-offsets.c
index 4ba3afe..e0ff5d5 100644
--- a/lib/smc/src/smc-rsi-offsets.c
+++ b/lib/smc/src/smc-rsi-offsets.c
@@ -7,13 +7,13 @@
#include <stddef.h>
#include <utils_def.h>
-COMPILER_ASSERT(sizeof(struct rsi_realm_config) == 0x1000UL);
-COMPILER_ASSERT(U(offsetof(struct rsi_realm_config, ipa_width)) == 0U);
-COMPILER_ASSERT(U(offsetof(struct rsi_realm_config, algorithm)) == 8U);
+COMPILER_ASSERT_NO_CBMC(sizeof(struct rsi_realm_config) == 0x1000UL);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rsi_realm_config, ipa_width)) == 0U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rsi_realm_config, algorithm)) == 8U);
-COMPILER_ASSERT(sizeof(struct rsi_host_call) == 0x100UL);
-COMPILER_ASSERT(U(offsetof(struct rsi_host_call, imm)) == 0U);
-COMPILER_ASSERT(U(offsetof(struct rsi_host_call, gprs[0U])) == 8U);
-COMPILER_ASSERT(U(offsetof(struct rsi_host_call,
+COMPILER_ASSERT_NO_CBMC(sizeof(struct rsi_host_call) == 0x100UL);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rsi_host_call, imm)) == 0U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rsi_host_call, gprs[0U])) == 8U);
+COMPILER_ASSERT_NO_CBMC(U(offsetof(struct rsi_host_call,
gprs[RSI_HOST_CALL_NR_GPRS - 1U])) ==
U(8U * RSI_HOST_CALL_NR_GPRS));
diff --git a/plat/host/host_cbmc/src/tb_realm.c b/plat/host/host_cbmc/src/tb_realm.c
index a4c7228..8ed5bcf 100644
--- a/plat/host/host_cbmc/src/tb_realm.c
+++ b/plat/host/host_cbmc/src/tb_realm.c
@@ -140,12 +140,6 @@
__CPROVER_assume(g.state == GRANULE_STATE_RD);
struct rd rd = init_rd();
- /*
- * This assert is necessary because the COMPILER_ASSERT in realm.h is
- * disabled for CBMC.
- */
- __CPROVER_assert(sizeof(struct rd) <= GRANULE_SIZE, "check rd size");
-
struct granule *rd_granule = inject_granule(&g, &rd, sizeof(rd));
return rd_granule;
diff --git a/plat/host/host_cbmc/src/tb_rec.c b/plat/host/host_cbmc/src/tb_rec.c
index 723245e..53283da 100644
--- a/plat/host/host_cbmc/src/tb_rec.c
+++ b/plat/host/host_cbmc/src/tb_rec.c
@@ -28,12 +28,6 @@
__CPROVER_assume(g.state == GRANULE_STATE_REC);
struct rec rec = nondet_rec();
- /*
- * This assert is necessary because the COMPILER_ASSERT in realm.h is
- * disabled for CBMC.
- */
- __CPROVER_assert(sizeof(struct rec) <= GRANULE_SIZE, "check rec size");
-
rec.realm_info.g_rd = g_rd;
/* It must be a valid g_rd */
diff --git a/runtime/include/rec.h b/runtime/include/rec.h
index a5aae5d..7aa9fdd 100644
--- a/runtime/include/rec.h
+++ b/runtime/include/rec.h
@@ -25,6 +25,7 @@
#define RMM_REC_SAVED_GEN_REG_COUNT U(31)
#define STRUCT_TYPE struct
#define REG_TYPE unsigned long
+#define RMM_REALM_TOKEN_BUF_SIZE SZ_1K
#else /* CBMC */
/*
* struct rec must fit in a single granule. CBMC has a smaller GRANULE_SIZE
@@ -44,6 +45,7 @@
#define STRUCT_TYPE union
/* Reserve a single byte per saved register instead of 8. */
#define REG_TYPE unsigned char
+#define RMM_REALM_TOKEN_BUF_SIZE 4U
#endif /* CBMC */
struct granule;
@@ -131,7 +133,7 @@
* Data used when handling attestation requests
*/
struct rec_attest_data {
- unsigned char rmm_realm_token_buf[SZ_1K];
+ unsigned char rmm_realm_token_buf[RMM_REALM_TOKEN_BUF_SIZE];
size_t rmm_realm_token_len;
struct token_sign_cntxt token_sign_ctx;
@@ -256,7 +258,7 @@
* registers.
*/
COMPILER_ASSERT(U(offsetof(struct rec, sp_el0)) ==
- (U(offsetof(struct rec, regs)) + U(sizeof(unsigned long) * RMM_REC_SAVED_GEN_REG_COUNT)));
+ (U(offsetof(struct rec, regs)) + U(sizeof(REG_TYPE) * RMM_REC_SAVED_GEN_REG_COUNT)));
/*
* Check that mpidr has a valid value with all fields except
diff --git a/tools/cbmc/CheckCBMC.cmake b/tools/cbmc/CheckCBMC.cmake
index bfb6447..64df056 100644
--- a/tools/cbmc/CheckCBMC.cmake
+++ b/tools/cbmc/CheckCBMC.cmake
@@ -90,8 +90,6 @@
set(cbmc_defines_list
"-DCBMC"
- "-DDISABLE_COMPILER_ASSERT"
- "-DDISABLE_SET_MEMBER"
"-DGRANULE_SHIFT=${GRANULE_SHIFT}"
"-DXLAT_GRANULARITY_SIZE_SHIFT=${GRANULE_SHIFT}"
"-DRMM_MAX_GRANULES=${MAX_NUM_OF_GRANULE}"