RecordFlux
RecordFlux copied to clipboard
AdaCore
Formal specification and generation of verifiable binary parsers, message generators and protocol state machines
- support most of our usual checkers - use pytests `-n auto` switch instead of `nproc` - remove launch configuration (didn't seem to be very helpful)
### 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...
The GNAT Studio plugin should be installable without access to the source code. The installation could be realized using a specific sub-command of `rflx` (e.g., `rflx install_gnatstudio`). The plugin needs...
This is caused by missing entries in the generated `locations.json`. ### Example ```console % rflx graph -d generated specs/ipv4.rflx Parsing specs/ipv4.rflx Processing IPv4 Creating generated/IPv4_Option.svg Creating generated/IPv4_Packet.svg ``` ```console %...
Currently `_prove_reachability` does not include constraints (type constraints and potentially others) which prevents it from finding unreachable paths. When the reachability proof is fixed, `_prove_contradictions` can be removed.
### Context and Problem Statement In protocols the values of two scalar types sometimes have to be mapped onto / converted into each other in a way that cannot be...
https://github.com/marketplace/actions/gs-commit-message-checker
The generator currently doesn't support private types (cf. #758). We need to decide whether we want / need private types at all an either implement them in the generator or...