Improve proving of byte alignment of opaque fields

Ref. eng/recordflux/RecordFlux#1563
AdaCore · Mar 21, 2024 · 74bffa6 · 74bffa6
1 parent c7959f5
commit 74bffa6
Showing 1 changed file with 9 additions and 5 deletions.
diff --git a/rflx/model/message.py b/rflx/model/message.py
@@ -1903,12 +1903,16 @@ def _prove_field_positions(
                     t = self.types[f]
                     if isinstance(t, mty.Opaque):
                         element_size = t.element_size
-                        start_aligned = expr.Not(
-                            expr.Equal(
-                                expr.Mod(self._target_first(last), element_size),
-                                expr.Number(1),
-                                last.location,
+                        start_aligned = expr.NotEqual(
+                            expr.Mod(
+                                expr.Add(
+                                    self._target_first(last),
+                                    expr.Number(-1),
+                                ).simplified(),
+                                element_size,
                             ),
+                            expr.Number(0),
+                            last.location,
                         )
 
                         path_message = " -> ".join([p.target.name for p in path])