Development Log in categories SPARK Pro

  • SPARK Pro
    Feb 15th, 2017

    Contracts for formal containers with model functions
    The formal containers library, which provides SPARK-compatible versions of Ada containers, has been enriched with comprehensive contracts. These contracts use functional, mathematical-like containers as models of imperative containers.

  • SPARK Pro
    Feb 5th, 2017

    Different message for floating point overflows
    Previously, for overflows on integer types and floating point types, the SPARK check message mentioned simply "overflow check". This made it difficult to know if the check was an overflow on integers or floating point numbers. Now, the message for floating point overflow checks mentions "float overflow check". The message for integer overflow is unchanged.

  • SPARK Pro
    Jan 31st, 2017

    New switch—no-inlining prevents inlining for proof
    The special inlining used in GNATprove to increase the precision of proof may be harmful in some cases, as it increases precision at the cost of longer running time and greater memory usage. GNATprove now supports no inlining under switch --no-inlining.

  • SPARK Pro
    Jan 25th, 2017

    SPARK tools produce more information about VCs
    Previously, it was hard to see which VCs were produced for a given check, and which prover was used to attempt to prove it. Now, this information is stored in the .spark files that are produced by GNATprove. The content of these files is now documented.

  • SPARK Pro
    Jan 23rd, 2017

    New lemmas on monotonicity of float operators
    The SPARK lemma library includes six new lemmas on the monotonicity of the float addition, substraction, multiplication and division.

  • SPARK Pro
    Jan 12th, 2017

    Check default of private types at declaration
    GNATprove now checks that no runtime error can occur during the default initialization of private types once and for all at the declaration of the type. This enforces a cleaner separation of library code from user code, allowing for an easier integration of proof with other verification means (tests, review...).

  • SPARK Pro
    Jan 6th, 2017

    Support for arbitrary lengths of entry queues
    GNATprove now supports arbitrary lengths of entry queues (which are specified by the Max_Queue_Length and Max_Entry_Queue_Length pragmas). This feature is only applicable when the GNAT Extended Ravenscar profile is active.

  • SPARK Pro
    Jan 5th, 2017

    Add message on proved termination
    When GNATprove is able to prove a Terminating annotation an info message is issued.

  • SPARK Pro
    Jan 5th, 2017

    Support of caching using memcached server
    The SPARK tools now support caching large parts of the analysis via a memcached server. If a memcached server is available to store analysis results, and this server is specified to GNATprove via the command line option --memcached- server=hostname:portnumber, then subsequent invocations of the tools, even across different machines, can store intermediate results of the tools. The user-visible effect is that GNATprove can produce results faster.

  • SPARK Pro
    Dec 21st, 2016

    More precise analysis for exclusive use of entries
    Tasks were previously only allowed to call the same entry if they were using entries belonging to different (library-level) objects. Now GNATprove also accepts calls from more than one task to a single entry provided that each task uses an entry belonging to a different component of a record object.

  • SPARK Pro
    Dec 9th, 2016

    Better termination error messages
    Every error message related to termination referred to a subprogram without specifying the name. This further information is now emitted.

  • SPARK Pro
    Dec 7th, 2016

    Only check component subtype at first declaration
    GNATprove now only checks subtype indications on record components when verifying the declaration of the first record type defining this component. This avoids having multiple checks on record component subtype indications, some of which could be undischarged due to missing information.

  • SPARK Pro
    Dec 1st, 2016

    Assume value of string literals
    GNATprove now knows precisely the value stored in a string literal which will result in more proofs when string literals are involved.

  • SPARK Pro
    Nov 23rd, 2016

    Improved error message
    In case of a subprogram having an output global which is used as an input of the subprogram in its body we now provide more information on the error message.

  • SPARK Pro
    Nov 22nd, 2016

    Better interval analysis of int to float conversions
    Interval analysis is a simple analysis that allows proving range checks and overflow checks simply by computing the worst-case bounds of expressions based on the types of subexpressions. This analysis now also deals precisely with conversions from integers to floating-point types, which improves provability of programs with such conversions.

  • SPARK Pro
    Nov 22nd, 2016

    Remove trivial checks on float-to-int conversions
    Range checks on float-to-int conversions that can be proved to be always passing by trivial interval analysis of the types of subexpressions are not emitted anymore. This improves provability of programs where such conversions are used, as automatic provers sometimes had difficulty proving range checks on such conversions.

  • SPARK Pro
    Nov 21st, 2016

    New lemma on array ordering
    We have added a new lemma for sorted arrays in the SPARK lemma library. This lemma allows proving ordering between arbitrary elements of the array using transitivity of the order.

  • SPARK Pro
    Nov 10th, 2016

    Loop invariant generation for preserved components
    GNATprove can automatically generate loop invariants specifying the preservation of array and record components that are not modified during a loop. This generation is a heuristic which only works in the most common cases.

  • SPARK Pro
    Nov 9th, 2016

    Types with partial default initialization allowed
    Types with partial default initialization were previously not allowed in SPARK, which made it difficult to analyze some existing codebases. They are now allowed.

  • SPARK Pro
    Nov 8th, 2016

    Improve provability of checks in loops
    Checks whose proof depends on assuming the loop invariant at the current iteration of the loop could be unprovable due to part of the loop invariant being simplified to True or False. This simplification is now disabled in assertions to improve provability of checks in loops.

  • SPARK Pro
    Nov 3rd, 2016

    more precise volatility for protected objects
    A new rule 7.1.2(16) was added to SPARK RM, along with SPARK tool updates, to better control the volatility of protected objects. Previously they were fully volatile, now they have only Async_Readers and Async_Writers. If a separate volatile variable is a Part_Of such a protected object, the protected object inherits any volatility aspects (i.e. Effective_Reads or Effective_Writes) of its Part_Of constituent.

  • SPARK Pro
    Nov 2nd, 2016

    Division checks now proved by CodePeer integration
    Division by zero checks can now be proved by the CodePeer integration in SPARK, which was not the case previously.

  • SPARK Pro
    Nov 2nd, 2016

    Assertion checks now proved by CodePeer integration
    Assertion checks (pragma Assert, Loop_Invariant, Assert_And_Cut) can now be proved by the CodePeer integration in SPARK, which was not the case previously.

  • SPARK Pro
    Oct 31st, 2016

    Nested loops allowed before a loop (in)variant
    A limitation in GNATprove forbade nested loops before loop (in)variants. This limitation has been removed.

  • SPARK Pro
    Oct 27th, 2016

    Better handling of always-fail subprograms
    Subprograms where all possible execution paths end in an exception are now dealt with in a more obvious fashion. Instead of raising many checks and warnings, we now emit only a single high check indicating that no path will return normally.

  • SPARK Pro
    Oct 26th, 2016

    Improve tracking of bounds of array aggregates
    GNATprove now does a better job of tracking the bounds of aggregates of dynamic array types, resulting in more discharged checks on array aggregates.

  • SPARK Pro
    Oct 20th, 2016

    level switch uses time limit instead of step limit
    The level switch used to provide a high level way of tuning the verification condition now sets time limits instead of step limits for provers. As a result, this switch is more predictable, as it always allows each prover to run for the same amount of time, but less deterministic, as the time needed for a prover to complete a proof may vary depending on the computer.

  • SPARK Pro
    Sep 29th, 2016

    Integration of Codepeer Technology into SPARK
    The CodePeer Static Analysis engine is now part of the SPARK tools. It can be enabled using the command line switch --codepeer=on, or selected via a new checkbox in the SPARK integration inside GPS. If this is done, SPARK will run the CodePeer engine prior to its own analysis to discharge checks. Depending on the project and kinds of checks, this can result in more proved checks, or quicker completion of analysis, because SPARK doesn't need to analyze some checks already proved by the CodePeer analysis. The strong point of the CodePeer static analysis are ranges of variables, including floating-point variables. As a result, proof of runtime checks will be improved if the CodePeer engine is used.

  • SPARK Pro
    Sep 29th, 2016

    Ability to replay proofs using SPARK
    The SPARK tools now support a new switch --replay. If this switch is passed to GNATprove, it will attempt to replay the proofs of all checks that are marked as proved in the proof session, using for each VC the same prover that succeeded in proving it, and a time and steps limits that were sufficient to make the proof succeed. This feature provides an efficient way of checking that all proofs still go through, e.g. after an upgrade of the SPARK tools.

  • SPARK Pro
    Sep 28th, 2016

    Use SMT-LIB float theory with prover Z3
    GNATprove can now benefit from SMT solvers with native floating- point support. In particular GNATprove uses this support in prover Z3, which gives more precise results on floating-point programs.

  • SPARK Pro
    Sep 27th, 2016

    Support for type invariants
    The tools now have initial support for type invariants (SRM 7.3.2). A type invariant can be specified on the completion of a private type. This invariant can be assumed anywhere outside the package where the type is declared; and is checked inside the package. Type invariants are useful to simplify a common pattern where an invariant is added to the pre- and post-conditions of all subprograms in a package.

  • SPARK Pro
    Sep 22nd, 2016

    Better handling of ‘Length on modular index types
    The translation of the 'Length array attribute has been improved to avoid unecessary conversions when the index type is a modular integer type. This should improve provability whenever 'Length is used on a modular index type in contracts.

  • SPARK Pro
    Sep 9th, 2016

    Suppressed unnecessary warning message
    For a null default subprogram defined in the formal part of a generic unit, now GNATprove does not emit a warning about formal parameters of the subprogram being unused and/or unmodified.

  • SPARK Pro
    Aug 29th, 2016

    Assume Initial_Condition of withed units
    When checking compilation units, we now assume that the Initial_Condition aspect of each withed unit holds. It results in more discharged verification conditions in particular on main units.

  • SPARK Pro
    Aug 29th, 2016

    Counterexamples involving quantified expressions
    Some counterexamples are now printed for universally quantified variables (in loop invariants for example).

  • SPARK Pro
    Aug 16th, 2016

    Improved documentation
    The UG section 8.6.4. Proof Limitations does now better document the support for storage place attributes. In particular, it states that First_Bit, Last_Bit and Position attributes are supported but in case there is no record representation clause then their value is assumed to be nonnegative.

  • SPARK Pro
    Aug 5th, 2016

    More fine-grain placement rules for pragma Annotate
    Previously, if pragma Annotate was placed e.g. at the start of a statement list, it would apply to the whole enclosing construct (e.g. an if statement including all branches and statements). Now it only applies to the range between the beginning of the enclosing statement and the pragma itself. This allows to e.g. apply a pragma Annotate to the condition of an if-statement, but not the other parts of the if-statement. Note that this may require changes to the placement of pragma Annotate in existing code, or more pragma Annotate than before.

  • SPARK Pro
    Aug 1st, 2016

    Support for GNAT attribute System’To_Address
    GNAT attribute System'To_Address, which is a static attribute equivalent to a call to System.Storage_Elements.To_Adress, is now supported.

  • SPARK Pro
    Jul 28th, 2016

    Improved precision on tagged conversion
    When a tagged type was converted, information about the value of its components was lost, and so, even when converting between types which are conceptually the same (tagged subtypes and derived types with null extension). Tagged conversion are now better handled in proof.

  • SPARK Pro
    Jul 21st, 2016

    Improve posting of SPARK violations
    SPARK violations are now posted on the entity that is not in SPARK rather than on the entity that will result not to be in SPARK for this violation. This is done for formal parameters of a function, return types of a function and indexes of an array.

  • SPARK Pro
    Jul 16th, 2016

    Take into account contracts on abstract subprograms
    When an abstract subprogram with a classwide contract is called from an annotation, its postcondition is now available for proof.

  • SPARK Pro
    Jul 15th, 2016

    More convenient support for Coq interactive prover
    Previously, to be able to use the Coq interactive prover with SPARK, it was required to create a why3.conf file with the appropriate configuration. Now, SPARK comes with the suitable configuration already included, and this extra step is not needed any more. The Coq prover still needs to be installed separately.

  • SPARK Pro
    Jul 15th, 2016

    New GPS panel for examine menu in spark2014 tab
    Menus 'Examine ...' in GPS now open a panel similar to the basic panel displayed for proof. In particular, it allows to choose between three modes of analysis: check, check all, and flow analysis.

  • SPARK Pro
    Jul 7th, 2016

    More fine-grained proof of checks using “and”
    Assertions, loop invariants and pre- and postconditions which consist of several parts combined with "and" or "and then", are now proved seperately by SPARK. This allows better reporting of which part of the check is unproved, and it also allows better interaction between provers, where one prover may be able to prove one part of the heck, and another one the remaining part.

  • SPARK Pro
    Jul 7th, 2016

    New mode which outputs current state of analysis
    Previously, finding out which checks are proved or unproved required rerunning the tools, which could take quite some time. We now have added a new check-box to the proof dialog which is opened after selecting the "Prove All", "Prove File" and similar menu entries. Selecting this check-box will run gnatprove as usual, but no provers will be run, only existing results will be used. In this way, this option provides a relatively quick way to assess what's currently proved and not proved. The same behavior can be achieved on the command line, by adding the switch --output-msg- only,

  • SPARK Pro
    Jul 6th, 2016

    Support for enumeration types in counterexamples
    The counterexamples output by GNATprove when a check is not proved now display correct enumeration literals for variables of enumeration types.

  • SPARK Pro
    Jun 23rd, 2016

    New check_all mode for GNATprove
    GNATprove now has a new mode for running the SPARK tools. This is the check_all mode, in which a full check of SPARK legality rules is done.

  • SPARK Pro
    Jun 16th, 2016

    Improved info messages on objects initialization
    Now we emit info messages for every constituent of an abstract state, including protected objects. Also, we only emit info messages on initialized objects if they are mentioned in an Initializes aspect.

  • SPARK Pro
    Jun 15th, 2016

    Entry guards are now taken into account
    GNATprove now also takes into account the boolean expression provided as a guard of an entry of a protected type. This was previously not the case.

  • SPARK Pro
    Jun 6th, 2016

    Support optional refinement in private part/child
    SPARK Reference Manual now allows refinement through the use of pragma or aspect Refined_Global and/or Refined_Depends in scopes where the full refinement of an abstract state is not visible, like the private part of the package defining the abstract state, or one of its child packages. The special rules in SPARK RM 7.2.4 for this so-called optional refinement are now supported in GNAT and GNATprove.

   1  2  3     Next »