diff --git a/.isort.cfg b/.isort.cfg index 8d099c006..8811c9c00 100644 --- 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 index 2f67a1bda..f1fef86d4 100644 --- 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'^: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 index bff892d7c..f967b07ee 100644 --- a/tests/test_verification.py +++ b/tests/test_verification.py @@ -491,10 +491,10 @@ 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 = { @@ -502,10 +502,27 @@ def test_invalid_negative_field_length() -> None: 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'^: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")),