[Ada] Analysis of delayed SPARK aspects and use of SPARK_Mode

This patch clarifies the need of saving and restoring SPARK_Mode in a stack like fashion. No change in behavior, no test needed. Tested on x86_64-pc-linux-gnu, committed on trunk 2014-07-17 Hristian Kirtchev kirtc...@adacore.com * sem_ch6.adb (Analyze_Subprogram_Body_Contract,

[Ada] Implement new partition-wide restriction No_Long_Long_Integer

This new restriction No_Long_Long_Integer forbids any explicit reference to type Standard.Long_Long_Integer, and also forbids declaring range types whose implicit base type is Long_Long_Integer, and modular types whose size exceeds Long_Integer'Size. The following is compiled with -gnatl: 1.

[Ada] Renaming of intrinsic generic subprograms

This patch allows the renaming and subsequent instantiation of generic subprograms that are marked Intrinsic, such as the predefined units Unchecked_Conversion and Unchecked_Deallocation. The following must execute quietly: gnatmake -q -gnatws uncrename.adb uncrename --- with Mumble;

[Ada] Add annotate aspect, add entity argument to pragma Annotate

An optional final named argument [Entity = local_NAME] is allowed for pragma Annotate to indicate that the annotation is for a particular entity, and a corresponding Annotate aspect is introduced. Given the test program: 1. package AspectAnn is 2.Y : constant Integer := 43; 3.

[Ada] Crash while processing illegal state refinement

This patch modifies the parser to catch a case where the argument of SPARK aspect Refined_State is not properly parenthesized. -- Source -- -- no_parens.ads package No_Parens with SPARK_Mode = On, Abstract_State = State is pragma Elaborate_Body; end

[Ada] Crash on transient classwide limited view on RHS of short-circuit

This change fixes a compiler crash that would occur in some cases where an expression involving transient return values of a limited view of a class-wide interface type occur on the right hand side of a short circuit operator. The following compilation must be accepted quietly: $ gcc -c

[Ada] Missing finalization of a transient class-wide function result

This patch corrects the transient object machinery to treat the renamed result of a controlled function call as a finalizable transient when the context is an expression with actions. If this was a different context, the lifetime of the result would be considered extended and not finalized.

[Ada] Enfore SPARK RM rule 7.1.5(2)

This patch modifies the analysis of aspects Abstract_State, Initializes and Initial_Condition to ensure that they are inserted after pragma SPARK_Mode. The proper placement allows for SPARK_Mode to be analyzed first and dictate the mode of the related package. -- Source --

[Ada] Warning match string does not need leading/trailing asterisks

The warning message pattern given for pragma Warning_As_Error or for pragma Warnings no longer requires leading and trailing asterisks. The match can be anywhere in the string without these characters as shown in this example, compiled with -gnatwa -gnatld7 -gnatj55 Compiling: warnmatch.adb

[Ada] Catch newly illegal case of Unrestricted_Access

It is now illegal to use Unrestricted_Access to directly generate a thin pointer of an unconstrained array type which references a non- aliased object. This never worked, and we might as well catch it as illegal, since it is not hard to do so, as shown in the following example: 1. with

[Ada] Warning if record size is not a multiple of alignment

This implements a new warning (on by default, controlled by -gnatw.z/-gnatw.Z, included in -gnatwa), that warns if a record type has a specified size and alignment where the size is not a multiple of the alignment resulting in an object size greater than the specified size. The warning is

[Ada] A static predicate can be specified by a Case expression.

This patch completes the implementation of Ada 2012 static predicates, by adding support for case expressions that can be transformed into a statically evaluable expression on values of the subtype. Compiling: gcc -c -gnata test_predicate.adb must yield: test_predicate.adb:11:20:

[Ada] New node kind N_Compound_Statement

This change reorganizes expansion of object initialization statements, which need to be captured under a single node id. Previously these were represented as a (malformed) N_Expression_With_Actions with a NULL statement as its expression. This irregularity is fixed by instead introducing a

[Ada] PR ada/61505

A blind attempt (since I'm using makeinfo 4.8 where the error does not show up) at fixing the makeinfo errors on gnat_rm.texi Let me know if this fixes the errors. 2014-06-14 Arnaud Charlet char...@adacore.com PR ada/61505 * gnat_rm.texi: Attempt to fix error with makeinfo 5.1

Re: [Ada] PR ada/61505

2014-06-14 Bernd Edlinger bernd.edlin...@hotmail.de PR ada/61505 * gnat_rm.texi: Fix errors with makeinfo 5.1. This looks good, except that there's a last change needed (at least according to older versions of makeinfo), now detected: --- gnat_rm.texi(revision

[Ada] Allow pragma Restrictions (No_Dependence = unit) in system.ads

This patch enables the recognition/processing of pragma Restrictions (No_Dependence = unit) in system.ads, allowing more flexibility in configuring specialized versions of System. Given a system.ads that contains the line pragma Restrictions (No_Dependence = Ada.Text_IO); Compiling the

[Ada] Fix spurious warning on use before def in Refined_Post aspect

The Refined_Post aspect defined in SPARK 2014 should be considered like a postcondition wrt issuing warnings on variable references. Tested on x86_64-pc-linux-gnu, committed on trunk 2014-06-13 Yannick Moy m...@adacore.com * sem_warn.adb (Check_Unset_References): Take case of

[Ada] Fix spurious warning on imported/exported variables with aspect

Aspects Import and Export were not treated like the equivalent pragmas wrt issuing warnings on missing initialization before use. Now fixed. Tested on x86_64-pc-linux-gnu, committed on trunk 2014-06-13 Yannick Moy m...@adacore.com * sem_ch13.adb

[Ada] Non-static aggregates in Preelaborate units

This patch removes a spurious error on a unit to which the Preelaborate pragma applies. The error appeared on a unit that holds an instantiation of a package containing a type declaration with an array component whose default value is given by an actual in the instance, but the error may occur in

[Ada] Elaborate Secondary_Stack early

This patch fixes an obscure bug that causes the secondary stack to be used before it is initialized in certain cases. This can only happen if (1) the -gnatE switch is used to disable the static elaboration mode, (2) the -p switch is passed to gnatbind to tell it to choose a pessimistic

[Ada] Make Task_Info pragma and package obsolescent

The functionality is now provided in a target-independent manner Tested on x86_64-pc-linux-gnu, committed on trunk 2014-06-13 Geert Bosch bo...@adacore.com * gnat_rm.texi, s-tasinf-solaris.ads, sem_prag.adb, gnat_ugn.texi, s-tasinf-mingw.ads, s-tasinf.ads, s-tasinf-linux.ads,

[Ada] Improvements to handling of pragma Compiler_Unit_Warning

We now check for null statement sequences, and for extended return statements. In addition, the message generated now includes a description of the non-permitted construct as shown in this test program (compiled with -gnatj60 -gnatl) 1. pragma Ada_2012; 2. pragma Compiler_Unit_Warning;

[Ada] Assertion policy and postconditions

This patch fixes the handling of attribute reference 'Old in the presence of Assertion_Policy (Checked) pragma, when a unit is compiled without the -gnata flag. Compiling and executing the following: gnatmake -q assertion_policy_test.adb assertion_policy_test Must yield: +

[Ada] GNAT.Command_Line.Get_Argument does't expand correctly with custom parser

This patches fixes the use of custom parsers when trying to expand command line arguments like *.adb. When run from the test directory, the following program should output next source test_cmd_line1.adb. with Ada.Text_IO; use Ada.Text_IO; with GNAT.Command_Line; use

[Ada] Remove global variable Root_Environment from Project Manager

Global variable Root_Environment was used in the Project Manager, but was not initialized by GNATCOLL and GPS. This patch eliminates the direct use of Root_Environment. Tested on x86_64-pc-linux-gnu, committed on trunk 2014-06-13 Vincent Celier cel...@adacore.com * makeutl.ads

[Ada] Handle range check for float Pre/Succ attributes

In Float_Check_Overflow mode, Succ applied to type'Last or Pred applied to type'First generates a constraint error since the argument is out of range. This was not previously changed, the following test: 1. with Ada.Exceptions; use Ada.Exceptions; 2. with Text_IO; use Text_IO; 3.

[Ada] Avoid unnecessary warnings about address clause alignment

This patch detects cases where we can tell at compile time that an address clause value is compatible with the alignment of the object so that we do not need to issue a warning. The following is compiled with -gnatwa -gnatld7 -gnatj55 1. pragma Restrictions (No_Exception_Propagation);

[Ada] Cleanup handling of info and warning messages

This is a fairly major internal reorganization of how info and warning messages are handled. Info messages for elaboration are now tagged as [-gnatel] if warning tagging is activated (-gnatw.d), and info messages coming from instantiations are consistently labeled as such as shown by this example,

[Ada] gnat link and shared libraries

When gnat link is invoked and there are shared libraries, the link may be incorrect on some platforms, such as Windows. This is fixed by this patch. Tested on x86_64-pc-linux-gnu, committed on trunk 2014-06-11 Vincent Celier cel...@adacore.com * gnatcmd.adb (Process_Link): Do not

[Ada] Analyze contracts of subprogram body stubs

This patch ensures that contract of subprogram body stubs are analyzed in timely fashion. -- Source -- -- pack.ads package Pack with SPARK_Mode, Abstract_State = State, Initializes= (Var_1, State) is Var_1 : Integer := 0; procedure Double

[Ada] Error not detected in illegal selected component

This patch corrects an error in the resolution of selected components when the prefix is overloaded and none of the interpretations matches the context. Compiling resolve_func_deref_comp.adb must yield: resolve_func_deref_comp.adb:14:18: no interpretation matches type access to T defined

[Ada] Better handling of variant records with No_Implicit_Conditionals

Previously, an attempt to declare a variant record type was rejected if restriction No_Implicit_Conditionals was active, since the resulting generated equality and initialization routines contained implicit tests. Now such declarations are allowed, but these routines are not generated if the

[Ada] Consistent processing of preelaborated units across language versions

The processing of pragma Preelaborate_05 might cause inconsistent compiler behaviour when a given unit having the pragma appears in the dependencies of both an Ada 95 and and Ada 2005 unit in the same closure. This is addressed by making runtime units Preelaborate in all cases. Tested on

[Ada] Fix handling of pragma/aspect Independent[_Components]

This fixes several errors in the handling of the pragmas Independent and Independent_Components. The implementation now matches the RM definition 100%. The following compiles without errors: 1. package Independ is 2.type A1 is array (1 .. 10) of Integer; 3.pragma

Re: [PATCH] Add support for GNU/Hurd in gnat-4.9

BTW, I wonder ho the kfreebsd people managed to get accepted upstream? This is typically a good example of patches being accepted too rapidly, and leading to maintenance issues, see: https://gcc.gnu.org/bugzilla/show_bug.cgi?id=56274 for which nobody is stepping up to fix. So we might well

Re: [PATCH] Add support for GNU/Hurd in gnat-4.9

I think the majority of work has bee done, Now that patch will change slightly for every missing feature added to Hurd. Then it's all good, it's a matter of what I said above. Don't forget also the part where general changes are done in GNAT which require update to target specific files:

[Ada] Add usage line for gnatmake switch -d

A new line is added in the gnatmake usage for switch -d: -dDisplay compilation progress Tested on x86_64-pc-linux-gnu, committed on trunk 2014-05-21 Vincent Celier cel...@adacore.com * makeusg.adb: Add switch -d to usage. Index: makeusg.adb

[Ada] Handling of deferred references with nested prefixed calls

When handling deferred references, if an actual that is the prefix of an enclosing prefixed call has been rewritten, we must use Nkind and Sloc to identify the corresponding formal. The First_Named_Actual of the enclosing call may be meaningless after the surrounding expansion. No simple example

[Ada] Fix possible overflow in table handling

The Reallocate procedures in g-htable.adb and g-dyntab.adb are subject to problems with possible intermediate overflow. This has never been reported to cause problems, but in theory it could cause performance degradation, so it is now fixed. No test, because too much trouble to construct, and we

[Ada] Detect illegal component of dereference of access-to-constant

This patch detects an error that was previously undetected. In particular, it is illegal to rename a subcomponent of an object designated by an access-to-constant value if that subcomponent depends on discriminants. The following test should get an error: % gnatmake -f -q acc_const_test.adb

[Ada] Clearer documentation of -gnatw.g and -gnatyg switches

This patch provides more precise documentation of the GNAT mode warning switch -gnatw.g and the GNAT mode style switch -gnatyg, in both the users guide and the usage information. Documentation change only, no test needed. Tested on x86_64-pc-linux-gnu, committed on trunk 2014-05-21 Robert Dewar

[Ada] Tag restriction warning messages

Restriction warning messages are now tagged [restriction warning] if -gnatw.d is used, instead of [enabled by default]. This new tag can be used in pragma Warning_As_Errors. The following is compiled with -gnatw.d -gnatj50 -gnatl 1. pragma Warning_As_Error ([restriction warning]); 2.

[Ada] Allow warning tag in pragma Warnings (Off, string)

This patch allows the use of a warning tag as the second parameter of a pragma Warnings (Off\On, ...) pragma. The effect is to control all error messages in that category. This tag may be either [-gnatw?] for a particular category of errors, or [restriction warning] to cover all restriction

[Ada] Add missing entities to Stand.Tree_Read and Stand.Tree_Write

Several entities were not written by Tree_Write and correspondingly not set by Tree_Read. Theoretically this could affect ASIS if it used any routines needing these entities, but we have never observed any issues in this area, so it is likely this is just a latent bug with no observable functional

[Ada] Do not complain about restricted references within defining units

Restrictions No_Abort_Statements and No_Dynamic_Attachment follow exactly the RM rule which forbids any references to certain entities. But this should not apply to the units in which these entities are declared, since otherwise, for example, a pragma Inline for one of these entities is a

[Ada] Fix error of not diagnosing bad body with non-standard file names

If Source_File_Name pragmas with patterns were used to specify a non- standard naming scheme, then the compiler would fail to diagnose an attempt to compile a spec which did not need a body when in fact a body file was present. Given a gnat.adc file containing: 1. pragma

[Ada] PR ada/9535 improved consistency of stream primitives for datagram sockets

This change implements a suggested improvement to the behaviour of stream primitives for streams backed by datagram sockets: a Read or Write call now corresponds to exactly one Receive_Socket or Send_Socket call. Test case: $ gnatmake -q udp_stream $ ./udp_stream Got 5 characters: hello with

[Ada] Implement legality rules for shared volatile variables

This patch implements the rules defined in SPARK 2014 RM section C.6. The rules forbit certain constructs to be labelled as volatile. -- Source -- -- shared_variables.ads package Shared_Variables with SPARK_Mode = On is type T is new Integer with Volatile;

[Ada] Update SPARK cross references for local packages

Cross references for GNATprove on SPARK code should not use local packages as valid scopes, but instead the enclosing subprogram, which is the meaningful scope to distinguish between local and global variables. Tested on x86_64-pc-linux-gnu, committed on trunk 2014-05-21 Yannick Moy

[Ada] Fix error in classification of restriction warnings

Some restriction warnings messages were still being tagged as [enabled by default] instead of [restriction warning]. The following program used not to give the warning since it got incorrectly suppressed (compiled with -gnatj55 -gnatw.d -gnatl) 1. pragma Warnings (Off, [enabled by default]);

[Ada] Overriding_Indicators not legal on protected subprogram bodies

The compiler incorrectly allows overriding_indicators to be applied to protected subprogram bodies (and flags a style error with -gnatyO when they're missing), but those are disallowed by the Ada RM (see RM-8.3.1(3-6) and AC95-00213 for confirmation of intent). This is fixed, but the error can be

[Ada] Proper handling of packed array of small record with reverse SSO

This change ensures proper processing for a packed array of 4-bit records specified with reverse scalar storage order. The following program must compile quietly and execute as shown: $ gnatmake -q reduced_pkd_array_small_rec $ ./reduced_pkd_array_small_rec Config 0 = 1 Config 1 = 3 Config 2 =

[Ada] Warnings on use of uninitialized entities in an instance

This patch adds warnings to uses of potentially uninitialzed entities in instances. If an entity of a generic type has default initialization, then the corresponding actual type should be fully initialized, or else there will be uninitialized components in the instantiation that might go

[Ada] Reject the use of volatiles in assertion expressions

This patch corrects the trigger which determines the proper context of a volatile object with enabled property Async_Writers or Effective_Reads. -- Source -- -- assert_exprs.ads package Assert_Exprs with SPARK_Mode is type T is new Integer with Volatile;

[Ada] Implement new restriction No_Fixed_IO

A new restriction No_Fixed_IO, which requires partition-wide consistent use, forbids fixed I/O operations which may end up using floating-point at run-time. These include any refernce to Fixed_IO or Decimal_IO in packages Ada.Text_IO, Ada.Wide_Text_IO, and Ada.Wide_Wide_Text_IO, and any use of the

Re: [PATCH] Add support for GNU/Hurd in gnat-4.9

The build went fine. Is something still missing? We never keep commented out code, except with a ??? comment explaining why. We don't use 'FIXME', we use ??? instead. Also, some of the comments seem to be copy/paste from freebsd, which is likely not appropriate for GNU Hurd, so need to be

Re: [PATCH] Add support for GNU/Hurd in gnat-4.9

Do you want me to remove all GNU/Hurd specific header file info? No, I want you to remove commented out code, such as: +-- SIGLTHRRES : constant := 32; -- GNU/LinuxThreads restart signal +-- SIGLTHRCAN : constant := 33; -- GNU/LinuxThreads cancel signal +-- SIGLTHRDBG : constant :=

Re: [PATCH] Add support for GNU/Hurd in gnat-4.9

That's actually the biggest concern when people submit a new port: they submit it, get it approved, commit it and then are no longer available for any maintenance when these files need to be updated/become outdated/ no longer compile or run. I can try to do that in the near future, then

Re: [ada, build] Ignore cp -p failures during Ada make install

It seems to me that (as already done in one of three cases in the install-gnatlib target) $(INSTALL_DATA_DATE) errors should be ignored, to allow for such a case. The following patch does just that and allowed the make install to complete. Ok for mainline? No, it's not OK to ignore all

Re: [RFC] Add aarch64 support for ada

The Makfile.in and init.c changes are OK. The types.h change is likely more controversial and may be problematic, I'll let Eric comment. + system.adssystem-linux-x86_64.ads IMO, this should really be called system-linux-lp64.ads, and should be usable for any 64-bit target that uses full

Re: Please revert the patches in bug #54040 and #59346 and special case x32

What do you think, Arno? I think that the POSIX breakage (and its fallout for the other Unices) is ugly and worth the additional complication. Yes, your patch looks good to me. Arno

[Ada] PR ada/60411

This change enables ZCX on armel linux, and should fix PR ada/60411, at least for the native part reported in comment #1 PR ada/60411 * system-linux-armel.ads (Backend_Overflow_Checks): Set to True. (Support_64_Bit_Divides): Removed, no longer used.

[Ada] Illegal use of SPARK volatile object not detected

This patch simplifies the entity resolution machinery which detects an illegaly used SPARK volatile object with enabled external properties Async_Writers or Effective_Reads. The mechanism no longer traverses the parent chain as this is not needed. -- Source -- --

[Ada] Memory leak with Ada 2012 iterator loop

This patch plugs several memory leaks involving Ada 2012 iterator loops by properly managing the secondary stack at each iteration of the loop. -- Source -- -- iterator_leak.adb with Ada.Containers; use Ada.Containers; with Ada.Containers.Vectors; with Ada.Text_IO;

[Ada] Handling of SPARK aspects/pragmas on subprogram body stubs

This patch reimplements the support for SPARK aspects/pragmas that apply to a subprogram body stub and implements a missing rule which forbids the placement of refinement annotations in subunits. -- Source -- -- error.ads package Error with SPARK_Mode = On,

[Ada] Implement new pragma Warning_As_Error

This implements a new pragma Warning_As_Error which can be used to specify that selected warnings are to be treated as errors. See new documentation in GNAT RM for full details. The pragma can appear either in a global configuration pragma file (e.g. gnat.adc), or at the start of a file. Given a

[Ada] Better enforcement of No_Dynamic_Attachment/No_Abort_Statements

No_Dynamic_Attachment is now enforced in -gnatc mode, and includes checking for any use of any of the entities, including rename and access. No_Abort_Statements now checks for any use of Abort_Task, including renaming. The following test programs are compiled using -gnatc -gnatj55. 1. pragma

[Ada] Do not issue warning specific to compilation in GNATprove mode

In GNATprove mode, a warning on ignored pre/post on imported subprograms was misleading, as it was meant for compilation only, while formal verification does take these into account. Hence, we do not generate this warning in GNATprove mode anymore. Tested on x86_64-pc-linux-gnu, committed on

[Ada] Do not expand dynamic subtypes for expressions in GNATprove_mode

During expansion, extra subtypes are generated for many expressions. This is in fact not needed and even harmful for the formal verification mode controlled by GNATprove_mode. This subtype expansion is now disabled in GNATprove_mode. Tested on x86_64-pc-linux-gnu, committed on trunk 2014-02-24

[Ada] Handling of generalized indexing in ASIS

This patch introduces a new semantic attribute Generalized_Indexing, for indexed_components that are instances of Ada 2012 container indexing operations. Analysis and resolution of such nodes is performed on the attribute, and the original source is preserved for ASIS operations. If expansion is

[Ada] Enabled external properties and volatile objects

This patch corrects the predicate which determines whether an object has an enabled external property to account for implicitly enabled properties. Tested on x86_64-pc-linux-gnu, committed on trunk 2014-02-24 Hristian Kirtchev kirtc...@adacore.com * sem_prag.adb (Analyze_Global_Item):

[Ada] Add missing Ravenscar restrictions

This patch enforces the restrictions No_Local_Timing_Events and No_Specific_Termination_Handlers when the Ravenscar restrictions are in effect, as required by D.13(6/3). The following tests must trigger the following errors: $ gcc -c tev.adb tev.adb:6:04: violation of restriction

[Ada] Improve error handling in Ada.Directories search system

This change ensures that when iterating on directory entries using Ada.Directories, and some parent of the searched directory is not accessable, Use_Error is appropriately raised (instead of just yielding no entries). The following program must raise USE_ERROR when run in a directory whose parent

[Ada] Syntax checks when SPARK_Mode is Off

This patch adds syntax checks for SPARK aspects/pragmas Abstract_State, Depends, Global, Initializes, Part_Of, Refined_Global, Refined_Depends and Refined_State that trigger when SPARK features are disabled through SPARK_Mode = Off. The patch also suppresses refinement-related checks when the

[Ada] Internal access to Reason for Warnings Off

This is an internal change to allow retrieval of the Reason argument for a given message suppressed by Warnings (Off). No functional effect. Tested on x86_64-pc-linux-gnu, committed on trunk 2014-02-20 Robert Dewar de...@adacore.com * errout.adb (Set_Warnings_Mode_Off): Add Reason

[Ada] Issue with SPARK aspects and generics

This patch corrects the propagation of various SPARK aspects from a generic template to an instance. -- Source -- -- values.ads package Values is In_1 : Integer := 1234; end Values; -- gen.ads with Values; use Values; generic package Gen with Abstract_State

[Ada] Proper handling of Raise_Expression nodes in Ada 2012

A Raise_Expression is expected to be of any type, and can appear as a component of any expression. This patch introduces a new type Raise_Type, that is the initial type of such a node prior to full resolution. A Raise_Expression node must eventually carry the type imposed by the context. If the

[Ada] Allow Object_Size that is a multiple of the alignment

For composite types, any object size should be allowed that is a multiple of the alignment, but the front end was rejecting some cases. The following should compile clean, giving the output shown for -gnatR2: 1. package ObjSizeTest is 2.type R is record 3. A : Integer;

[Ada] Improve error messages on SPARK annotations

This patch updates the error diagnostics of various SPARK features to emit clearer and more descriptive messages. -- Source -- -- messages.ads package Messages with SPARK_Mode = On is A : Integer := 1; B : Integer := 2; procedure Error_1 (X : in Integer)

[Ada] gnatmake -s: no recompilation when adding some -gnate? switches

When gnatmake is invoked with -s and some additional compilation switches (-gnateA, -gnateE, -gnateF, -gnateinn, -gnateu, -gnateV or -gnateY), recompilation does not necessarily occur. This patch fix this. The test is to invoke gnatmake with -s and one or these switches: recompilation should

[Ada] Error recovery in task body

This patch fixes a crash in a task body with a single statement missing a terminating semicolon. The tree can be repaired locally so further compilation can proceed. Compiling libthr3.adb must yield: libthr3.adb:10:18: missing ; libthr3.adb:13:04: warning: no accept for entry Test ---

[Ada] Accept a constituent in a null dependency clause

This patch implements the following SPARK RM rule from 7.2.5 (3g): at least one of its constituents shall be denoted in the input_list of a null_dependency_clause; or -- Source -- -- null_dependency.ads package Null_Dependency with Abstract_State =

[Ada] Incorrect error on valid global refinement

This patch updates the analysis of aspect/pragma Refined_Global to interpret states and variables with an encapsulating state as constituents only when the related state has visible refinement. -- Source -- -- parent.ads package Parent with Abstract_State = State is

[Ada] GNAT driver and externally built library project files

When the GNAT driver is invoked to bind a main of a project file, and there are externally built library projects in the closure of the main project file, the invocation of gnatbind may fail if the object directory does not contain any ALI files. Tested on x86_64-pc-linux-gnu, committed on trunk

[Ada] Missing parentheses on [Refined_]Global and [Refined_]Depends

This patch modifies the parser to detect missing parentheses on SPARK aspects Global, Depends, Refined_Global and Refined_Depends. -- Source -- -- malformed_contracts.ads package Malformed_Contracts with Abstract_State = (State_1, State_2) is procedure OK_1

[Ada] Semantics of attribute 'Old in aspect/pragma Contract_Cases

This patch implements rule SPARK RM 6.1.3 (5) which states: If an Old attribute_reference occurs within a consequence other than the consequence selected for (later) evaluation as described above, then the associated implicit constant declaration (see Ada RM 6.1.1) is not elaborated.

[Ada] Fix removal of side-effects in GNATprove mode

In the GNATprove mode for formal verification, side-effects are removed from expressions when the corresponding procedure is called in the frontend. This should only be done when not inside a generic, which is both useless and harmful as it deactivates the mechanism for name resolution of generic

[Ada] Legality rules for Synchronization aspect on protected operations

This patch detects additional errors when a Synchronization aspect on an overriding protected operation does not match the given aspect on the overridden operation of an ancestor interface. Compiling b95000g.ads must yield: b95000g.ads:29:13: type Lock_Type must implement abstract

[Ada] Do not perform expansion of generics even in GNATprove mode

In GNATprove mode for formal verification, some treatment typically only done during expansion needs to be performed on the tree, but it should not be applied inside generics. Otherwise, this breaks the name resolution mechanism for genetic instances. This completes a previous similar fix. Tested

[Ada] Duplicate projects due to symbolic links

When the same projec is imported by several projects in the project tree through different paths that includes symbolic links, the Project Manager may reported an error indicating that two different projects have the same name. This is corrected by this patch. Tested on x86_64-pc-linux-gnu,

[Ada] Reduce use of N_Reference nodes in generated code

This is an internal optimization that reduces the number of cases in which we generate N_Reference nodes. Generally has no effect on functional behavior, but the following test: 1. function StrangeRef (A, B : Integer) return Integer is 2.X : Integer; 3. begin 4.X :=

[Ada] Use of attributes 'Old and 'Result and local entities in another 'Old

This patch implements the following sentence from Ada RM 6.1.1 (27/3): The prefix of an Old attribute_reference shall not contain a Result attribute_reference, nor an Old attribute_reference, nor a use of an entity declared within the postcondition expression but not within prefix itself

Re: Use [warning enabled by default] for default warnings

IMO the natural assumption is that gnu++11 is enabled by default, which is how Lars also read it. There seemed to be support for using warning enabled by default instead, so this patch does that. Tested on x86_64-linux-gnu. OK to install? I'll post an Ada patch separately. FWIW this

Re: [Ada] Use [warning enabled by default] for default warnings

This switches Ada from using [enabled by default] to [warning enabled by default] for consistency with: http://gcc.gnu.org/ml/gcc-patches/2014-02/msg00549.html Tested on x86_64-linux-gnu. OK if the above patch goes in? As I just mentioned, this isn't OK at first sight. Arno

[Ada] Exception during finalization of controlled object

This patch corrects the finalization machinery to properly handle a controlled object that is initialized by an aggregate and acts as a transient. The object is now considered fully initialized after the last component assignment takes place. This avoids the finalization of uninitialized data that

[Ada] Crash on processing external property

This patch modifies the mechanism that detects an enabled property to handle the case where the property appears with an expression. -- Source -- -- serial_port.ads pragma SPARK_Mode; package Serial_Port with Abstract_State = (Input_Port with External =

[Ada] Predicates on partial views

This patch fixes some errors in the handling of dynamic predicates applied to private types. Compiling and executing the following: gnatmake -q -gnata main main must yield: Endevour Ariane5 Failure to launch --- with gnat.io; with ada.assertions; procedure Main is package

[Ada] Exception during finalization of controlled object

This patch corrects the transient object machinery to detect subprogram calls in constructs that have been heavily expanded. -- Source -- -- types.ads with Ada.Finalization; use Ada.Finalization; package Types is Bomb : exception; Not_Zero : exception;

[Ada] Forbid the use of aspect/pragma SPARK_Mode in generics

The following patch modifies the analysis of generic packages and subprograms to flag aspect/pragma SPARK_Mode as illegal. -- Source -- -- in_function.ads pragma SPARK_Mode (On); generic Val : Integer; function In_Function return Integer with SPARK_Mode; --

[Ada] Composite postconditions

This patch fixes the order in which the conjuncts in complex postconditions are tested. Such postconditions are expanded into individual tests, chained to internal lists when aspects are processed, and combined with other tests when building the contract checking procedure for a given subprogram.

<    6   7   8   9   10   11   12   13   14   15   >