- Ada 2012
- Ada 2005 / 95 / 83
- Embedded Development
- Formal Methods
- Open Source
- Safety-Critical Development
- Static Analysis
Jun 30th, 2011
We still have places left for the upcoming webinar introducing SPARK 10 next Tuesday (July 5). 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 Pro 10 is a major release including many new features – automatic selection of flow analysis mode, language profile for SCADE KCG, support for explicitly derived numeric types, addition of the SPARKBridge preview for Windows, library additions, and improvements to the SPARK proof tools.
To register, please visit:
AI-0142 Explicitly aliased parameters
Formal parameters of funtions and procedures can be marked as aliased. This forces by-reference passing of the parameter, requiring an aliased view for the actual. The parameter can then be referenced using 'Access.
AI-0191 Aliasing predicates
This AI introduces two new attributes: Same_Storage and Overlaps_Storage, whose purpose is to determine whether two objects of arbitrary types share some or all of their storage.
AI-0159 Queue containers
This AI specifies new units in the Ada standard library for queue containers.
Warning when—create-map-file is not supported
When option --create-map-file is not supported (that is attribute Linker'Map_File_Option is not declared in the configuration project file), gprbuild issues a warning if this option is used.
AI-167 Managing affinities on multiprocessors
Facilities are provided to allow a multiprocessor platform to be partitioned into a number of non-overlapping dispatching domains (DDs). Every task is scheduled within a DD. A task may also be assigned to execute on just one CPU from within its DD.
Jun 15th, 2011
Simplifier reports time stamps in verbose mode
When the -verbose switch is active and the -plain switch is not active, the Simplifier now reports the time-of-day, expressed in hours, minutes and seconds, before each on-screen message. This may be useful in assessing the Simplifier's performance in processing particular VCs.
Jun 10th, 2011
Support user-defined mutual exclusion procedures
An Annotate pragma may be used to indicate that a pair of procedures are to be considered as Lock/Unlock procedures for purposes of CodePeer's race condition analysis. This improves CodePeer's race condition analysis in cases like
Locking_Ops.Acquire; Global_Variable := Global_Variable + 1; Locking_Ops.Release;where Global_Variable is being accessed outside of any protected action.
Jun 8th, 2011
Conditional/Case/Quantified expression parens
The compiler now properly implements the latest version of the Ada 2012 rules regarding parenthesization of conditional/case/quantified expressions. Parens can now be omitted only if the construct is parenthesized, and in particular, this means that in the case of subprogram arguments, the parens can be omitted only if there is a single argument.
Jun 7th, 2011
SPARK Pro Demo - An Introduction to SPARK Pro - Part 4
The fourth in a series of 5 SPARK Pro demos that will present a practical, hands-on introduction on using the most important features of the SPARK programming language. This demo covers secure flows of information. We'll present a new demo in the series every Monday.
AI-0149 Access type conversion and membership
Values of anonymous access types are now allowed in contexts where the expected type is a named general access type and the implicit conversion has to be safe (access parameters and stand-alone anonymous access objects are not allowed, because their accessibility level is not statically known in Ada 2012). Additionally, the expression of a membership test is now allowed to be of an anonymous access type.
AI-0148 Anonymous access stand-alone objects
In Ada2012, a stand-alone object of an anonymous access type "remembers" the accessibility level of a value which is assigned to it. The dynamic accessibility level of the anonymous access type is equal to its "remembered" level.