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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

 

 

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.

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?

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.

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.

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

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.

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.

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.

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.

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 and Ada2012 – Overview and Rationale

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

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

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

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.

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.

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.

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.