Use Opaque.element_size for alignement/length checks

Ref. #288, #327
AdaCore · Jul 23, 2020 · bd7811c · bd7811c
1 parent 135637f
commit bd7811c
Showing 1 changed file with 16 additions and 8 deletions.
diff --git a/rflx/model.py b/rflx/model.py
@@ -1247,32 +1247,40 @@ def __prove_field_positions(self) -> None:
                     )
                     return
 
-                if f in self.__types and isinstance(self.__types[f], Opaque):
+                if f in self.__types:
+                    t = self.__types[f]
+                    if not isinstance(t, Opaque):
+                        continue
+                    element_size = t.element_size
                     start_aligned = Not(
-                        Equal(Mod(self.__target_first(last), Number(8)), Number(1), last.location)
+                        Equal(
+                            Mod(self.__target_first(last), element_size), Number(1), last.location
+                        )
                     )
                     proof = start_aligned.check([*facts, *self.__type_constraints(start_aligned)])
                     if proof.result != ProofResult.unsat:
                         path_message = " -> ".join([p.target.name for p in path])
                         self.error.append(
-                            f'opaque field "{f.name}" not aligned to 8 bit boundary'
+                            f'opaque field "{f.name}" not aligned to {element_size} bit boundary'
                             f" ({path_message})",
                             Subsystem.MODEL,
                             Severity.ERROR,
                             f.identifier.location,
                         )
                         return
 
-                    length_multiple_8 = Not(
-                        Equal(Mod(self.__target_length(last), Number(8)), Number(0), last.location)
+                    length_multiple_element_size = Not(
+                        Equal(
+                            Mod(self.__target_length(last), element_size), Number(0), last.location
+                        )
                     )
-                    proof = length_multiple_8.check(
-                        [*facts, *self.__type_constraints(length_multiple_8)]
+                    proof = length_multiple_element_size.check(
+                        [*facts, *self.__type_constraints(length_multiple_element_size)]
                     )
                     if proof.result != ProofResult.unsat:
                         path_message = " -> ".join([p.target.name for p in path])
                         self.error.append(
-                            f'length of opaque field "{f.name}" not multiple of 8 bit'
+                            f'length of opaque field "{f.name}" not multiple of {element_size} bit'
                             f" ({path_message})",
                             Subsystem.MODEL,
                             Severity.ERROR,