Development Log in March 2012.

  • GNAT Pro|GPRbuild
    Mar 30th, 2012

    New package Clean in project file
    A new package Clean is added in project files. It can contain declarations of attributes Source_Artifact_Extensions and Object_Artifact_Extensions, that specify the extensions of files whose names are derived from source or object file names, that reside in the object directory and that are to be cleaned by gprclean.

  • GNAT Pro | GPS | GNATbench
    Mar 30th, 2012

    GPS: Improved Emacs selection mode support
    When in Emacs mode, after setting a mark, the commands to go to the beginning and end of line will extend the selection.

  • GNAT Pro | GPRbuild
    Mar 30th, 2012

    New package Clean in project file
    A new package Clean is added in project files. It can contain declarations of attributes Source_Artifact_Extensions and Object_Artifact_Extensions, that specify the extensions of files whose names are derived from source or object file names, that reside in the object directory and that are to be cleaned by gprclean.

  • GNAT Pro | GPS | GNATbench
    Mar 29th, 2012

    GPS: isearch.py stores result of ctrl-w in history
    When you start a search (ctrl-s) and then use ctrl-w to copy parts of the current identifier as the search pattern, this pattern is now stored immediately in the history. That way, cancelling the search and restarting it with ctrl-s ctrl-s will search what was copied. (We used to update the pattern only after you pressed ctrl-s a second time after ctrl-w.) This is closer to Emacs' behavior.

  • GNAT Pro
    Mar 29th, 2012

    Enhanced heap support in GNAAMP libraries
    A more flexible version of the low-level support for heap allocations (package Heap_Simple) is integrated in the GNAAMP run-time libraries, allowing selection of different pool sizes by changing the template.lec file to include the appropriate heap_pool_*.obj. Heap support can be included or excluded based on object include directives and the setting of the symbol _HEAP_INIT in template.lec.

  • GNAT Pro
    Mar 29th, 2012

    Exception-handling support in AAMP small library
    The GNAAMP small run-time library (aamp*-small) now includes support for basic exception handling, based on a reduced version of the Ada.Exceptions package.

  • GNAT Pro | GPS | GNATbench
    Mar 27th, 2012

    GPS: UI: add custom radio menu items
    The GPS.Menu API has been enhanced to allow the creation of radio menu items and get/set their activity status.

  • GNATCOLL.SQL quotes table and field names
    When a table or field name is also a SQL keyword (or has a special meaning for one of the DBMS) it is now quoted. This gives more flexibility in what names can be used for the database model.

  • GNATCOLL.SQL.Sqlite binding for online backup API
    GNATCOLL now provides a binding to sqlite's online backup API, allowing to manipulate a database in memory and then dumping to the disk (or the opposite), which can greatly speed up operations.

  • GNATCOLL.SQL.Exec.Insert_And_Get_PK
    This new function provides an efficient way to insert a new row in a table and immediately retrieve its primary key (for instance when the key was computed from a sequence). This can be more efficient than using the function Last_Id.

  • GNATCOLL.SQL adds support for Money type
    It is now possible to use a type of "Money" for fields, which will be automatically converted to the appropriate DBMS type.

  • GNAT Pro | GPS | GNATbench
    Mar 20th, 2012

    GPS: simplify Default Builder preference
    The Default Builder preference has been simplified, with the following changes to the settings:

      - 'Gprmake' has been removed, since gprmake is no longer supported
      - 'Gprbuild' has been renamed 'Auto', which is a more accurate description
      - 'Gprbuild_Always' has been renamed 'Gprbuild', for consistency with the
        'Gnatmake' setting.
    
    
    Note that if you were using a non-default setting for this preference, you will need to reset it manually.

  • GNAT Pro
    Mar 20th, 2012

    Improved display of gnatcheck messages in GPS
    When gnatcheck is called interactively from GPS, the generated messages are displayed as warnings, and each message starts with a "check: " prefix.

  • GNATCOLL.Traces adds support for trace hierarchies
    It is now possible to use "*." or ".*" in the configuration file to change the settings for multiple trace handles.

  • Modeling
    Mar 18th, 2012

    Compilation of Heterogeneous Models: Motivations and Challenges

    The widespread use of model driven engineering in the development of software-intensive systems, including high- integrity embedded systems, gave rise to a “Tower of Babel” of modeling languages. System architects may use languages such as OMG SysML and MARTE, SAE AADL or EAST-ADL; control and command engineers tend to use graphical tools such as MathWorks Simulink/Stateflow or Esterel Technologies SCADE, or textual languages such as MathWorks Embedded Matlab; software engineers usually rely on OMG UML; and, of course, many in- house domain specific languages are equally used at any step of the development process. This heterogeneity of modeling formalisms raises several questions on the verification and code generation for systems described using heterogeneous models: How can we ensure consistency across multiple modeling views? How can we generate code, which is optimized with respect to multiple modeling views? How can we ensure model-level verification is consistent with the run-time behavior of the generated executable application?

    In this position paper we describe the motivations and challenges of analysis and code generation from heterogeneous models when intra-view consistency, optimization and safety are major concerns. We will then introduce Project P and Hi-MoCo - respectively FUI and Eurostars -funded collaborative projects tackling the challenges above. This work continues and extends, in a wider context, the work carried out by the Gene-Auto project. Hereby we will present the key elements of Project P and Hi-MoCo, in particular: (i) the philosophy for the identification of safe and minimal practical subsets of input modeling languages; (ii) the overall architecture of the toolsets, the supported analysis techniques and the target languages for code generation; and finally, (iii) the approach to cross-domain qualification for an open-source, community-driven toolset.

  • Formal Methods
    Mar 18th, 2012

    Integrating Formal Program Verification with Testing

    Access the paper here.

    Verification activities mandated for critical software are essential to achieve the required level of confidence expected in life-critical or business-critical software. They are becoming increasingly costly as, over time, they require the development and maintenance of a large body of functional and robustness tests on larger and more complex applications. Formal program verification offers a way to reduce these costs while providing stronger guarantees than testing. Addressing verification activities with formal verification is supported by upcoming standards such as do-178c for software development in avionics. In the Hi-Lite project, we pursue the integration of formal verification with testing for projects developed in C or Ada. In this paper, we discuss the conditions under which this integration is at least as strong as testing alone. We describe associated costs and benefits, using a simple banking database application as a case study.

     

     

  • GNATcoverage
    Mar 18th, 2012

    Formalization and Comparison of MCDC and Object Branch Coverage Criteria

    This paper presents formal results derived from the COUVERTURE project, whose goal was to develop tools to support structural coverage analysis of unin- strumented safety-critical software. After briefly introducing the project context and explaining the need for formal foundations, we focus on the relationships between machine branch coverage and the DO-178B Modified Condition/Decision Coverage (MCDC) criterion. A thorough understanding of those relationships is important, since it provides the foundation for knowing where efficient execution trace techniques can be used to demonstrate compliance with the MCDC criterion. We first present several conjectures that were tested using Alloy models, then provide a formally verified characterization of the situations when coverage of object control-flow edges implies MCDC compliance.


  • Mar 18th, 2012

    Compilation of Heterogeneous Models: Motivations and Challenges

    The widespread use of model driven engineering in the development of software-intensive systems, including high- integrity embedded systems, gave rise to a “Tower of Babel” of modeling languages. System architects may use languages such as OMG SysML and MARTE, SAE AADL or EAST-ADL; control and command engineers tend to use graphical tools such as MathWorks Simulink/Stateflow or Esterel Technologies SCADE, or textual languages such as MathWorks Embedded Matlab; software engineers usually rely on OMG UML; and, of course, many in- house domain specific languages are equally used at any step of the development process. This heterogeneity of modeling formalisms raises several questions on the verification and code generation for systems described using heterogeneous models: How can we ensure consistency across multiple modeling views? How can we generate code, which is optimized with respect to multiple modeling views? How can we ensure model-level verification is consistent with the run-time behavior of the generated executable application?

  • SPARK Pro
    Mar 15th, 2012

    Fully qualified names in proof files
    The Examiner now emits fully qualified subprogram names in the headers of .vcg, .rls and .fdl files. Previously the headers would state only the package name and the subprogram name, eg "function Grandchild.Negate" but now the complete hierarchy is included, eg "function Parent.Child.Grandchild.Negate". This removes any ambiguity in cases where there are duplicate names in different parts of a package hierarchy. Note that if you are configuring proof output files for regression analysis this change will result in a large one-off difference to the proof files.

  • CodePeer
    Mar 15th, 2012

    Improved race condtion analysis for singleton tasks
    In some cases, CodePeer is able to perform more precise race condition analysis if it is known that exactly one object of some given task type is declared. Previously, this was known only in the case of an anonymous task type. CodePeer is now able to detect this situation in some common scenarios involving named task types.

  • GNAT Pro | GPS | GNATbench
    Mar 14th, 2012

    GPS: PowerPC E500v2 Wind River Linux support
    GPS support for the e500v2-wrs-linux GNAT Pro toolchain has been added.

  • SPARK Pro
    Mar 12th, 2012

    B-Method – AdaCore micro-seminar

    AdaCore Internal Seminar - June 25, 2012

    Jean Louis Dufour (Sagem DS, http://fr.linkedin.com/pub/jean-louis-dufour/18/7b7/228), will come to the AdaCore Paris offices to give a 101 introduction to the B-Method.

    AdaCore, from time to time, organizes seminars in the Paris offices. If you are interested in a particular talk, please send email to events@adacore.com.

  • GNAT Pro
    Mar 10th, 2012

    Better error message for bad preprocessor directive
    If a preprocessor directive such as #if is detected when preprocessing has not been activated, a clear error message is now given, instead of just flagging the # as an illegal character.

  • GNAT Pro
    Mar 10th, 2012

    Improve error message for a**b**c
    Ada does not permit writing a**b**c. Parenthesization is required to make the intended association clear. Writing this without parentheses now outputs an explicit message saying that ** requires parenthesization.

  • GNAT Pro | GPS | GNATbench
    Mar 9th, 2012

    GB: project names need not be legal Ada identifiers
    The name of an Eclipse/Workbench project need not conform to the rules for Ada identifiers. This change applies to both new projects as well as existing Eclipse/Workbench projects to be converted to GNATbench use.

  • GNAT Pro
    Mar 8th, 2012

    Improve warnings from -gnatw.t
    When a postcondition is explicitly True or False, it is reasonable to assume that this is exactly what is intended, and it is now the case that warnings for such postconditions are suppressed.

  • Ada
    Mar 7th, 2012

    Ada and Ada2012 – Overview and Rationale

    Ada 2012
    View more PowerPoint from AdaCore

    By Quentin Ochem
    Technical Account Manager

  • Ada
    Mar 6th, 2012

    Ada 2012 Rationale - Chapter 1 - Contracts and Aspects

    Read the latest installment of the Ada 2012 Rational by John Barnes:
    Download Chapter 1 - Contracts and Aspects

  • Ada Web Server
    Mar 5th, 2012

    Add support for session cookies
    A session cookie is one without a Max-Age attribute. Such cookies expire when the web browser is closed.

  • Ada Web Server
    Mar 5th, 2012

    Add support for session cookies
    A session cookie is one without a Max-Age attribute. Such cookies expire when the web browser is closed.

  • GNAT Pro
    Mar 5th, 2012

    Switch to control maximum number of instantiations
    A new switch -gnateinn (/MAX_INSTANTIATIONS=nn in VMS) is introduced which sets the maximum number of instantiations during compilation of a single unit to the value nn. This may be useful in increasing the default limit of 8000 in the rare cases where a single unit legitimately exceeds this limit.

  • CodePeer
    Mar 1st, 2012

    More precise analysis of array bounds
    CodePeer now understands that the bounds of a subprogram parameter of an unconstrained subtype satisfy the constraints of the index subtype if the bounds define a non-null range. Previously CodePeer conservatively assumed that out-of-subtype array bounds were possible in more cases.

  • CodePeer
    Mar 1st, 2012

    More precise analysis of concatenation bounds
    CodePeer now correctly issues no warning when the result of concatenating two arrays is passed as an actual parameter and the subtype of the corresponding formal parameter is unconstrained. CodePeer assumes that the low bound of such a formal parameter satisfies the constraints of the index subtype even if the bounds define a null range.

  • GNAT Pro
    Mar 1st, 2012

    Extension of warning -gnatw.t to Contract_Case
    The warning option -gnatw.t already issued warnings on suspicious postconditions. This extends it to contract cases, which is a GNAT pragma and aspect allowing expression of fine-grain contracts.