JK

Disallow identifiers starting with dots

1

I noticed that it is possible to create a crate with a name starting with `.`: ```shell $ alr init --bin .dot Alire needs some user information to initialize the...

### Context and Problem Statement Optimizations of the generated code are currently done only in the generator. The problem here is that depending on the target and use case of...

RFLX.RFLX_Types.Operators package

3

The operators for the types defined in `RFLX.RFLX_Types` are currently also defined in this package. As the types in this package are only subtypes the operators are not primitive functions...

The state `Start` in the following spec assigns the return value of a function call to a message variable. This message can be invalid yet the model checker complains that...

Messages can contain statically false links if at least one similar link exists that can become true. The following code should produce an error: ```Python from rflx.model import Message, ModularInteger,...

Using Boolean value as condition causes exception in Z3

2

Using a boolean variable or field as a condition value as follows: ```Ada package Test is type Tag is (Tag_A, Tag_B) with Size => 8; type Message (Has_Tag : Boolean)...

If the specs are given in the wrong order and are in different directories RecordFlux emits an error that it could not find the spec. E.g. if `a.rflx` depends on...

NotImplementedError raised when using function call as argument of message aggregate

2

With my current SPDM spec I get the following bugbox: ``` ------------------------------ RecordFlux Bug ------------------------------ RecordFlux 0.6.0-pre RecordFlux-parser 0.10.0 ruamel.yaml 0.17.21 attrs 21.4.0 pydotplus 2.0.2 z3-solver 4.8.17.0 pydantic 1.9.0 icontract...

Setting a sequence field by referring to a sequence field of a message

3

When I try to edit a message in a session by assigning it to itself and editing the fields as follows ```Ada Response := SPDM::Response' (Meas_Cap => Response.Meas_Cap, Hash_Type =>...

non-definite message in return type of function not allowed

2

I'm getting the following error when trying to return a non-defined message in a function: ``` ------------------------------ RecordFlux Bug ------------------------------ RecordFlux 0.6.0-pre RecordFlux-parser 0.10.0 ruamel.yaml 0.17.21 pydantic 1.9.0 icontract 2.6.1...