GPS: improve batch codefix support
GPS now provides the ability to automatically fix similar errors in batch mode when multiple choices are available.

Function calls in proof contexts
It was always possible to call functions in SPARK proof contexts, however now their return annotation (if any) will appear in the hypothesis. For a function f(x) with precondition P and postcondition Q the instantiation that will appear in the hypothesis is: ((P and in_type(x)) -> Q) and in_type(f(x)). Proof functions can now be annotated with preconditions and return annotations (and they can also be refined). These annotations will also appear in the hypotheses if such a proof function is called in proof contexts (including pre- and post-conditions). This has two benefits: structured proof is much easier to achieve and the number of user rules to write will decrease significantly.

Implementation of interfacing aspects
The aspects Convention, Import, Export, Link_Name and External_Name are now properly implemented, as an Ada 2012 alternative for the Convention, Import, and Export pragmas (which continue to be available).

Package Ada.Streams.Stream_IO is preelaborated
As specified in AI05-0283, package Ada.Streams.Stream_IO is now declared with a pragma Preelaborate. This allows the declarations of Remote_Types and Remote_Call_Interface packages to depend on it, for support of such features as logging and persistence.

GPS: automatic mode for “strip blanks” preference
A new mode "Autodetect" has been added to the "strip blanks" preference. In this mode, if a file is open and contains zero trailing blanks, GPS will automatically strip trailing blanks when saving that file. Otherwise, trailing blanks will be preserved.

GPS: strip trailing blank lines
A new preference is provided in GPS to strip or keep trailing blank lines at end of file when saving editors.

More precise analysis of standard arithmetic
CodePeer now analyzes more precisely code involving standard arithmetic functions, such as Sin and Cos, by taking into account the postconditions of these functions giving bounds and results for special values.

New proof statement for system assumptions
A new proof statement (assume) has been added to introduce assumptions about a system. In essence, this can be used to introduce any fact into the proof system and is intended as a replacement for certain prv files. An example assumption could be "we reboot this system every 10 years, hence the uptime counter cannot overflow".

Add postconditions to standard numeric functions
The Ada RM requires numeric functions to return values in specific ranges, and specific values for some specified argument values. Many of these are now translated as Ada 2012 Post aspects on numeric functions, so that they can used by analysis tools, such as codepeer.

Further relaxation of static limits
The symbol table has been made dynamic and the limit of 1 million source lines per file has also been relaxed - it is now 2.1 billion lines which should be enough for most...

GNAAMP emits exception instructions for small lib
On the AAMP target, when using the small library configuration, raises of Program_Error and Constraint_Error are compiled into EXCEPT1 and EXCEPT2 instructions rather than run-time calls, reducing code size.

GB: Improved search results interaction
In search results, when a non-nested entry is selected, the IDE opens an editor on the first enclosed match, rather than on the enclosing construct itself. For example, let's say the search finds one more more references to an entity within a subprogram. Only one entry, the subprogram name, will appear in the results, rather than every enclosed match being given an entry. Selecting that subprogram entry will open the editor at the first enclosed reference, rather than at the subprogram name.

Code size reduction for controlled operations
The output of informative messages for the case of raising Program_Error in Finalize and Adjust due to earlier exceptions is now enabled only when the switch -gnateE is used. As a consequence, code size is reduced for programs using controlled types.

GPS: inherit ALI parser for custom language
GPS may now be configured to use its ALI parser to read cross referencing information for custom languages.

Support for VxWorks Linux
gprbuild now support VxWorks Linux targets.

Support for VxWorks Linux
gprbuild now support VxWorks Linux targets.

GPS: wildcard support in Open From Project
Interpretation of wildcard characters is now available in the "Open From Project..." dialog.

gnatcoll_db2ada can now generate Create_Database
This function (that is generated with the -adacreate switch) provides the necessary code to recreate the database from your application, with no need for the external files that define the schema and initial data of the database.

GNATCOLL.Readline: new package
This package provides an interface to the readline library, providing advanced interactive input.

GNAT.Command_Line: default value for string switch
The function Define_Switch that automatically assigns the value of the parameter to a variable will now preserve the default value set in that variable, instead of systematically reseting to the empty string. This makes it easier to specify default values.

GNAT.Command_Line: specify argument names
It is now possible to specify the name of the argument, as displayed in the automatic help message, when registering switches in Define_Switch. This helps make the help message more readable.

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 Connection 2011 - Real-Time Management & Production Systems for Manufacturing and Energy Facilit

Here's this Monday's installment from the Ada Connection 2011 talks. Jozef Cvirik from Ipesoft gives a talk on Real-Time Management & Production Systems for Manufacturing and Energy Facilities

A new film added every Monday. To view all the films we've added to date, please visit the Ada Lecture Series.

Extending functionality of cil2ada
The cil2ada interfacing tool now support assemblies of .NET 4.0

Minutes and Seconds predefined in RavenSPARK2005
In RavenSPARK2005 mode, the functions Seconds and Minutes are now predefined in the package Ada.Real_Time with specifications as in the Ada 2005 LRM D.8. These functions are only predefined when both the Examiner switches -profile=ravenscar and -language=2005 are given.

CodePeer now takes pragma Unreferenced into account
In the case of an assignment to a variable which is subject to an Unreferenced pragma (which indicates that the variable will never be read), CodePeer no longer generates a useless "unused assignment" warning.

Improved detection of unreachable code
Pragmas are now ignored when checking for unreachable code. This causes additional cases of unreachable code to generate warnings (or errors in SPARK mode). This also fixes the anomaly that attempting to suppress an unreachable code warning could generate a spurious warning.

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.

New GNAT pragma and aspect Contract_Case
A new aspect Contract_Case is defined, using the Ada 2012 aspect syntax, that allows defining fine-grain specifications that can complement or replace the contract given by a precondition and a postcondition. This is also usable by testing and formal verification tools. It applies only to subprogram declarations in a package declaration inside a package spec unit. Note that the syntax of Contract_Case is similar to that of Test_Case. A corresponding pragma Contract_Case is defined, which can be used in all Ada modes.

Ada 2012 attributes First_Valid/Last_Valid
The new Ada 2012 attributes First_Valid and Last_Valid are implemented. These apply to static discrete types with at least one valid value. The static discrete type may have a static predicate (which is the case where these attributes are useful). They return the lowest and highest values for which valid values (that is values that satisfy any static predicate) exist.

SPARK 10.1 webinar recording now online

The InSight webinar series continued with a presentation on the new features of SPARK Pro 10.1:

• Generics Phase 1 – Release 10.1 includes the first phase of the addition of support for Ada generics to the SPARK language and toolset
• Dynamic Flow Analyser and VCG Heaps
• Unicode characters now allowed in strings
• Improved use of types and subtypes in FDL
• Improvements to Simplifier tactics and performance
• Auto-generation of refinement rules
• Improvements to SPARKBridge
• New SPARKClean utility

This webinar can be viewed at:
http://www.adacore.com/home/products/sparkpro/language_toolsuite/webinars/

AWS now supports IPv6
AWS now supports IPv6, to enable IPv6 support:

   $ make IPv6=true setup

AWS now supports IPv6
AWS now supports IPv6, to enable IPv6 support:

   $ make IPv6=true setup

Improved indentation in parenthesized expressions
Automatic indentation of 'or else' and 'and then' constructs at the end of lines inside parenthesized expressions has been improved. In particular, they no longer generate an extra indentation on the next line.

Improved indentation of comments within expressions
Indentation of comments within expressions or as part of continuation lines will take the extra continuation line preference into account.

Increase efficiency of bounded strings
Bounded strings have been optimized by avoiding the need to NUL-out unused characters.

Improved support for task names under GNU/Linux
Under GNU/Linux systems, task names (either implicit from the source code, or explicit via pragma Task_Name) are now set via the prctl() system call, so that they also appear as part of e.g. the ps command.

Improved linker DLL build time
When building a shared library with many exported symbols on Windows the creation of the DLL was taking a long time. This performance issue has been addressed and now creating a DLL takes about the same time as creating an executable.

GPS: improvements in auto_highlight_occurrences.py
There are two new features in the auto_highlight_occurrences.py plugin:

  - if there is a selection, other occurrences of the selected text
    will be highlighted in the editor
  - if the cursor is on a word which is not a navigable entity (for instance
    keywords, words in comments, or in languages other than Ada or C), GPS
    will perform text-based highlighting of this word

Both of these behaviors can be deactivated through the Preferences dialog, under Plugins->auto_highlight_occurrences.

