CHANGELOG.md

Changelog

All notable changes to this project will be documented in this file.

The format is based on Keep a Changelog, and this project adheres to Semantic Versioning.

Unreleased

Changed

• Display message fields involved in a cycle (eng/recordflux/RecordFlux#256)

Fixed

• Bug box for aspect without expression (eng/recordflux/RecordFlux#1555, eng/recordflux/RecordFlux#1559)
• Bug box for division and modulo by 0 in numeric expression (eng/recordflux/RecordFlux#1556)
• Bug box for unary - preceding unary + in expression (eng/recordflux/RecordFlux#1558)
• Bug box for missing operand (eng/recordflux/RecordFlux#1560)
• Bug box for negated expressions (eng/recordflux/RecordFlux#1561, eng/recordflux/RecordFlux#1569)
• Bug box for duplicated operator (eng/recordflux/RecordFlux#1562)
• Bug box for link to missing field (eng/recordflux/RecordFlux#1566)

0.21.0 - 2024-04-23

Changed

• Improve error messages for type refinements of non-message types (#383, eng/recordflux/RecordFlux#383)

Fixed

• Generation of uncompilable code in the presence of some Boolean conditions (eng/recordflux/RecordFlux#1365)
• Exception when checking specification in GNAT Studio (eng/recordflux/RecordFlux#1492)

0.20.0 - 2024-03-26

Added

• Possibility to use multiple initial links in messages to allow the first message field to be defined by parameter values (#764, eng/recordflux/RecordFlux#764)

Changed

• Improve performance of code optimizer (requires SPARK 25; eng/recordflux/RecordFlux#1533)
• Improve error message when package name matches source file name but the casing isn't correct (eng/recordflux/RecordFlux#1554)

Fixed

• Parsing of messages that depend on fraction comparisons in PyRFLX (#981, eng/recordflux/RecordFlux#981)
• Installation of VS Code extension (eng/recordflux/RecordFlux#1544)

0.19.0 - 2024-02-29

Added

• Prevent different casings for same entity (#563, eng/recordflux/RecordFlux#563)
• Code optimizer that removes unnecessary checks in generated state machine code (eng/recordflux/RecordFlux#1525)

Fixed

• Unexpected errors when using different casings for same entity (#562, eng/recordflux/RecordFlux#1506)

0.18.0 - 2024-01-30

Added

• Pragma marking all generated files as Ada 2012 (#1293, eng/recordflux/RecordFlux#1509)
• --no-caching option to rflx (eng/recordflux/RecordFlux#1488)
• Model verification caching to validator

Changed

• Insert/Extract functions accept Byte array instead of access type (eng/recordflux/RecordFlux#1515)

Fixed

• Various inaccuracies in Language Reference (#958, eng/recordflux/RecordFlux#958)
• Erroneous acceptance of consecutive / trailing underscores (eng/recordflux/RecordFlux#1468)
• Fatal error when digit in numeric literal exceeds base (eng/recordflux/RecordFlux#1469)
• Fatal error when unsupported base is used in numeric literal (eng/recordflux/RecordFlux#1470)
• Missing diagnostics provided by language server
• --split-disjunctions options of rflx validate
• Misleading CLI output about verification (#1295, eng/recordflux/RecordFlux#1522)

0.17.0 - 2024-01-03

Fixed

• Fatal error when comparing opaque fields (#1294, eng/recordflux/RecordFlux#1497)
• Fatal error when GraphViz is missing (eng/recordflux/RecordFlux#1499)
• Missing rejection of sequences of parameterized messages (eng/recordflux/RecordFlux#1439)

Removed

• Verification of message bit coverage (eng/recordflux/RecordFlux#1495)

0.16.0 - 2023-12-05

Added

• Support for FSF GNAT 13.2 (eng/recordflux/RecordFlux#1458)
• --reproducible option to rflx generate and rflx convert (eng/recordflux/RecordFlux#1489)

Changed

• Improve parallelization of message verification (#444, eng/recordflux/RecordFlux#444)
• Improve message verification (#420, #1090, eng/recordflux/RecordFlux#420, eng/recordflux/RecordFlux#1090, eng/recordflux/RecordFlux#1476)

Fixed

• Proving of validity of message field after update with valid sequence (eng/recordflux/RecordFlux#1444)
• Style check warnings for license header (#1293, eng/recordflux/RecordFlux#1461)

0.15.0 - 2023-11-08

Added

• Support for SPARK Pro 24.0 (eng/recordflux/RecordFlux#1409)
• Support for GNAT Pro 24.0 (eng/recordflux/RecordFlux#1443)

Changed

• Syntax for passing repeated -i and -v options to rflx validate (eng/recordflux/RecordFlux#1441)
• Simplify setter code and remove internal Successor function (eng/recordflux/RecordFlux#1448)
• Improve names of enum literals generated from IANA registries (eng/recordflux/RecordFlux#1451)

Fixed

• Fatal errors caused by condition on message type field (#1291, eng/recordflux/RecordFlux#1438)

Removed

• Support for SPARK Pro Wavefront 20230905 (eng/recordflux/RecordFlux#1409)
• Short form field conditions (eng/recordflux/RecordFlux#617)

0.14.0 - 2023-09-26

Added

• Functions Valid_Next_Internal, Field_Size_Internal, Field_First_Internal (eng/recordflux/RecordFlux#1382)
• rflx validate -v and -i options accept multiple directories (eng/recordflux/RecordFlux#1393)
• rflx validate -v and -i options accept also files (eng/recordflux/RecordFlux#1418)
• Caching of successful verification of derived messages and refinements (eng/recordflux/RecordFlux#1421)

Changed

• Removed Predecessor field from Field_Cursor record (eng/recordflux/RecordFlux#1387)
• Improve stability and performance of language server (eng/recordflux/RecordFlux#1417)
• Improve performance of model verification

Fixed

• Code generation for accesses to optional fields whose presence is ensured by a condition (eng/recordflux/RecordFlux#1420)
• Error when passing checksum module to validator on the command line

Removed

• Functions Valid_Predecessor and Path_Condition (eng/recordflux/RecordFlux#1382)

0.13.0 - 2023-09-13

Added

• Support for SPARK Pro Wavefront 20230905 (eng/recordflux/RecordFlux#1403, eng/recordflux/RecordFlux#1409)

Changed

• Reject duplicate optional arguments in rflx CLI (eng/recordflux/RecordFlux#1342)
• Split the Valid_Context into multiple functions (eng/recordflux/RecordFlux#1385)
• IANA registries with unsupported content are skipped with a warning (eng/recordflux/RecordFlux#1406)

Removed

• Support for GNAT Pro 20.2 and GNAT Community 2020 (eng/recordflux/RecordFlux#1403)
• Support for SPARK Pro 23.1 (eng/recordflux/RecordFlux#1403)

0.12.0 - 2023-08-22

Added

• Language server (eng/recordflux/RecordFlux#1355)
• VS Code extension (eng/recordflux/RecordFlux#1355)
• Support for GNAT Pro 23.2
• Logging of required runtime checks during code generation (#1204, eng/recordflux/RecordFlux#1204)

Changed

• Prevent unnecessary runtime checks in generated code (#1204, eng/recordflux/RecordFlux#1204)
• Removal of discriminant in Field_Cursor type (eng/recordflux/RecordFlux#1377)

Fixed

• Missing quotes in error messages about invalid aspects (#1267, eng/recordflux/RecordFlux#1267)
• Subsequent errors caused by style errors (#1268, eng/recordflux/RecordFlux#1268)
• Missing type checking in refinement conditions (eng/recordflux/RecordFlux#1360)
• Exception caused by comparing integer field to aggregate (#1251, eng/recordflux/RecordFlux#1251)
• Unexpected errors when using --max_errors=1 (#825, eng/recordflux/RecordFlux#825)
• Incorrect detection of conditions as always true for enumerations with Always_Valid aspect (#1276, eng/recordflux/RecordFlux#1276)
• Potential name conflicts with internally used identifiers that start with RFLX_ (#638, eng/recordflux/RecordFlux#638)
• Deadlocks during verification caused by forked processes (eng/recordflux/RecordFlux#1366)

0.11.1 - 2023-07-14

Fixed

• Caching of successful verification (eng/recordflux/RecordFlux#1345)
• Locations of message fields and field sizes in error messages (eng/recordflux/RecordFlux#1349)
• Invalid use of First aspect that led to overlay of multiple fields (eng/recordflux/RecordFlux#1332)
• Update of message field with invalid sequence (eng/recordflux/RecordFlux#1353)
• Detection of negative field size (eng/recordflux/RecordFlux#1357)

0.11.0 - 2023-06-16

Removed

• Support for installing RecordFlux package with GNAT Pro 20, GNAT Pro 21 and GNAT Community 2020 (eng/recordflux/RecordFlux#1335)

0.10.0 - 2023-05-24

Changed

• Allow update of generated files (#1275, eng/recordflux/RecordFlux#1275)
• Integrate parser into RecordFlux package (eng/recordflux/RecordFlux#1316)
• Simplify shape of the Valid_Context predicate (eng/recordflux/SparkFlux#11)
• Remove unneeded postcondition of setters (eng/recordflux/RecordFlux#1330)

Fixed

• Installation of GNAT Studio plugin (eng/recordflux/RecordFlux#1293)
• Order of types and sessions after parsing (#1076, eng/recordflux/RecordFlux#1076)
• Strict dependency on specific versions of shared libraries (eng/recordflux/RecordFlux#1316)
• Displaying of graphs in GNAT Studio (#1169, eng/recordflux/RecordFlux#1169)

0.9.1 - 2023-03-28

Fixed

• Missing with clause in session package for indirectly used enumeration types (eng/recordflux/RecordFlux#1298)
• Compilation error for message field access in state transition (eng/recordflux/RecordFlux#1299)
• Warning about that with RFLX.RFLX_Types is unreferenced or might be moved to body of session package

0.9.0 - 2023-01-06

Added

• Support for Python 3.11

Removed

• Bindings (#724)

0.8.0 - 2022-12-02

Changed

• Rename Structural_Valid to Well_Formed (#986)
• Reject statically true conditions in messages (#662)
• Reject statically false and true refinement conditions (#662)

Removed

• Modular integer types (#727)

Fixed

• Exception transition rejected on message assignment (#1144)
• Document where type derivations and sequence types are valid (#1235)

0.7.1 - 2022-11-04

Fixed

• Exception when using a boolean value as condition (#776)

0.7.0 - 2022-10-04

Added

• CLI:
  • rflx setup_ide subcommand for installing IDE integration (#795)
  • rflx option --unsafe (#987)
  • rflx convert subcommand for converting foreign specifications
  • rflx convert iana subcommand for converting IANA "Service Name and Transport Protocol Port Number Registry" XML files (#708)
• Model:
  • Detection of unused parameters (#874)
  • Detection of invalid use of literals in expressions (#686, #1194)

Changed

• Specification:
  • Syntax for defining initial and final states of session (#700)
• Model:
  • Change representation of null messages (#643)
• Generator:
  • Style of Ada comments (#816)
  • Detect when a generated file would overwrite an existing file (#993)
  • Move operators and operations on types into separate child packages (#1126)

Removed

• Specification:
  • Private types (#1156)

Fixed

• Non-null state accepted as final state (#1130)
• Spurious error if providing specifications in certain order (#759)
• Handling of specification dependencies when using multiple directories

0.6.0 - 2022-08-31

Added

• Parameterized messages (#609, #743)
• Endianness (#104, #914)
• Validator (#560)
• Parallelization of Z3 proofs and code generation (#625, #976)
• Simple specification style checker (#799)
• Integration files for defining buffer sizes of messages and sequences in sessions (#713)
• Memory management in sessions to avoid use of heap (#629)
• Setting of single message fields (#1067)
• Case expressions (#907)
• Optimization and support for Head attributes on list comprehensions (#1115)
• Specification:
  • Enable deactivation of style checks for individual files (#1079)
• CLI:
  • rflx option --max-errors NUM (#748)
  • rflx option --workers NUM for setting the maximum number of parallel processes which are used for model verification (#755)
  • rflx generate option --integration-files-dir (#713)
  • rflx generate option --debug {built-in,external} (#1052)
• Generator:
  • Function for getting current state of session (#796)
  • Support for No_Secondary_Stack restriction (#911)
  • Possibility for externally defined debug output function in generated code (#1052)
  • Compatibility of generated code to FSF GNAT 11, 12 and GNAT Pro 23 (#674, #905, #1015, #1116)
  • Backward compatibility of generated code to GNAT Community 2020 and GNAT Pro 20 (#896)
• Python dependency ruamel.yaml
• Support for Python 3.10

Changed

• CLI:
  • Make rflx option --no-verification global (#750)
• Specification / Model:
  • Model.__init__ now considers all type dependencies (#1074)
  • Rename then to goto in session states (#738)
  • Allow omitting the size aspect for opaque and sequence fields which are the last field of the message (#736)
  • Allow use of Message'Last and Message'Size only in conditions of the last fields of the message (#736)
  • Enable use of Opaque attribute for arguments of function calls and on sequences (#984, #1021)
  • Keep multiple message versions in verification cache (#1028)
  • Improve generation of specification files for model (#1009, #1022)
  • Detect duplicate aspects (#714)
• Generator:
  • Improve binary size of generated code (#908)
  • Use tagged types instead of generic packages for sessions (#768)
  • Change channel interface in generated code (#766, #807)
  • Improve handling of bounds in message contexts (#844)
  • Optimize provability of generated code (#806, #840, #938, #975)
  • Relax length precondition of To_Context (#1054)
  • Enable comprehensions with message sequence as target (#891)
  • Add precondition Uninitialized to procedure Initialize (#788)
  • Add operators for Length and Index types (#1070)
  • Overwrite symlinks when creating files
  • Make In_IO_State session function public (#1155)
  • Generate improved code for messages with reduced feature usage (#1114)
• PyRFLX:
  • Remove __getitem__ (#783)
• Graph:
  • Improve layout of session graphs (#400)

Removed

• Support for Python 3.7

Fixed

• Installation of parser when installing RecordFlux from PyPI (#745)
• Examples in README (#879)
• Model:
  • Handling of Message attributes in message types (#729)
  • Missing file location in error messages (#647)
  • Bug box due to dangling field when merging messages (#1033)
  • Missing type information in Reset statement (#1080)
  • Incorrect message size calculation if size depends on variables (#1064)
• Generator:
  • Error when using Boolean as return type of function (#752)
  • Error when using unqualified type as return type of function (#892)
  • Bugbox when using Reset attribute on a sequence while running without optimization (#946)
  • Generation of use clauses for sessions (#757)
  • Missing type conversions in generated code (#761, #902, #965)
  • Code generation for:
    • Boolean as function parameter (#882)
    • Message aggregates (#770)
    • Use of messages with single opaque field in sessions (#888)
    • Function calls in sessions (#763)
    • Mathematical expressions with intermediate values outside type range (#726)
    • Logical expressions in assignments (#1012)
    • Boolean relations containing global variables (#1059)
    • Minimal session (#883)
    • Message aggregates with variables as field values (#1064)
    • Message fields with a sequence type name equal to the package name
  • Code generation when using non-default prefix (#897)
  • Conversion between message Structure and Context (#961)
  • Missing reset in assignment to comprehension (#1050)
  • Message size calculation for message aggregates (#1042)
  • Initialization of session context (#954)
  • Unprovable VC with some user conditions on fields (#995)
• PyRFLX:
  • Error caused by relations between sequences, opaque fields or aggregates (#964)
  • Undefined attribute in MessageValue.Field (#1045)
  • Missing type check for arguments of parameterized message (#1104)

0.5.0 - 2021-08-11

Added

• Preview Features:
  • Message checksums (#222, #240)
  • Protocol sessions (#47, #291, #292, #675)
• General:
  • Achieve "Passing" level of CII Best Practices Badge Program (#660)
  • Enforce 100% test coverage (#334)
  • Show bug box on fatal errors (#607, #655)
  • Add ping example app (#366)
  • Improve language reference (#703)
  • Support showing message graphs in GNAT Studio (#345)
• Specification / Model:
  • Improve specification parser (#547, #572)
  • Change syntax of message types (#380, #432, #421), sequence types (#528) and package separators (#441)
  • Enable specification of field conditions (#95, #617)
  • Add modulo operation (#476)
  • Enable use of size of static types in expressions (#384, #480)
  • Add static type checking of expressions (#87)
  • Fix message verification (#388, #389, #410, #413, #492, #497, #520, #522, #530, #579)
  • Add caching of verification result of message specifications (#442)
• SPARK Code Generation:
  • Switch from GNAT Community 2020 to GNAT Community 2021 (#494)
  • Fix code generation (#375, #479, #486, #356, #500, #536, #530, #593, #665)
  • Change API of generated code (#487, #514, #548, #557, #659)
• PyRFLX:
  • Enable type checking in external applications (#393)
  • Change API (#406, #423, #467, #529, #510)
  • Fix message parsing and serialization (#407, #503, #531, #533, #525, #606, #559, #624)
  • Improve performance (#344)
• New Dependencies:
  • Python >=3.7
  • attrs
  • GNAT Community 2021 (GNAT compiler and SPARK verification tools)

0.4.1 - 2020-07-23

Added

• Specification / Model:
  • Improve error messages (#248)
  • Add GNAT Studio integration (#243)
  • Add more checks for invalid models (#282, #288, #298, #309, #310, #311, #313, #336, #338)
  • Fix erroneously rejected specifications (#277, #347, #351)
  • Improve parsing performance (#305)
• SPARK Code Generation:
  • Allow use of scalars up to 64 bit (#238)
  • Prevent potentially failing code compilation (#312, #314, #315, #316, #319, #320, #329, #349)
  • Allow setting empty sequence field (#353)
  • Fix comparison of field values with aggregate (#328)
  • Improve verifiability of accesses to opaque fields (#287)
  • Fix handling of empty prefixes (#266)
• PyRFLX:
  • Improve performance (#254)
  • Fix determining of predecessor field (#289)
  • Fix handling of prefixed literals (#346)

0.4.0 - 2020-06-02

Added

• Introduce PyRFLX - a Python library for rapid-prototyping and validation
  • Based on RecordFlux message specifications
  • Allows parsing and generation of messages
  • Validates formal specification at runtime
• Introduce design-by-contract programming in Python code using icontract
• Specification / Model:
  • Allow import of types of other packages
  • Allow use of message types as field types
  • Add built-in Boolean type
  • Support aggregates and strings
  • Allow comparisons of arrays to aggregates in conditions
• SPARK Code Generation:
  • Allow use of custom buffer type
  • Support for GNAT Community 2020 (GNAT compiler and SPARK verification tools)
• Python dependency icontract (library for design by contract)

Changed

• Specification / Model:
  • Simplify derived types by removing inheritance of refinements
  • Improve detection of error cases
  • Improve error messages
  • Fix incorrect parsing of mathematical expressions
  • Rename Payload to Opaque in specifications

Removed

• Need for SPARK Pro for verification
• Support for GNAT Community 2019

0.3.0 - 2020-01-24

Added

• Generation of message generator
• Verification of message specifications
• Generation of graph from message specification
• Python dependency PyDotPlus (used for generation of graphs)
• Python dependency Z3 (used for verification of message specifications)

Changed

• Incorrect handling of absolute file paths
• Minimum required version of PyParsing increased to 2.4.0
• Minimum required version of SPARK verification tools changed to Pro 20.0 (known issues will be resolved in GNAT Community 2020)

0.2.0 - 2019-09-16

0.1.0 - 2019-05-14