summaryrefslogtreecommitdiffstats
path: root/src/md.h
diff options
context:
space:
mode:
authorChristophe Grenier <[email protected]>2022-04-06 07:42:41 +0200
committerChristophe Grenier <[email protected]>2022-04-06 07:42:41 +0200
commite6c21a9bb47bc55e137382ee310debb68ff18148 (patch)
tree331f35e3e2e167e78bf5d469dda1adbdc40e0907 /src/md.h
parent37d1b8ce36b2af3d99a7792dc6928929e437d617 (diff)
Avoid field with a 0 size as Frama-C do not support them.
Diffstat (limited to 'src/md.h')
-rw-r--r--src/md.h2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/md.h b/src/md.h
index eb579f48..76da2da1 100644
--- a/src/md.h
+++ b/src/md.h
@@ -242,7 +242,9 @@ struct mdp_superblock_1 {
* into the 'roles' value. If a device is spare or faulty, then it doesn't
* have a meaningful role.
*/
+#if !defined(__FRAMAC__)
uint16_t dev_roles[0]; /* role in array, or 0xffff for a spare, or 0xfffe for faulty */
+#endif
};
#if 0