Misleading warning that variable could be constant
If the actual in a call is an access selected component of a variable, it is treated as a possible modification of the enclosing record, to prevent a spurious warning that a variable might be declared as a constant.

GPS: new command GPS.EditorLocation.inside_word
A new GPS shell/Python command is available to determine whether a location is inside a word. This is useful when creating editor plugins.

Better message for Range in integer type definition
Surprisingly, a range attribute definition is not permitted to be used as a signed integer type definition. A clearer message is now given for this case, advising that instead x'First .. x'Last must be used.

Add support for limiting HTTP POST parameters
It is now possible to limit the maximum number of POST parameters that AWS will handle. This is a per server configuration option whose default value is set to 100.

Add support for limiting HTTP POST parameters
It is now possible to limit the maximum number of POST parameters that AWS will handle. This is a per server configuration option whose default value is set to 100.

Speed up gnatmake in presence of extending projects
The check in gnatmake to verify if an object file is in the correct object directory in the presence of extending projects has been optimized, as it was taking a considerable amount of time when there were many sources.

Introducing CodePeer 2.1

April 10, 2012 – 4:00pm GMT, 5:00pm CET, 11:00am EST

CodePeer is a source code analyzer that detects run-time and logic errors in Ada programs. This webinar, presented by Tucker Taft, will provide an overview of the technology, and focus on the new features introduced in this latest 2.1 release. These include support for Ada 2012 and its new syntax for specifying contracts, analysis of the elaboration of library units to enable detection of uninitialized global variables, better support for analysis of race conditions including new GPS reports, and more precise handling of preconditions and unused assignments. Presented by Tucker Taft, we will also allow for a Q&A session at the end of the presentation.

To register, please visit:
http://www.adacore.com/home/products/codepeer/toolset/webinars/

Unit testing with GNATtest webinar

March 20, 2012 – 4:00pm GMT, 5:00pm CET, 12:00am EST

The InSight webinar series continues with a webinar demonstrating how to write unit tests in a cost-effective way using the AdaCore toolset. More precisely it will show how to generate the unit testing framework using GNATtest, how to run the tests on an emulator such as GNATemulator, and how to extract coverage results using GNATcoverage. This is primary aimed at developers and projects managers that already have unit testing infrastructure in place and are looking to reduce maintenance costs, as well as teams that are looking at implementing such techniques with minimal effort.

To register please visit:
http://www.adacore.com/home/products/gnatpro/webinars/

GPS: Coverage Report accessible through Back button
When clicking on a file or subprogram in the Code Coverage report, GPS opens this location in an editor. It is now possible to click the "Back" button in the toolbar to go back to the Code Coverage report.

Process ids in traces
Process IDs can now optionally be included in trace messages logged to standard error. This feature is enabled by setting "pid=true" in section [log] of the PolyORB configuration.

Unmoded globals permitted with flow=auto
Previously, the Examiner enforced the rule that global annotations on procedures must always specify variable modes when in automatic flow analysis mode. This rule has now been relaxed, so modes may be omitted from globals if there is a derives annotation present. The Examiner will then infer the modes from the derives annotation as it does in information-flow mode. This means that legacy code with derives annotations and unmoded globals can be analysed with flow=auto.

GPS: multi-line option in MDI.input_dialog
The GPS function MDI.input_dialog used in plug-ins has been enhanced to offer multi-line input on fields as an option.

Process ids in traces
Process IDs can now optionally be included in trace messages logged to standard error. This feature is enabled by setting "pid=true" in section [log] of the PolyORB configuration.

Automatic flow analysis mode is the default
The default flow analysis mode is now automatic, which replaces the previous default of information flow. Automatic flow analysis was introduced in release 10. In this mode the Examiner selects information flow or data flow analysis on a per-subprogram basis depending on the presence or absence of derives annotations. This change is backwards compatible for current projects using information flow, data flow or a combination of the two. However, if you wish to enforce information flow or data flow for all analysis this can still be done explicitly via the option -flow=information or -flow=data.

Miscellaneous updates to Victor
We have fixed a number of small issues with victor wrapper: timing information is now correctly stored in the .vct files; temporary files are now correctly deleted; temporary files can be placed in the current working directory and not deleted using the new -keep flag; and finally, experimental support for CVC4 has been added.

