New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Release version 0.4.1 #340

Closed

4 tasks done

treiher opened this issue Jul 14, 2020 · 0 comments

Assignees

Collaborator

treiher commented Jul 14, 2020 •

edited

Loading

Add version to limitations labels
Update limitations link in README
Change version in code
Upload to PyPI

Release Notes Draft

Specification / Model

Improve error messages (Refactor error message #248)
Add GNAT Studio integration (GNAT Studio integration #243)
Add more checks for invalid models (Insufficient model verification regarding comparisons of opaque fields #282, Missing check of size and alignment of opaque fields #288, Enums with identical literals not always detected #298, Missing check for naming conflicts between field names and literals #309, Missing check of field type in refinement #310, Missing check of element type of array #311, Incorrect check of maximum literal value #313, Underflow not detected for range length field #336, New-line and missing location in conflict info #338)
Fix erroneously rejected specifications (Contradiction check too strict #277, Defining array with element type of other package not possible #347, Prefixed enumeration literals not correctly handled in proofs #351)
Improve parsing performance (Additional parentheses cause significant increase of parsing time #305)

SPARK Code Generation

Allow use of scalars up to 64 bit (Scalars with size greater than 57 bit #238)
Prevent potentially failing code compilation (Compilation fails due to range integer with single value #312, Compilation fails due to range integer using full value range #314, Compilation fails due to enumeration using full value range #315, Compilation fails due to suspicious modulus value #316, Compilation fails due to comparison with aggregate #319, Compilation fails due to comparison of big integers #320, Name conflicts between literals and field names in SPARK code #329, Compilation fails due to use of array with element type of other package #349)
Allow setting empty sequence field (Setting empty sequence field #353)
Fix comparison of field values with aggregate (Invalid code generation for comparison of field and aggregate #328)
Improve verifiability of accesses to opaque fields (Missing SPARK_Mode in generic Write procedures in tests #287)
Fix handling of empty prefixes (Using an empty prefix generates invalid file names #266)

PyRFLX

Improve performance (PyRFLX performance #254)
Fix determining of predecessor field (PyRFLX: prev_field does not return correct predecessor field #289)
Fix handling of prefixed literals (Missing substitution of qualified enumeration literals in conditions #346)

treiher self-assigned this

treiher closed this as completed

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment