Development Log in categories SPARK Pro

  • SPARK Pro
    May 11th, 2017

    Added preconditions to standard numerical functions
    Preconditions have been added to functions from the standard numerical package Ada.Numerics.Generic_Elementary_Functions, in cases that may lead to Numerics.Argument_Error or Constraint_Error when called on actual parameters that are not suitable, like a negative input for Sqrt. This ensures that GNATprove generates corresponding precondition checks when such functions are called.

  • SPARK Pro
    May 10th, 2017

    Precise handling of dispatching calls with known tag
    GNATprove now precisely determines the subprogram called by a dispatching call when the tag is known. In particular, it is now able to use its more precise specific contract if any.

  • SPARK Pro
    May 5th, 2017

    Improve message for functions that could not return
    GNATprove used to emit a confusing check about initialization of functions when it could not determine if a function would return. We have now improved the message for this check. In addition, when encountering a potentially non returning function, GNATprove will now precise if the function may not return on some or on every path.

  • SPARK Pro
    May 3rd, 2017

    Use unique names for private record parts
    GNATprove now generates unique names for the Why3 translation of private parts of distinct record types. This should facilitate mappings of these parts to distinct types in interactive theorem provers.

  • SPARK Pro
    May 2nd, 2017

    Use unique names for simple private types
    For simple private types (untagged private type with no discriminants and full view out of SPARK) we now use unique names in Why3 so that they can easily be mapped to distinct existing types in interactive provers.

  • SPARK Pro
    Apr 20th, 2017

    Better handling of powers of 2 in modular types
    GNATprove now handles better powers of 2 that are of a modular type, leading to better proof results. This improvement only concerns modular types whose modulus is itself a power of 2.

  • SPARK Pro
    Apr 20th, 2017

    Better handling of discriminant-dependent components
    GNATprove now handles accesses to discriminant-dependent record components better, leading to more proofs and less spurious trivial checks on such components.

  • SPARK Pro
    Apr 19th, 2017

    Improved handling of compile-time-known assertions
    Assertions that are known to be true at compile-time are now handled in a more efficient way by the SPARK tools. This results in shorter running times on projects that contain such assertions.

  • SPARK Pro
    Apr 13th, 2017

    Protect against unsound function contracts
    When a function has an inconsistent contract (a contract which cannot hold for some inputs), GNATprove used to generate an unsound axiom which may then allow to prove anything in a caller of such a function, and so, even if the function is always called on 'valid' inputs, that is, inputs on which the contract holds. Though this behavior is expected with a proof technology such as SPARK, it used to come as a surprise to some users. We now avoid generating unsound axioms as much as possible by introducing guards for function axioms which are only assumed to hold on actually used values. Note that there are still cases where an unsound axiom will be generated (functions called in type invariants / type predicates, in primitive equalities of record types, or sometimes in user written quantified expressions). As a consequence, having inconsistent contracts on functions is still a bad usage of SPARK, and users should avoid it as much as possible. Also, this new 'safer' translation can sometimes impact proof capabilities. Thus, we provide an advanced switch --no-axiom-guard to disable it.

  • SPARK Pro
    Mar 30th, 2017

    Globals of renamed subprograms in code not-in-SPARK
    GNATprove now synthesizes more precise Global contracts for subprograms annotated with SPARK_Mode => Off that make calls via subprogram renamings. Such calls happen, for example, in instances of generic units with formal subprogram parameters.

  • SPARK Pro
    Mar 24th, 2017

    Empty “others” alternative in Case statement
    Flow analysis now detects when an "others" alternative of a Case statement corresponds to an empty range and effectively considers its sequence of statements as unreachable. This helps to avoid spurious messages about variables not being referenced or initialized within that sequence of statements.

  • SPARK Pro
    Mar 21st, 2017

    Simplified translation of simple private types
    Untagged private types with no discriminant whose full view is not in SPARK are now translated in Why3 as clones of the predefined __private abstract type. This should allow users of interactive proof assistants to more easily map these private types to a logic type of their choice.

  • SPARK Pro
    Mar 20th, 2017

    Theories for conversion of discrete types realized
    The Why3 theories used by GNATprove to model conversions between discrete types have been realized in Coq. This increases confidence in their correction.

  • SPARK Pro
    Mar 9th, 2017

    New switch produces header in gnatprove.out
    The new switch --output-header produces a header in the generated file gnatprove.out, with useful information about the run of GNATprove, such as the version number, date, host platform and switches used.

  • SPARK Pro
    Feb 24th, 2017

    Dynamic type constraints of protected components
    GNATprove now better tracks dynamic type constraints of protected components, such as dynamic bounds, predicates and invariants. This results in more automatic proof on protected operations or their callers, whenever types of protected components have some dynamic constraints.

  • 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).

   1  2  3     Next »