to allow for a "fast" version using memcpy and a "provable" version that uses
Ada assignment statements. The fast version disables SPARK_Mode at the package body
level, whereas the "provable" version does not.
There are two package bodies implementing this copying facility, for a single common
package decl (that has SPARK_Mode enabled). Thus there are two source files.
Define and use a scenario variable to control the selection of the source file to
use as the body of this package.
re-enable pragma Assertion_Policy (Pre => Check) since we need those because we are not proving clients
formatting for readability
replace unsigned 32 type used for indexes with a signed 64-bit type having the same range
fix off-by-one for post in Unbounded_Slice
For the other two Append routines' postconditions, replace the calls
to the Head functions with explicit quantified expressions using Element.
Give complete post for Slice and Unbounded_Slice functions
formatting
move the two lemma procs for Get_*String to package level and name them with "Lemma_" prefix
formatting and comment cleanup
the two Get_* for strings now prove, with Claire/Joffrey's lemma in place and change to post in unbounded strings package
apply gnata to unbounded strings package
disable pragma requiring pre checks only, until finished developing proofs
comment fixes etc
make function Element be an expression function in the spec for the sake of proof, which means we need to enable the preconditions as well.
full post for Append routines
minor formatting
take the post off Equal so it can be inlined
on ghost function Equal, we don't need the precondition, and we can at least have a little postcondition
remove commented-out Raw_Slice
general improvements
add stored length checks in calls to Get_Unbounded_String
move the Stored_Length Raw_Bytes check up in the postcondition
simpler postcondition
add post to verify Stored_Length at the right position in Get_Unbounded_String
clean up comments
new Get_String postcondition verifying Stored_Length in Raw_Bytes
minor subprogram decl reordering
add comments
weaker preconditions on Put_* numerics
correct a comment
Get_Real* both now have postconditions verifying that
the value returned in the parameter corresponds to the
raw bytes starting at the Position when Get was called
don't need the Bswap* intrinsics
minor formatting
simplified preconditions on Get_* for the two reals
Get_UInt32 at First now proves successfully
Get_UInt32 at First still not proving, but has parts we want to keep anyway
all the Get_* for ints are proving complete postconditions, except for
Get_UInt32 that specifies an absolute position via First
proving with less preconditions
use correct conversion routines for actuals passed to lemma proc
intermediate version of ByteBuffers package that successfully provers
a postcondition for Get_Int16 saying that the two bytes equal the retrieved parameter value returned
formatting
make and use a New_Content_Equal function for Byte_Array too
while package proves successfully (--level=4 --proof=progressive)
Remove post on Raw_Bytes returning Byte_Array since it is an expression function and this would preclude inlining (and is not useful anyway)
For Raw_Bytes returning String, remove useless Pre for Min_String_Length and make Post reflect actual body
remove unnecessary conversion
no use of Retrieve_x_Bytes generic
framing conditions for all Put routines in place and proving successfully!!
Get_String and Get_Unbounded_String can have postconditions simplified and strengthened;
the precondition for Get_Unbounded_String can be weakened
The final, additional byte comparisons for numeric insertion routines' postconditions are partially implemented and not proving yet
In the body, comment out the expected-to-be-unused for proof code.
remove commented-out pragma Annotate
Put_Raw_Bytes for String now proves, so now all routines do.
Next: we need to augment the numeric insertion routines'
postconditions to test that the Content slice actually
contains the argument value passed to insert
now proving Put_Raw_Bytes for input of type ByteArray
inserting into cm (permanently)
Put_Raw_Bytes can allow zero-length input arrays
simpler preconditions, but Put_Raw_* still don't prove
remove Ada2020 switch
inserting
minor formatting
Put_Raw_Bytes for Byte_Array doesn't need to check that Value'Length <= Index'Last
Put_Raw_Bytes procs don't require Value'First = 1
New_Content_Equal need not require Comparand'First to be 1
Make New_Content_Equal allow empty string input
Have Put_String and Put_Unbounded_String call New_Content_Equal and Prior_Content_Unchanged
slight refinement
additional assertions at end
intermediate commit, Put_Raw_Bytes still a problem
minor formatting
remove Length references and proc Clear
In Put_Raw_Bytes taking a Byte_Array, add the loop invariant saying that the prior content was unchanged
Intermediate checkin:
Many framing conditions proved, but not Put_Raw_Bytes
for the bytearray type
Lacking the Post for checking that the integers/real
values inserted into buffers are written where expected
update text in justifications for unchecked conversion to reals in Get_Realxx
remove Get_String_with_Recovery, per discussion with Laura
Get_Unbounded_String proves now, with modified Ada.Strings.Unbounded
First pass at Put_Raw_Bytes framing condition, not proving yet
better names for subtypes Count and Buffer_Size
ensure no wrap-around
add wrapper for memcpy, currently in comments
get unbounded strings not yet proving; needs pre/post in Ada.Strings.Unbounded
trivial indentation fix
all routines classwide now, except for Get_String_With_Recovery which won't prove without the pre/post being classwide
Get_String and Get_String_with_Recovery prove successfully.
Working on the Unbounded_Strng version.
intermediate commit, Get_String post is not proving yet
scalar stuff proves
* fix casing for generated/copied files, for TB04-026
* Add docstrings, remove redundant calls.
Docstrings are added to elements that are introduced in this change set
or are updated by this change set. The intent of the docstrings is to
explain the purpose of the various elements and, where appropriate,
suggest how they might be improved going forward.
There were several instances of redundant calls to the `SPECIAL_CASING`
map or to `getDeconflictedName`. These have been eliminated. Similarly,
redundant calls to `toLowerCase` have been eliminated where possible.
The `descending_namespace_spec` method has been significantly edited to
improve code quality.
* Previously flagged redundancies are removed. Most variables have been
marked final. There were many instances of reuse of local variable
for a different purpose, which challenges readability and maintenance;
these have been eliminated and protected against through the
systematic use of `final`.
* Inefficient string concatenation (concatenating strings with
variables) are replaced by use of `MessageFormat`.
* Multiline strings are (efficiently) broken across over multiple lines,
for readability.
More could be done to improve `descending_namespace_spec`, specifically
to eliminate the for loops; possibly a recursive implementation would
fit well. That was not undertaken for this commit.
For testing, Ada sources were generated from all MDMs and spot-checked
for reasonableness.
Co-authored-by: rogers <rogers@adacore.com>
* prevent numeric overflow when working with huge strings
* now raise an exception when reading a string length > message length
* now preconditions prevent inserting a string with length great than UInt16'Last
* add unit test program
* calculate_packed_size_body must first call ancestor version
* first clear vector contents before loading them here
* correct handling for Get_Unbounded_String
* correct value used for subscriptions in series template specs
* better pre/post
* additional contracts; minor formatting
* allow putting empty unbounded_strings into buffers
* must account for 'Size that is less than 8, such as Boolean
* unpack object components into record components instead of local temp
* generate a full gpr file with generated sources
* enable warnings but not about unused/redundant entities
* fix typo in comment
* minor refinement to preclude warning msg
* Update AdaMethods to use Formal Containers
Now using formal containers, with a set size of 200. Many updates to required because the formal containers are not tagged types and cannot use the distinguished receiver syntax.
* Revert "Update AdaMethods to use Formal Containers"
This reverts commit c9af76c1f5.
* Correct the checksum calculation and usage
Co-authored-by: rogers <rogers@adacore.com>
Update existing verification code (python and C++) to test their xml
serialization/deserialization functions using the generated reference binary
byte streams.
