RecordFlux Versions Save

Changed

• Improve error messages for type refinements of non-message types (AdaCore/RecordFlux#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)

Added

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

Changed

• Improve performance of code optimizer (requires SPARK 25; eng/recordflux/RecordFlux#1533)

Fixed

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

Added

• Prevent different casings for same entity (AdaCore/RecordFlux#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 (AdaCore/RecordFlux#562, eng/recordflux/RecordFlux#1506)

Added

• Pragma marking all generated files as Ada 2012 (AdaCore/RecordFlux#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 (AdaCore/RecordFlux#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 (AdaCore/RecordFlux#1295, eng/recordflux/RecordFlux#1522)

Fixed

• Fatal error when comparing opaque fields (AdaCore/RecordFlux#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)

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 (AdaCore/RecordFlux#444, eng/recordflux/RecordFlux#444)
• Improve message verification (AdaCore/RecordFlux#420, AdaCore/RecordFlux#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 (AdaCore/RecordFlux#1293, eng/recordflux/RecordFlux#1461)

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

• User defined GNATCOLL_ICONV_OPT environment variable is ignored (AdaCore/RecordFlux#1289, eng/recordflux/RecordFlux#1437)
• Fatal errors caused by condition on message type field (AdaCore/RecordFlux#1291, eng/recordflux/RecordFlux#1438)

Removed

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

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)

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)

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 (AdaCore/RecordFlux#1204, eng/recordflux/RecordFlux#1204)

Changed

• Prevent unnecessary runtime checks in generated code (AdaCore/RecordFlux#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 (AdaCore/RecordFlux#1267, eng/recordflux/RecordFlux#1267)
• Subsequent errors caused by style errors (AdaCore/RecordFlux#1268, eng/recordflux/RecordFlux#1268)
• Missing type checking in refinement conditions (eng/recordflux/RecordFlux#1360)
• Exception caused by comparing integer field to aggregate (AdaCore/RecordFlux#1251, eng/recordflux/RecordFlux#1251)
• Unexpected errors when using --max_errors=1 (AdaCore/RecordFlux#825, eng/recordflux/RecordFlux#825)
• Incorrect detection of conditions as always true for enumerations with Always_Valid aspect (AdaCore/RecordFlux#1276, eng/recordflux/RecordFlux#1276)
• Potential name conflicts with internally used identifiers that start with RFLX_ (AdaCore/RecordFlux#638, eng/recordflux/RecordFlux#638)
• Deadlocks during verification caused by forked processes (eng/recordflux/RecordFlux#1366)