Debugger condition support in exception catchpoints
The debugger has been enhanced to support the use of conditions attached to exception catchpoints.

Avoid obsolescent feature messages for instances
When restriction No_Obsolescent_Features is used, the use of an obsolescent feature in a generic template results in a diagnostic only when compiling the template, and not when compiling instantiations of the generic.

SPARK 10.1 webinar

February 21, 2012 - 4:00pm GMT, 5:00pm CET, 11:00am EST

The InSight webinar series continues with a presentation on the new features of the AdaCore/Altran Praxis joint offering – SPARK Pro 10.1. SPARK Pro combines the proven SPARK Ada language and supporting toolset with AdaCore’s GNAT Programming Studio (GPS) integrated development environment, backed by unrivalled support systems.

SPARK 10.1 includes the following enhancements:

• Generics Phase 1 – Release 10.1 includes the first phase of the addition of support for Ada generics to the SPARK language and toolset
• Dynamic Flow Analyser and VCG Heaps
• Unicode characters now allowed in strings
• Improved use of types and subtypes in FDL
• Improvements to Simplifier tactics and performance
• Auto-generation of refinement rules
• Improvements to SPARKBridge
• New SPARKClean utility

This webinar will include a demo and Q&A session with the developers of the SPARK Pro toolset.

 

To register for this webinar please visit:
www.adacore.com/home/products/sparkpro/language_toolsuite/webinars/

Security Advisory SA-2012-L119-003: Hash collisions in AWS

Problem:

Impacted versions of AWS store key/value pairs from submitted form data in hash tables using a hash function that has predictable collisions. As a result, a single specially crafted HTTP request can cause the server to use hours of CPU time, thus causing a denial of service.

Impact:

All AWS releases and wavefronts prior to 2012-01-21

Status:

This was fixed in AWS 2.11 and 2.10.2 on 2012-01-21

References:

• n.runs-SA-2011.004
• Effective Denial of Service attacks against web application platforms :: AWS round
• AWS: AdaCore site, OpenDO Forge

Improved error messages for violation of 12.3(18)
If an instantiation is illegal because a private primitive operation in the generic fails to override a visible operation in the same generic, the compiler now reports the names of the relevant type and operation.

Verbosity when linking shared SALs
In default mode (not verbose and not quiet), the base name of gnatbind and of the compiler when binding and compiling the binder generated file is now output, instead of the full path names. Also, when the command line is long, only the beginning is output.

Alt-Ergo 0.94 and more fine-grained steps
Upgraded SPARKBridge's default SMT solver, Alt-Ergo, to version 0.94. Additionally this version includes more fine-grained proof steps for better predictability, which is helpful in regression testing.

Verbosity when linking shared SALs
In default mode (not verbose and not quiet), the base name of gnatbind and of the compiler when binding and compiling the binder generated file is now output, instead of the full path names. Also, when the command line is long, only the beginning is output.

ECL: Removal policy when fixing code
The preference "Removal policy when fixing code" has been added to the Ada "General" preference page. It defines the way code should be altered when sections of code are to be removed. - "Always_Remove" means that the code will be removed by GNATbench. - "Always_Comment" means that the code will always be commented out. - "Propose_Both_Choices" will propose a menu with both choices.

GPS: goto next/previous bookmark
Two new actions ("Goto Next Bookmark" and "Goto Previous Bookmark") are now available to jump to the nearest next or previous bookmark in the current file. These actions can be bound to keys in the "General" section of the Key Shortcuts dialog.

Documentation converted to sphinx
The documentation format was changed, so that we can produce nicer looking output. In particular, the new format provides an integrated search feature over all pages of the manual.

Simple storage pools
The GNAT-specific pragma Simple_Storage_Pool_Type (or aspect) can be applied to library-level limited types to designate the types as simple storage pool types. Access types can be associated with a simple pool object via the new Simple_Storage_Pool attribute (or aspect), so that allocators will invoke the Allocate procedure of the simple storage pool. This is an alternative to Ada's standard storage pools that does not require tagged types or finalization support, which may be useful in some contexts (for example, certification contexts where tagged types and finalization are forbidden).

Better warnings for suspicious mod values
Two more cases of suspicious mod values (for example in "type X is mod 2*8", and "R := X mod 2 * 32"), where in each case the * should almost certainly be **, now generate warnings under control of -gnatw.m (on by default).