Development Log in categories SPARK Pro

  • SPARK Pro
    Jun 6th, 2016

    Support optional refinement in private part/child
    SPARK Reference Manual now allows refinement through the user 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.

  • SPARK Pro
    Jun 6th, 2016

    Global variables known to be initialized in loops
    GNATprove now knows that in out global variables and parameters that are modified in loops are always initialized and thus are in their types. In particular, variables are in their range for scalars and their dynamic predicate is true if they have one.

  • SPARK Pro
    Jun 3rd, 2016

    Suppressed wrong warning message for X’Address
    SPARK does not look at X in X'Address as a used variable anymore and therefore it does not emit a warning message in case X is not initialised.

  • SPARK Pro
    May 23rd, 2016

    SPARK lemma library for nonlinear int arithmetic
    SPARK now comes with a library of lemmas separately proved in Coq, that can be called in user code to automatically prove nonlinear integer arithmetic properties, i.e. properties involving multiplication, division, modulo. The lemmas are ghost procedures, hence they are removed from the final executable when compiling without assertions. This library of lemmas is meant to be extended based on user needs. It is documented in the SPARK User's Guide, in section 4.10 about SPARK Libraries.

  • SPARK Pro
    May 16th, 2016

    Do not re-use files from previous versions of SPARK
    Intermediate files in the gnatprove directory from previous versions of the tools could mislead later versions of the tools, sometimes resulting in confusing crashes or confusing error messages. We now detect any such version mismatch and issue a prompt to clean up.

  • SPARK Pro
    May 12th, 2016

    Support for pragma Unused/Unreferenced/Unmodified
    SPARK now has support for pragma Unused, Unreferenced and Unmodified. We silence warnings (but not checks) about variables that have been mentioned in one of these pragmas; they can be used as an alternative to pragma Warnings Off.

  • SPARK Pro
    Apr 17th, 2016

    More flexible elaboration rules with static model
    GNATprove now implements a more flexible enforcement of SPARK elaboration rules, that does not always requires Elaborate_All for calls and reads of subprograms and variables defined in other units during elaboration. Specifically, when the static elaboration model of GNAT is used (i.e. when neither switch -gnatE nor pragma Elaboration_Checks (Dynamic) are used), the more powerful mechanism of the compiler is used to compute a safe elaboration order for calls across units during elaboration, and GNATprove only requires the use of Elaborate_Body on units that modify the value of library-level variables defined in the spec during the elaboration of the unit body (SPARK RM rule 7.7.1(5)).

  • SPARK Pro
    Apr 7th, 2016

    More options for reporting of results
    The --report switch of the gnatprove tool now provides one more option to select from. If the option --report=provers is selected, gnatprove will show information about which provers have contributed to the proof of each check.

  • SPARK Pro
    Mar 31st, 2016

    Deterministic proof by default with no timeout
    GNATprove is now deterministic by default, so it does not use timeouts unless explicitly instructed by the user to do so. Instead, a steps limit is used to bound the effort made by automatic provers to find a proof. This new design is based on a few changes: the proof level (switch --level) is 0 by default, proof level sets a value of steps but no value of timeout, switch --timeout takes a new value "auto", in addition to a possible time in seconds. The semantics of --timeout=auto is that it adjusts to the value of the proof level.

  • SPARK Pro
    Mar 31st, 2016

    Always generate axiom for expression function
    Previously, no axiom was generated for an expression function in a part of code with no explicit SPARK_Mode, which prevented proofs of client code that relied on the implicit postcondition of the expression function. Now, an axiom is generated in such a case.

  • SPARK Pro
    Mar 22nd, 2016

    Use stable names for aggregates used in definitions
    Aggregates used as initialization expressions in the declaration of objects now get transformed in Why3 into modules and functions with a stable name across versions in GNATprove, based on the name of the object they define. This eases maintenance of manual proofs done in interactive provers.

  • SPARK Pro
    Mar 21st, 2016

    Reproducible generation of VCs
    Previously, proof oblications (or VCs) generated by SPARK could be slightly different from one run of SPARK tools to the other. Now, if the source files have not changed, exactly the same VCs will be generated. This is useful if external tools are used to track or cache such VCs.

  • SPARK Pro
    Mar 15th, 2016

    Allow to disable steps limit
    The --level switch of GNATprove sets a steps limit, and it was previously impossible to disable this steps limit without removing the --level switch entirely. Now one can add the switch --steps=0 to the GNATprove command line invocation to keep all the settings of the --level switch and only disable the steps limit.

  • SPARK Pro
    Mar 15th, 2016

    Specific attributes as valid volatile context
    A reference to a volatile object with enabled properties Async_Writers or Effective_Reads can now safely appear as the prefix of attributes Address, Alignment, Component_Size, First_Bit, Last_Bit, Position, Size, Storage_Size.

  • SPARK Pro
    Dec 23rd, 2015

    Fine-grain analysis of generic code in GPS
    It is now possible to use the submenus "Examine Subprogram", "Prove Subprogram", "Prove Line" and "Prove Check" (from the contextual menu in GPS) from within a generic unit, which has the effect of applying the desired analysis on all instances of the generic unit. The same effect can be obtained on the command-line by using switch -U in addition to the required switches --limit-subp and --limit-line, although the main benefit is expected to be for interactive use in GPS.

  • SPARK Pro
    Dec 15th, 2015

    Better support for use of Why3 IDE
    For advanced users and mainly in connection with manual proof using interactive proof assitansts such as Coq and Isabelle, it can be useful to use the Why3 IDE (not provided by AdaCore) to inspect and modify the session file. This use case is now better supported, mainly it is easier to see what SPARK check a VC corresponds to.

  • SPARK Pro
    Dec 9th, 2015

    Generics’ formals can now appear on contracts
    The SPARK toolset now allows user provided contracts that are placed on generics to refer to the generics' formals.

  • SPARK Pro
    Nov 20th, 2015

    Better support for ‘Update of arrays
    The SPARK toolset now has a better understanding of the 'Update attribute related to array updates. In particular previously SPARK did not know that the attribute could not change the bounds of the underlying array. SPARK now uses this information and this leads to more proofs related to array bounds, array length and array equality, when the 'Update attribute is involved.

  • SPARK Pro
    Nov 20th, 2015

    Continue compilation/analysis on division by zero
    When SPARK_Mode is On, GNAT and GNATprove implement stricter rules than those mandated by Ada RM, by issuing errors on compile-time known constraint errors instead of warnings and unproved check messages. This was the case for divisions by zero which appear legitimately in deactivated code. Such divisions by zero do no stop compilation and analysis anymore, instead a check is generated by GNATprove during proof.

  • SPARK Pro
    Nov 19th, 2015

    SPARK uses transformations in Why3 session file
    If the Why3 session of SPARK is modified using other tools (e.g. the why3ide tool), and extra transformations are inserted into the session tree, then SPARK will now use this information and "follow" these transformations. This allows a better use of external tools such as why3ide in combination with SPARK, for example to apply transformations that help automatic proof, or for manual proof.

  • SPARK Pro
    Nov 18th, 2015

    Global refinement of In_Out abstract state
    An abstract state classified as In_Out in a Global annotation can now be refined by the following combinations of constituents: 1) At least one constituent must be of mode In_Out, 2) At least one constituent must be of mode Output and at least one constituent must be of mode Input or Proof_In.

  • SPARK Pro
    Nov 12th, 2015

    Generic formals as initialization items
    Generic formal parameters can now appear in the input_list of an initialization_item within aspect or pragma Initializes.

  • SPARK Pro
    Nov 10th, 2015

    Display correct counterexample values in loops
    If there is both counterexample value for a variable in the first iteration of a loop and a counterexample value for the same variable after the first iteration, only the former one was displayed by GNATprove. However, in this case, the counterexample value after the first iteration is relevant and thus GNATprove now displays this value in the counterexample.

  • SPARK Pro
    Nov 10th, 2015

    Better provability of conversion between floats
    It is now easier to prove that conversions between floating-point types preserve the value converted, when both the source and the target types are single (resp. double) precision floating-point types.

  • SPARK Pro
    Nov 9th, 2015

    External abstract state refinement
    The refinement of an external abstract state can now mention non-external constituents.

  • SPARK Pro
    Nov 6th, 2015

    Display array bounds in counterexamples
    GNATprove now displays values of attributes 'First and 'Last for values of array types in counterexamples.

  • SPARK Pro
    Nov 5th, 2015

    Support for Ghost and tagged type inheritance
    The SPARK toolset now supports Ghost derived types as well as inheritance and overriding of primitive Ghost subprograms.

  • SPARK Pro
    Nov 5th, 2015

    Issue low severity message on string concat
    Range checks on string concatenations are likely to be unprovable due to missing ranges on arguments of the concatenation. Issue a low severity message in such a case, instead of the default medium severity for unproved proof checks.

  • SPARK Pro
    Nov 4th, 2015

    Distribute Crazyflie as documented example
    The stabilization code of the small leisure drone Crazyflie, rewritten in SPARK and proved free of run-time errors, is now distributed with SPARK, and documented in the SPARK User's Guide.

  • SPARK Pro
    Nov 2nd, 2015

    Improved provability of predicates with subtypes
    When a subtype of a type with predicate was created, its inherited predicate was leading to unprovable checks. Such inherited predicates are now better handled in proof.

  • SPARK Pro
    Nov 2nd, 2015

    Optional dependence of task unit on itself
    Aspects or pragmas Depends and Refined_Depends may now omit the dependence of the current instance of a task unit on itself.

  • SPARK Pro
    Oct 23rd, 2015

    Generation of counterexamples for unproved checks
    GNATprove can now generate counterexamples when a check is not proved, to give the execution path for which the check cannot be proved, as well as values of variables that occur on this path. The counterexample is best displayed in GPS by clicking on the icon "Show counterexample" on the left of the check message or line in the editor. The message itself may detail the values from the counterexample for variables that appear in the checked expression. For details, see section 6.3.5 "Understanding Counterexamples" in the SPARK User's Guide.

  • SPARK Pro
    Oct 21st, 2015

    Support for tasking - RavenSPARK
    The SPARK language and toolset have been extended to support tasking under the Ravenscar profile. On the language side we have added support for protected objects, suspension objects, tasks and synchronous state. The toolset also statically checks all restrictions of the Ravenscar profile that are not already enforced at compile time (for example maximum queue length and the ceiling priority protocol), in addition the toolset will prevent data races. For more information consult chapter 9 of the SPARK Reference Manual which fully defines the formal verification activities performed in SPARK by GNATprove.

  • SPARK Pro
    Oct 9th, 2015

    Z3 prover comes with SPARK tools
    The SPARK toolset now supports the SMT prover Z3. The prover comes installed with the SPARK tools and can be selected using the --prover option just like the already present provers CVC4 and Alt-Ergo. Having this extra prover results in more proved checks and assertions when using the SPARK tools.

  • SPARK Pro
    Oct 7th, 2015

    Simple proof panel based on user profile
    Menus 'Prove ...' in GPS now open a simple panel or a more complex one depending on the user profile. The user profile for SPARK is a preference that the user can set to 'Basic' (the default) or 'Advanced'. The panel displayed for the basic user profile includes only a few switches, among which the recent --level switch. The panel displayed for the advanced user profile corresponds to the former panel with more detailed switches.

  • SPARK Pro
    Oct 5th, 2015

    Documentation of SPARK pragmas
    The GNAT Reference Manual now contains syntax information for all pragmas that emulate SPARK aspects.

  • SPARK Pro
    Sep 25th, 2015

    Examples from SPARK Book included in distribution
    The SPARK distribution now packages the examples presented in the SPARK Book by McCormick and Chapin ("Building High Integrity Applications with SPARK"), in example directories called spark_book and thumper. A short description of both has been added to SPARK User's Guide.

  • SPARK Pro
    Sep 23rd, 2015

    New switch—level to adjust proof power
    A new switch --level allows to set together the group of switches that control proof power, so that --level=0 corresponds to the fastest mode, and --level=4 corresponds to the most precise mode. The new default of switch --prover is now cvc4 instead of cvc4,altergo.

  • SPARK Pro
    Aug 5th, 2015

    Detection of some corrupted ALI files
    The SPARK toolset now detects some cases of corrupted ALI files and informs users about how to fix them.

  • SPARK Pro
    Jul 30th, 2015

    Generated Initializes contracts
    The tools now internally generate Initializes contracts for packages that do not have user-provided Initializes contracts. This reduces the false alarm rate about uninitialized uses of variables.

  • SPARK Pro
    Jul 29th, 2015

    Support for all kinds of type predicates
    The SPARK tool now handles all kinds of type predicates, in particular static predicates on floating-point types and dynamic predicates on any type. A dynamic predicate check is generated at every program point where the predicate associated to a value might be violated.

  • SPARK Pro
    Jul 24th, 2015

    Avoid unprovable LSP checks on untagged private
    Visible primitive operations of untagged private types whose full view is tagged previously lead to unprovable checks related to the verification of Liskov Substitution Principle, as Pre'Class cannot be specified on such operations. Dispatching on such subprograms is now forbidden in SPARK and LSP checks not needed anymore on such subprograms as a result.

  • SPARK Pro
    Jul 24th, 2015

    Better support for quantification with Iterable
    The SPARK proof tool now handles quantification using the Iterable aspect better, especially when cursors are record or private subtypes.

  • SPARK Pro
    Jul 23rd, 2015

    Summary table for proved and unproved checks
    The gnatprove output file "gnatprove.out" now contains a summary table which summarizes the verification results. It shows the number of proved checks, to which category they belong (like initialization checking, runtime errors, or functional contracts) and how various provers contributed to it. Unproved checks are also counted.

  • SPARK Pro
    Jul 13th, 2015

    Membership tests in tagged type hierarchy
    The GNATprove tool now supports testing for membership of an expression in a tagged type hierarchy.

  • SPARK Pro
    Jul 9th, 2015

    Better support for if expressions on real types
    The SPARK proof tool now handles if expressions better, which results in more automatic proofs on programs using if expressions, especially when they have a floating point type.

  • SPARK Pro
    Jun 26th, 2015

    Constant can now appear in contracts
    The SPARK toolset now allows for constants with variable input to appear in flow-related contracts. This allows for more precise information flow analysis.

  • SPARK Pro
    Jun 25th, 2015

    Support for volatile functions
    The SPARK toolset now correctly implements the semantics of the Boolean aspect volatile_function in both flow analysis and proof.

  • SPARK Pro
    Jun 24th, 2015

    Detect violations of language restrictions
    The SPARK toolset now checks settings of the pragma Restrictions before analyzing the code; previously they were only checked by the compiler.

  • SPARK Pro
    Jun 19th, 2015

    Better progress bar in graphical interface
    SPARK now provides better progress information when the --ide-progress-bar switch is used, so that the progress bar in graphical interfaces can convey this information to the user.

   1  2  3     Next »