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
-----------------------------------