search

AdaCore / RecordFlux

Formal specification and generation of verifiable binary parsers, message generators and protocol state machines
Apache License 2.0
104 stars 6 forks source link

AssertionError caused by comparison of integer field and aggregate #1251

Closed treiher closed 1 year ago

treiher commented 1 year ago 
package Test is

   type T is range 1 .. 10 with Size => 16;

   type M is
      message
         F1 : T
            then null
               if F1 = [1, 2];
   end message;

end Test;
Traceback (most recent call last):
  File "/home/devel/Componolit/RecordFlux/rflx/cli.py", line 259, in main
    args.func(args)
  File "/home/devel/Componolit/RecordFlux/rflx/cli.py", line 307, in check
    parse(args.files, args.no_verification, args.workers)
  File "/home/devel/Componolit/RecordFlux/rflx/cli.py", line 368, in parse
    model = parser.create_model()
  File "/home/devel/Componolit/RecordFlux/rflx/specification/parser.py", line 1854, in create_model
    self._evaluate_specification(error, spec_node.spec, spec_node.filename)
  File "/home/devel/Componolit/RecordFlux/rflx/specification/parser.py", line 1981, in _evaluate_specification
    new_type = handlers[t.f_definition.kind_name](
  File "/home/devel/Componolit/RecordFlux/rflx/specification/parser.py", line 1012, in create_message
    return create_proven_message(
  File "/home/devel/Componolit/RecordFlux/rflx/specification/parser.py", line 1603, in create_proven_message
    proven_message = unproven_message.proven(
  File "/home/devel/Componolit/RecordFlux/rflx/model/message.py", line 2191, in proven
    return Message(
  File "/home/devel/Componolit/RecordFlux/rflx/model/message.py", line 873, in __init__
    self.verify()
  File "/home/devel/Componolit/RecordFlux/rflx/model/message.py", line 893, in verify
    self._prove_contradictions()
  File "/home/devel/Componolit/RecordFlux/rflx/model/message.py", line 1747, in _prove_contradictions
    constraints = self.message_constraints() + self.type_constraints(contradiction)
  File "/home/devel/Componolit/RecordFlux/.venv/lib/python3.10/site-packages/icontract/_checkers.py", line 892, in wrapper
    result = func(*args, **kwargs)
  File "/home/devel/Componolit/RecordFlux/rflx/model/message.py", line 429, in type_constraints
    *self._aggregate_constraints(expression),
  File "/home/devel/Componolit/RecordFlux/rflx/model/message.py", line 456, in _aggregate_constraints
    aggregate_constraints.extend(get_constraints(r.right, r.left))
  File "/home/devel/Componolit/RecordFlux/rflx/model/message.py", line 437, in get_constraints
    assert isinstance(comp, mty.Composite)
AssertionError
treiher commented 1 year ago

Fixed in version 0.12.0.