Address comments of PR #337

- Add more known third party packages to .isort.cfg - Move field length test to test_verification - Improve field length test to not only contain invalid values Ref. #336, #337
AdaCore · Jul 23, 2020 · 81b5145 · 81b5145
1 parent cd91cff
commit 81b5145
Show file tree

Hide file tree

Showing 3 changed files with 21 additions and 21 deletions.
diff --git a/.isort.cfg b/.isort.cfg
@@ -4,4 +4,4 @@ include_trailing_comma=True
 force_grid_wrap=0
 use_parentheses=True
 line_length=100
-known_third_party=pytest,z3,pydotplus
+known_third_party=icontract,pydotplus,pyparsing,pytest,z3
diff --git a/tests/test_model.py b/tests/test_model.py
@@ -1520,20 +1520,3 @@ def test_opaque_length_valid_multiple_of_8_dynamic_cond() -> None:
         ],
         {Field("L"): MODULAR_INTEGER, Field("O"): Opaque()},
     )
-
-
-def test_length_range_underflow() -> None:
-    with pytest.raises(
-        RecordFluxError,
-        match=r'^<stdin>:44:3: model: error: negative length for field "O" [(]L -> O[)]$',
-    ):
-        o = Field(ID("O", location=Location((44, 3))))
-        Message(
-            "P.M",
-            [
-                Link(INITIAL, Field("L")),
-                Link(Field("L"), o, length=Mul(Number(8), Sub(Variable("L"), Number(50))),),
-                Link(o, FINAL),
-            ],
-            {Field("L"): RangeInteger("P.Len", Number(40), Number(1500), Number(16)), o: Opaque()},
-        )
diff --git a/tests/test_verification.py b/tests/test_verification.py
@@ -491,21 +491,38 @@ def test_invalid_length_forward_reference() -> None:
     assert_message_model_error(structure, types, '^model: error: subsequent field "F2" referenced$')
 
 
-def test_invalid_negative_field_length() -> None:
+def test_invalid_negative_field_length_modular() -> None:
     structure = [
         Link(INITIAL, Field("F1")),
-        Link(Field("F1"), Field("F2"), length=Sub(Variable("F1"), Number(300))),
+        Link(Field("F1"), Field("F2"), length=Sub(Variable("F1"), Number(2))),
         Link(Field("F2"), FINAL),
     ]
     types = {
         Field("F1"): MODULAR_INTEGER,
         Field("F2"): Opaque(),
     }
     assert_message_model_error(
-        structure, types, r"^" r'model: error: negative length for field "F2" [(]F1 -> F2[)]' r"$",
+        structure, types, r'^model: error: negative length for field "F2" [(]F1 -> F2[)]$',
     )
 
 
+def test_invalid_negative_field_length_range_integer() -> None:
+    with pytest.raises(
+        RecordFluxError,
+        match=r'^<stdin>:44:3: model: error: negative length for field "O" [(]L -> O[)]$',
+    ):
+        o = Field(ID("O", location=Location((44, 3))))
+        Message(
+            "P.M",
+            [
+                Link(INITIAL, Field("L")),
+                Link(Field("L"), o, length=Mul(Number(8), Sub(Variable("L"), Number(50))),),
+                Link(o, FINAL),
+            ],
+            {Field("L"): RANGE_INTEGER, o: Opaque()},
+        )
+
+
 def test_payload_no_length() -> None:
     structure = [
         Link(INITIAL, Field("F1")),