| Age | Commit message (Collapse) | Author | Files | Lines |
|---|
|
Unit sem_spark was implementing the borrow-checker for the support of
ownership pointers in SPARK. It has been moved to gnat2why codebase to
facilitate its evolution and allow the more powerful flow analysis to
provide its results for better analysis on pointers.
2019-09-19 Yannick Moy <moy@adacore.com>
gcc/ada/
* gcc-interface/Make-lang.in: Remove references to sem_spark.
* sem_spark.adb, sem_spark.ads: Remove unit.
From-SVN: r275944
|
|
In GNATprove, a borrow during package elaboration is illegal, but a
crash could be issued when analyzing the corresponding declaration. Now
avoid analyzing the declaration in that case.
There is no test as this does not impact compilation.
2019-09-17 Yannick Moy <moy@adacore.com>
gcc/ada/
* sem_spark.adb (Check_Declaration): Do not check the assignment
from an illegal declaration.
From-SVN: r275788
|
|
This change only affects the SPARK toolset. In the part of semantic
analysis enforcing ownership rules for SPARK, it corrects a crash in
analysis of a declaration of a local borrower whose definition is a
chain of several calls to traversal functions.
2019-09-17 Claire Dross <dross@adacore.com>
gcc/ada/
* sem_spark.adb (Get_Observed_Or_Borrowed_Expr): If the
definition of a local borrower contains calls to traversal
functions, the borrowed expression is the first parameter of the
first traversal function call in the definition.
From-SVN: r275785
|
|
2019-08-21 Piotr Trojanek <trojanek@adacore.com>
gcc/ada/
* einfo.adb (Is_Discriminal): Remove extra parens.
(Is_Constant_Object): Simplify by reusing Ekind_In.
(Is_Prival): Remove extra parens.
* checks.adb, exp_ch4.adb, sem_ch3.adb, sem_spark.adb: Minor
reformattings.
From-SVN: r274790
|
|
2019-08-21 Yannick Moy <moy@adacore.com>
gcc/ada/
* sem_spark.adb: Update references to the SPARK RM.
From-SVN: r274787
|
|
Ownership checking done as in GNATprove should ignore address of
subprograms, as it applies only on objects. Now fixed.
There is no impact on compilation.
2019-08-21 Yannick Moy <moy@adacore.com>
gcc/ada/
* sem_spark.adb (Process_Path): Do nothing on address of
subprogram.
From-SVN: r274779
|
|
2019-08-20 Gary Dismukes <dismukes@adacore.com>
gcc/ada/
* ali.adb, ali.ads, aspects.adb, checks.ads, checks.adb,
doc/gnat_rm/implementation_defined_pragmas.rst,
doc/gnat_ugn/building_executable_programs_with_gnat.rst,
einfo.ads, exp_aggr.adb, exp_ch11.adb, exp_ch3.ads, exp_ch4.adb,
exp_disp.adb, inline.adb, libgnat/a-locale.ads,
libgnat/s-soflin.ads, par_sco.adb, repinfo.adb, sem_ch5.adb,
sem_disp.adb, sem_elab.adb, sem_eval.adb, sem_spark.adb,
sem_spark.ads, sinfo.ads: Minor reformattings, typo fixes and
and rewordings.
From-SVN: r274737
|
|
No impact on regular compilation.
2019-08-19 Claire Dross <dross@adacore.com>
gcc/ada/
* sem_spark.ads, sem_spark.adb (Is_Pledge_Function): New
parameter of the generic. Function used to decide whether a
function is a pledge function.
(Check_Not_Borrowed): Disable check inside the second parameter
of a pledge function for the path borrowed by the first
parameter. Also disable checks for entities inside a Global
contract.
From-SVN: r274644
|
|
GNATprove needs to be able to call a subset of the ownership legality
rules from marking. This is provided by a new function
Sem_SPARK.Is_Legal.
There is no impact on compilation.
2019-08-14 Yannick Moy <moy@adacore.com>
gcc/ada/
* sem_spark.adb, sem_spark.ads (Is_Legal): New function exposed
for use in GNATprove, to test legality rules not related to
permissions.
(Check_Declaration_Legality): Extract the part of
Check_Declaration that checks rules not related to permissions.
(Check_Declaration): Call the new Check_Declaration_Legality.
(Check_Type_Legality): Rename of Check_Type. Introduce
parameters to force or not checking, and update a flag detecting
illegalities.
(Check_Node): Ignore attribute references in statement position.
From-SVN: r274454
|
|
--#! r336866
--#! no-mail
SPARK RM rule 3.10(14) restricts the use of Old and Loop_Entry
attributes on prefixes of an owning or observing type (i.e. a type with
access inside).
There is no impact on compilation.
2019-08-14 Yannick Moy <moy@adacore.com>
gcc/ada/
* sem_spark.adb (Check_Old_Loop_Entry): New procedure to check
correct use of Old and Loop_Entry.
(Check_Node): Check subprogram contracts.
(Check_Pragma): Check Loop_Variant.
(Check_Safe_Pointers): Apply checking to library-level
subprogram declarations as well, in order to check their
contract.
From-SVN: r274453
|
|
Like Is_Path_Expression, function Is_Subpath_Expression should consider
the possibility that the subpath is a type conversion or type
qualification over the actual subpath node. This avoids spurious
ownership errors in GNATprove.
There is no impact on compilation.
2019-08-14 Yannick Moy <moy@adacore.com>
gcc/ada/
* sem_spark.adb (Is_Subpath_Expression): Take into account
conversion and qualification.
From-SVN: r274452
|
|
A modified rule in SPARK RM specifies that object declarations of
anonymous access type should only occur immediately in subprogram, entry
or block. Now checked.
There is no impact on compilation.
2019-07-23 Yannick Moy <moy@adacore.com>
gcc/ada/
* sem_spark.ads (Is_Local_Context): New function.
* sem_spark.adb (Check_Declaration): Issue errors on violations
of SPARK RM 3.10(4)
(Process_Path): Do not issue error on borrow/observe during
elaboration, as these are caught by the new rule.
From-SVN: r273721
|
|
A traversal function, especially when implemented as an expression
function, may need to return an if-expression or case-expression, while
still respecting Legality Rule SPARK RM 3.10(5). This case is now
allowed in GNATprove.
There is no impact on compilation.
2019-07-22 Yannick Moy <moy@adacore.com>
gcc/ada/
* sem_spark.adb (Get_Root_Object, Is_Path_Expression,
Is_Subpath_Expression): Add parameter Is_Traversal to adapt
these functions to the case of paths returned from a traversal
function.
(Read_Indexes): Handle the case of an if-expression or
case-expression.
(Check_Statement): Check Emit_Messages only when issuing an
error message. This is important as Emit_Messages may store the
information that an error was detected.
From-SVN: r273693
|
|
Ownership checking as done in SPARK should be applied only to SPARK
code, which requires GNATprove knowledge of the SPARK_Mode boundary.
Transform the checking unit into a generic to allow passing in the
knowledge from GNATprove to that unit in GNAT sources.
Keeping the code in GNAT sources makes it possible in the future to
adapt it further (or simply instantiate it differently) to be used on
Ada code, independently of GNATprove.
There is no impact on compilation.
2019-07-11 Claire Dross <dross@adacore.com>
gcc/ada/
* gnat1drv.adb: SPARK checking rules for pointer aliasing are
moved to GNATprove backend.
* sem_spark.ads, sem_spark.adb (Sem_SPARK): Is now a generic
unit. Takes as parameters:
- Retysp which is used to query the most underlying type
visible in SPARK. We do not introduce aliasing checks for
types which are not visibly deep.
- Component_Is_Visible_In_SPARK is used to avoid doing pointer
aliasing checks on components which are not visible in SPARK.
- Emit_Messages returns True in the second phase of SPARK
analysis. Error messages for failed aliasing checks are only
output in this case.
Additionally, errors on constructs not supported in SPARK are
removed as duplicates of marking errors. Components are stored
in the permission map using their original component to avoid
inconsistencies between components of different views of the
same type.
(Check_Expression): Handle delta constraints.
(Is_Deep): Exported so that we can check for SPARK restrictions
on deep types inside SPARK semantic checkings.
(Is_Traversal_Function): Exported so that we can check for SPARK
restrictions on traversal functions inside SPARK semantic
checkings.
(Check_Call_Statement, Read_Indexes): Check wether we are
dealing with a subprogram pointer type before querying called
entity.
(Is_Subpath_Expression): Image attribute can appear inside a
path.
(Check_Loop_Statement): Correct order of statements in the loop.
(Check_Node): Ignore raise nodes.
(Check_Statement): Use Last_Non_Pragma to get the object
declaration in an extended return statement.
From-SVN: r273402
|
|
Pointer support in GNATprove leads to spurious messages about global
variables, with local variables declared in local packages and protected
components. Now fixed.
There is no impact on compilation.
2019-07-10 Yannick Moy <moy@adacore.com>
gcc/ada/
* sem_aux.adb, sem_aux.ads (Is_Protected_Operation): New
function to determine if a subprogram is protected.
* sem_spark.adb (Setup_Protected_Components): New procedure to
add protected components to the environment.
(Check_Callable_Body): Call the new Setup_Protected_Components.
(Check_Package_Spec): Merge local environment with enclosing one
when done.
From-SVN: r273349
|
|
The new analysis of SPARK pointer rules could crash on some constructs.
Now fixed.
There is no impact on compilation.
2019-07-10 Claire Dross <dross@adacore.com>
gcc/ada/
* sem_spark.adb (Check_Expression): Allow digits constraints as
input.
(Illegal_Global_Usage): Pass in the entity.
(Is_Subpath_Expression): New function to allow different nodes
as inner parts of a path expression.
(Read_Indexes): Allow concatenation and aggregates with box
expressions. Allow attributes Update and Loop_Entry.
(Check_Expression): Allow richer membership test.
(Check_Node): Ignore bodies of generics.
(Get_Root_Object): Allow concatenation and attributes.
From-SVN: r273348
|
|
2019-07-10 Hristian Kirtchev <kirtchev@adacore.com>
gcc/ada/
* bindo-graphs.adb, bindo.adb, debug.adb, exp_ch6.adb,
sem_ch10.adb, sem_ch13.adb, sem_ch3.adb, sem_ch4.adb,
sem_ch6.adb, sem_ch7.adb, sem_res.adb, sem_spark.adb,
sem_util.adb, warnsw.ads: Minor reformatting.
From-SVN: r273335
|
|
Code that violates the conditions for ownership checking should lead to
error messages pointing to the violations instead of crashes.
There is no impact on compilation, only GNATprove.
2019-07-10 Yannick Moy <moy@adacore.com>
gcc/ada/
* sem_spark.adb (Get_Root_Object): Replace precondition by error
message.
(Read_Indexes): Replace precondition by error message.
(Check_Callable_Body): Check only traversal function returns an
anonymous access type.
(Check_Expression): Issue error on unexpected expression as
path.
* sem_util.adb (First_Global): Fix access to global on
entry/task.
From-SVN: r273329
|
|
2019-07-09 Hristian Kirtchev <kirtchev@adacore.com>
gcc/ada/
* exp_ch9.adb, exp_util.adb, repinfo.adb, sem_ch12.adb,
sem_prag.adb, sem_res.adb, sem_spark.adb, sem_util.adb: Minor
reformatting.
From-SVN: r273282
|
|
Allocator expressions and sub-expressions of (extension) aggregates are
implicitly the source of assignments in Ada. Thus, they should be moved
when of a deep type when checking ownership rules in SPARK.
There is no impact on compilation.
2019-07-09 Yannick Moy <moy@adacore.com>
gcc/ada/
* sem_spark.adb (Check_Expression): Handle correctly implicit
assignments as part of allocators and (extension) aggregates.
(Get_Root_Object): Adapt for new path expressions.
(Is_Path_Expression): Return True for (extension) aggregate.
From-SVN: r273271
|
|
Check for declaration of global variables prior to use in the ownership
checking for SPARK.
There is no impact on compilation.
2019-07-09 Yannick Moy <moy@adacore.com>
gcc/ada/
* sem_spark.adb (Get_Perm_Or_Tree): Issue an error when
encountering unknown global variable.
From-SVN: r273267
|
|
Checking of the readable status of sub-expressions occurring in the
target path of an assignment should occur before the right-hand-side is
moved or borrowed or observed.
There is no impact on compilation.
2019-07-09 Yannick Moy <moy@adacore.com>
gcc/ada/
* sem_spark.adb (Check_Expression): Change signature to take an
Extended_Checking_Mode, for handling read permission checking of
sub-expressions in an assignment.
(Check_Parameter_Or_Global): Adapt to new behavior of
Check_Expression for mode Assign.
(Check_Safe_Pointers): Do not analyze generic bodies.
(Check_Assignment): Separate checking of the target of an
assignment.
From-SVN: r273266
|
|
Analysis could crash on extended return of a non-deep type, now fixed.
This has no impact on compilation.
2019-07-04 Yannick Moy <moy@adacore.com>
gcc/ada/
* sem_spark.adb (Check_Statement): Only check permission of
object in extended return when it is of a deep type.
From-SVN: r273055
|
|
Ownership rules for pointer support should only apply to code marked in
SPARK. There is no impact on compilation.
2019-07-04 Yannick Moy <moy@adacore.com>
gcc/ada/
* sem_spark.adb (Check_Package_Spec, Check_Package_Body): Only
analyze parts of the code marked in SPARK.
From-SVN: r273052
|
|
When SPARK code does not follow the ownership rules of SPARK RM 3.10,
the error message now points to a location explaining why the object has
a more restricted permission than the expected one.
There is no impact on compilation.
2019-07-04 Yannick Moy <moy@adacore.com>
gcc/ada/
* sem_spark.adb (Explanation, Get_Expl): New functions to get
the explanation for a permission mismatch.
(Perm_Error, Perm_Mismatch, Perm_Error_Loop_Exit): Take
explanation into account for issuing a more precise error
message.
(Set_Perm_Prefixes, Set_Perm_Extensions,
Set_Perm_Extensions_Move): Pass suitable argument for the
explanation node.
From-SVN: r273050
|
|
Refine the implementation of pointer support for SPARK analysis.
There is no impact on compilation.
2019-07-03 Yannick Moy <moy@adacore.com>
gcc/ada/
* sem_spark.adb (Get_Observed_Or_Borrowed_Expr): New function to
return go through traversal function call.
(Check_Type): Consistently use underlying type.
(Get_Perm): Adapt for case of elaboration code where variables
are not declared in the environment. Remove incorrect handling
of borrow and observe.
From-SVN: r272981
|
|
2019-07-03 Gary Dismukes <dismukes@adacore.com>
gcc/ada/
* bindo-augmentors.adb, bindo-augmentors.ads,
bindo-builders.ads, bindo-elaborators.adb, sem_ch12.adb,
sem_ch13.adb, sem_spark.adb, sinfo.ads: Minor editorial
corrections and reformatting.
From-SVN: r272979
|
|
SPARK rules allow local borrowers and observers to be declared. During
their lifetime, the access to the borrowed/observed object is
restricted.
There is no impact on compilation.
2019-07-03 Yannick Moy <moy@adacore.com>
gcc/ada/
* sem_spark.adb: Add support for locally borrowing and observing
a path.
(Get_Root_Object): Add parameter Through_Traversal to denote
when we are interesting in getting to the traversed parameter.
(Is_Prefix_Or_Almost): New function to support detection of
illegal access to borrowed or observed paths.
(Check_Pragma): Add analysis of assertion pragmas.
From-SVN: r272975
|
|
2019-07-01 Hristian Kirtchev <kirtchev@adacore.com>
gcc/ada/
* checks.adb, exp_ch9.adb, exp_unst.adb, sem_ch4.adb,
sem_prag.adb, sem_spark.adb: Minor reformatting.
From-SVN: r272882
|
|
SPARK RM 3.10 is the final version of the pointer ownership rules. Start
changing the implementation accordingly. Anonymous access types are not
fully supported yet.
There is no impact on compilation.
2019-07-01 Yannick Moy <moy@adacore.com>
gcc/ada/
* sem_spark.adb: Completely rework the algorithm for ownership
checking, as the rules in SPARK RM have changed a lot.
* sem_spark.ads: Update comments.
From-SVN: r272878
|
|
From-SVN: r267683
|
|
2018-12-11 Gary Dismukes <dismukes@adacore.com>
gcc/ada/
* exp_util.ads: Use preferred U.S. spelling of "honored".
* sem_spark.adb: Remove extra whitespace.
From-SVN: r266997
|
|
2018-11-14 Hristian Kirtchev <kirtchev@adacore.com>
gcc/ada/
* back_end.adb, checks.adb, exp_ch3.adb, exp_ch4.adb,
exp_ch7.adb, exp_disp.adb, exp_unst.adb, exp_util.adb,
freeze.adb, sem_ch13.adb, sem_ch6.adb, sem_ch7.adb,
sem_prag.adb, sem_spark.adb, sem_util.adb: Minor reformatting.
From-SVN: r266122
|
|
2018-10-09 Maroua Maalej <maalej@adacore.com>
gcc/ada/
* sem_spark.adb (Check_Declaration): fix bug related to non
access object permissions.
From-SVN: r264979
|
|
2018-09-26 Maroua Maalej <maalej@adacore.com>
gcc/ada/
* sem_spark.adb (Check_Loop_Statement): Fix a bug related to
loop exit environment.
(Check_Statement): fixing a bug when comparing the source and
target in an assignment statement.
From-SVN: r264631
|
|
2018-09-26 Maroua Maalej <maalej@adacore.com>
gcc/ada/
* sem_spark.adb (Check_Param_In, Setup_Parameter_Or_Global):
Change the operation associated to assigning to an IN parameter.
In SPARK, IN access-to-variable is an observe operation for a
function, and borrow operation for a procedure.
From-SVN: r264601
|
|
The implementation of these Ownership rules for safe pointers and
automatic memory management is still a prototype at an experimental
stage.
To activate the checks, the code should be compiled with the debug flag
-gnatdF and the flag -gnatd.F for setting the context for formal
verification of SPARK.
These changes do not affect compilation.
2018-08-21 Maroua Maalej <maalej@adacore.com>
gcc/ada/
* sem_spark.adb (Check_Call_Statement): Check global and formal
parameter permissions at call sites.
(Check_Callable_Body): Assume permissions on globals and
parameters depending on their modes then analyse the body
operations.
(Check_Declaration): Consider both deep (including elementary
access) object declarations and normal variables. First check
whether the deep object is of Ownership Aspec True or not, then,
depending on its initialization, assign the appropriate state.
Check related to non access type variables deal with
initialization value permissions.
(Check_Expression): Check nodes used in the expression being
analyzed.
(Check_Globals): Call by Check_Call_Statement to perform the
check on globals.
(Check_List): Call Check_Node on each element of the list.
(Check_Loop_Statement): Check the Iteration_Scheme and loop
statements.
(Check_Node): Main traversal procedure to check safe pointer usage.
(Check_Package_Body): Check subprogram's body.
(Check_Param_In): Take a formal and an actual parameter and
Check the permission of every in-mode parameter.
(Check_Param_Out): Take a formal and an actual parameter and
check the state of out-mode and in out-mode parameters.
(Check_Statement): Check statements other than procedure call.
(Get_Perm, Get_Perm_Or_Tree, Get_Perm_Tree): Find out the state
related to the given name.
(Is_Deep): Return True if an object is of access type or has
subfields of access type.
(Perm_Error, Perm_Error_Subprogram_End): Add an error message
whenever the found state on the given name is different from the
one expected (in the statement being analyzed).
(Process_Path): Given an operation and a current state, call
Perm_Error if there is any mismatch.
(Return_Declarations, Return_Globals, Return_The_Global): Check
the state of a given name at the end of the subprogram. These
procedures may change depending on how we shall finally deal
with globals and the rhs state in a move operation.
(Set_Perm_Extensions, Set_Perm_Prefixes_Borrow,
Set_Perm_Prefixes, Setup_Globals, Setup_Parameter_Or_Global,
Setup_Parameters): Set up the new states to the given node and
up and down the tree after an operation.
(Has_Ownership_Aspect_True): This function may disappear later
when the Ownership Aspect will be implemented in the FE.
From-SVN: r263727
|
|
2018-05-23 Hristian Kirtchev <kirtchev@adacore.com>
gcc/ada/
* exp_disp.adb, freeze.adb, gnat1drv.adb, sem_ch5.adb, sem_spark.adb:
Minor reformattings.
From-SVN: r260600
|
|
This commit fixes bugs in the code that implements the rules for safe pointers
in SPARK. This only affects SPARK tools, not compilation.
* Global variables should be handled differently compared
to parameters. The whole tree of an in global variable has the
permission Read-Only. In contrast, an in parameter has the
permission Read-Only for the first level and Read-Write permission
for suffixes.
* The suffix X of Integer'image(X) was not analyzed correctly.
* The instruction X'img was not dealt with.
* Shallow aliased types which are not initialized are now allowed
and analyzed.
Dealing with function inlining is not handled correctly yet.
2018-05-23 Maroua Maalej <maalej@adacore.com>
gcc/ada/
* sem_spark.adb: Fix of some permission rules of pointers in SPARK.
From-SVN: r260583
|
|
This patch dismantles the prototype implementation of the first proposal
for Reduction expressions, one of the important potentially parallel
constructs for Ada2020. The ARG is going in a different direction with
a simpler syntax.
2018-05-22 Ed Schonberg <schonberg@adacore.com>
gcc/ada/
* exp_ch4.ads, exp_ch4.adb, exp_util.adb, expander.adb: Remove mention
of N_Reduction_Expression and N_Reduction_Expression_Parameter.
* par-ch4.adb: Remove parsing routines for reduction expressions.
* sem.adb, sinfo.ads, sinfo.adb, sem_ch4.ads, sem_ch4.adb, sem_res.adb,
sem_spark.adb, sprint.adb: Remove analysis routines for reduction
expressions.
From-SVN: r260524
|
|
2018-01-11 Arnaud Charlet <charlet@adacore.com>
gcc/ada/
Bump copyright notices to 2018.
From-SVN: r256519
|
|
2017-12-15 Hristian Kirtchev <kirtchev@adacore.com>
* sem_prag.adb (Analyze_Initialization_Item): Remove the specialized
processing for a null initialization item. Such an item is always
illegal.
2017-12-15 Bob Duff <duff@adacore.com>
* types.ads, types.h, libgnat/a-except.adb, exp_ch11.adb
(PE_Build_In_Place_Mismatch): New reason code for raising when the
BIPalloc formal parameter is incorrect. This can happen if a compiler
bug causes a mismatch of build-in-place between caller and callee.
* exp_ch6.adb (Expand_N_Extended_Return_Statement): Use
PE_Build_In_Place_Mismatch.
2017-12-15 Ed Schonberg <schonberg@adacore.com>
* exp_ch4.ads, exp_ch4.adb (Expand_N_Reduction_Expression): New
procedure.
* exp_util.adb (Insert_Actions): Handle N_Reduction_Expression.
* expander.adb (Expand): Call Expand_N_Reduction_Expression
* par-ch4.adb (P_Reduction_Expression): New procedure.
(P_Iterated_Component_Assoc_Or_Reduction): New precedure, extension of
P_Iterated_Component_Association.
(OK_Reduction_Expression_Parameter): New procedure.
(P_Aggregate_Or_Paren_Expr): Improve error message for malformed delta
aggregate.
* sem.adb (Analyze): Call Analyze_Reduction_Expression and
Analyze_Reduction_Expression_Parameter
* sinfo.ads, sinfo.adb: New node kinds N_Reduction_Expression and
N_Reduction_Expression_Parameter.
* sem_ch4.ads, sem_ch4.adb (Analyze_Reduction_Expression,
Analyze_Reduction_Expression_Parameter): New procedures.
* sem_res.adb (Resolve): Handle Reduction_Expression and
Reduction_Expression_Parameter
* sem_spark.adb: Dummy entries for Reduction_Expression and
Reduction_Expression_Parameter
* sprint.adb (Sprint_Node_Actual): Print Reduction_Expression,
Reduction_Expression_Parameter
From-SVN: r255693
|
|
SPARK-related flags.
2017-11-08 Hristian Kirtchev <kirtchev@adacore.com>
* exp_ch3.adb (Expand_N_Object_Declaration): Save and restore relevant
SPARK-related flags. Add ??? comment.
* exp_util.adb (Insert_Actions): Add an entry for node
N_Variable_Reference_Marker.
* sem.adb (Analyze): Add an entry for node N_Variable_Reference_Marker.
* sem_ch8.adb (Find_Direct_Name): Add constant Is_Assignment_LHS. Build
and record a variable reference marker for the current name.
(Find_Expanded_Name): Add constant Is_Assignment_LHS. Build and record
a variable reference marker for the current name.
* sem_elab.adb (Build_Variable_Reference_Marker): New routine.
(Extract_Variable_Reference_Attributes): Reimplemented.
(Info_Scenario): Add output for variable references and remove output
for variable reads.
(Info_Variable_Read): Removed.
(Info_Variable_Reference): New routine.
(Is_Suitable_Scenario): Variable references are now suitable scenarios
while variable reads are not.
(Output_Active_Scenarios): Add output for variable references and
remove output for variable reads.
(Output_Variable_Read): Removed.
(Output_Variable_Reference): New routine.
(Process_Variable_Read): Removed.
(Process_Variable_Reference): New routine.
(Process_Variable_Reference_Read): New routine.
* sem_elab.ads (Build_Variable_Reference_Marker): New routine.
* sem_res.adb (Resolve_Actuals): Build and record a variable reference
marker for the current actual.
* sem_spark.adb (Check_Node): Add an entry for node
N_Variable_Reference_Marker.
* sem_util.adb (Within_Subprogram_Call): Moved to the library level.
* sem_util.ads (Within_Subprogram_Call): Moved to the library level.
* sinfo.adb (Is_Read): New routine.
(Is_Write): New routine.
(Target): Updated to handle variable reference markers.
(Set_Is_Read): New routine.
(Set_Is_Write): New routine.
(Set_Target): Updated to handle variable reference markers.
* sinfo.ads: Add new attributes Is_Read and Is_Write along with
occurrences in nodes. Update attribute Target. Add new node
kind N_Variable_Reference_Marker.
(Is_Read): New routine along with pragma Inline.
(Is_Write): New routine along with pragma Inline.
(Set_Is_Read): New routine along with pragma Inline.
(Set_Is_Write): New routine along with pragma Inline.
* sprint.adb (Sprint_Node_Actual): Add an entry for node
N_Variable_Reference_Marker.
From-SVN: r254531
|
|
2017-10-09 Justin Squirek <squirek@adacore.com>
* sem_ch3.adb: Rename Uses_Unseen_Priv into
Contains_Lib_Incomplete_Type.
2017-10-09 Hristian Kirtchev <kirtchev@adacore.com>
* sem_aggr.adb, sem_spark.adb, adabkend.adb, exp_ch5.adb, frontend.adb,
sem_ch12.adb, fmap.adb, exp_ch6.adb, exp_spark.adb, lib-load.adb,
exp_ch9.adb, osint.adb, exp_disp.adb, sem_ch8.adb, sem_ch8.ads,
prepcomp.adb, gnat1drv.adb, atree.adb, sinput-l.adb, targparm.adb,
sem_ch10.adb, par-ch8.adb: Minor reformatting.
From-SVN: r253566
|
|
2017-10-09 Bob Duff <duff@adacore.com>
* exp_ch6.adb (Make_Build_In_Place_Call_In_Object_Declaration): Use
Defining_Identifier (Obj_Decl) in two places, because it might have
changed.
* exp_ch6.adb (Make_Build_In_Place_Call_In_Allocator): Deal with cases
involving 'Input on (not visibly) derived types.
2017-10-09 Hristian Kirtchev <kirtchev@adacore.com>
* atree.adb: Add new soft link Rewriting_Proc.
(Rewrite): Invoke the subprogram attached to the rewriting soft link.
(Set_Rewriting_Proc): New routine.
* attree.ads: Add new access-to-subprogram type Rewrite_Proc.
(Set_Rewriting_Proc): New routine.
* checks.adb (Install_Primitive_Elaboration_Check): Use 'E' character
for *E*laboration flag to maintain consistency with other elaboration
flag generating subprograms.
* debug.adb: Document the new usage of flag -gnatdL.
* einfo.adb: Node19 is now used as Receiving_Entry. Node39 is now used
as Protected_Subprogram. Flag148 is now used as
Is_Elaboration_Checks_OK_Id. Flag302 is now used as
Is_Initial_Condition_Procedure.
(Is_Elaboration_Checks_OK_Id): New routine.
(Is_Initial_Condition_Procedure): New routine.
(Protected_Subprogram): New routine.
(Receiving_Entry): New routine.
(SPARK_Pragma): Update assertion.
(SPARK_Pragma_Inherited): Update assertion.
(Suppress_Elaboration_Warnings): Removed.
(Set_Is_Elaboration_Checks_OK_Id): New routine.
(Set_Is_Initial_Condition_Procedure): New routine.
(Set_Protected_Subprogram): New routine.
(Set_Receiving_Entry): New routine.
(Set_SPARK_Pragma): Update assertion.
(Set_SPARK_Pragma_Inherited): Update assertion.
(Write_Entity_Flags): Update the output for Flag148 and Flag302.
(Write_Field19_Name): Add output for Receiving_Entry.
(Write_Field39_Name): Add output for Protected_Subprogram.
(Write_Field40_Name): Update the output for SPARK_Pragma.
* einfo.ads: New attributes Is_Elaboration_Checks_OK_Id,
Is_Initial_Condition_Procedure, Protected_Subprogram, Receiving_Entry.
Remove attribute Suppress_Elaboration_Warnings. Update the stricture
of various entities.
(Is_Elaboration_Checks_OK_Id): New routine along with pragma Inline.
(Is_Initial_Condition_Procedure): New routine along with pragma Inline.
(Protected_Subprogram): New routine along with pragma Inline.
(Receiving_Entry): New routine along with pragma Inline.
(Suppress_Elaboration_Warnings): Removed.
(Set_Is_Elaboration_Checks_OK_Id): New routine along with pragma
Inline.
(Set_Is_Initial_Condition_Procedure): New routine along with pragma
Inline.
(Set_Protected_Subprogram): New routine along with pragma Inline.
(Set_Receiving_Entry): New routine along with pragma Inline.
(Set_Suppress_Elaboration_Warnings): Removed.
* exp_ch3.adb (Build_Init_Procedure): Use name _Finalizer to maintain
consistency with other finalizer generating subprograms.
(Default_Initialize_Object): Mark the block which wraps the call to
finalize as being part of initialization.
* exp_ch7.adb (Expand_N_Package_Declaration): Directly expand pragma
Initial_Condition.
(Expand_N_Package_Body): Directly expand pragma Initial_Condition.
(Next_Suitable_Statement): Update the comment on usage. Skip over call
markers generated by the ABE mechanism.
* exp_ch9.adb (Activation_Call_Loc): New routine.
(Add_Accept): Link the accept procedure to the original entry.
(Build_Protected_Sub_Specification): Link the protected or unprotected
version to the original subprogram.
(Build_Task_Activation_Call): Code cleanup. Use a source location which
is very close to the "begin" or "end" keywords when generating the
activation call.
* exp_prag.adb (Expand_Pragma_Initial_Condition): Reimplemented.
* exp_spark.adb (Expand_SPARK): Use Expand_SPARK_N_Loop_Statement to
process loops.
(Expand_SPARK_N_Loop_Statement): New routine.
(Expand_SPARK_N_Object_Declaration): Code cleanup. Partially insert the
call to the Default_Initial_Condition procedure.
(Expand_SPARK_Op_Ne): Renamed to Expand_SPARK_N_Op_Ne.
* exp_util.adb (Build_DIC_Procedure_Body): Capture the SPARK_Mode in
effect.
(Build_DIC_Procedure_Declaration): Capture the SPARK_Mode in effect.
(Insert_Actions): Add processing for N_Call_Marker.
(Kill_Dead_Code): Explicitly kill an elaboration scenario.
* exp_util.ads (Make_Invariant_Call): Update the comment on usage.
* frontend.adb: Initialize Sem_Elab. Process all saved top level
elaboration scenarios for ABE issues.
* gcc-interface/trans.c (gnat_to_gnu): Add processing for N_Call_Marker
nodes.
* lib.adb (Earlier_In_Extended_Unit): New variant.
* sem.adb (Analyze): Ignore N_Call_Marker nodes.
(Preanalysis_Active): New routine.
* sem.ads (Preanalysis_Active): New routine.
* sem_attr.adb (Analyze_Access_Attribute): Save certain
elaboration-related attributes. Save the scenario for ABE processing.
* sem_ch3.adb (Analyze_Object_Declaration): Save the SPARK mode in
effect. Save certain elaboration-related attributes.
* sem_ch5.adb (Analyze_Assignment): Save certain elaboration-related
attributes. Save the scenario for ABE processing.
* sem_ch6.adb (Analyze_Abstract_Subprogram_Declaration): Save the SPARK
mode in effect. Save certain elaboration-related attributes.
(Analyze_Subprogram_Body_Helper): Skip N_Call_Marker nodes when
locating the first real statement.
(Analyze_Subprogram_Declaration): Save the SPARK mode in effect. Save
certain elaboration-related attributes.
* sem_ch7.adb (Analyze_Package_Declaration): Do not suppress
elaboration warnings.
* sem_ch8.adb (Attribute_Renaming): Mark a subprogram body which was
generated for purposes of wrapping an attribute used as a generic
actual.
(Find_Direct_Name): Save certain elaboration-related attributes. Save
the scenario for ABE processing.
(Find_Expanded_Name): Save certain elaboration-related attributes. Save
the scenario for ABE processing.
* sem_ch9.adb (Analyze_Entry_Declaration): Save certain
elaboration-related attributes.
(Analyze_Requeue): Save certain elaboration-related attributes. Save
the scenario for ABE processing.
(Analyze_Single_Task_Declaration): Save certain elaboration-related
attributes.
(Analyze_Task_Type_Declaration): Save certain elaboration-related
attributes.
* sem_ch12.adb (Analyze_Generic_Package_Declaration): Save certain
elaboration-related attributes.
(Analyze_Generic_Subprogram_Declaration): Save the SPARK mode in
effect. Save certain elaboration-related attributes.
(Analyze_Package_Instantiation): Save certain elaboration-related
attributes. Save the scenario for ABE processing. Create completing
bodies in case the instantiation results in a guaranteed ABE.
(Analyze_Subprogram_Instantiation): Save certain elaboration-related
attributes Save the scenario for ABE processing. Create a completing
body in case the instantiation results in a guaranteed ABE.
(Provide_Completing_Bodies): New routine.
* sem_elab.ads: Brand new implementation.
* sem_prag.adb (Analyze_Pragma, cases Elaborate, Elaborate_All,
Elaborate_Body): Do not suppress elaboration warnings.
* sem_res.adb (Make_Call_Into_Operator): Set the parent field of the
operator.
(Resolve_Call): Save certain elaboration-related attributes. Save the
scenario for ABE processing.
(Resolve_Entity_Name): Do not perform any ABE processing here.
(Resolve_Entry_Call): Inherit certain attributes from the original call.
* sem_util.adb (Begin_Keyword_Location): New routine.
(Defining_Entity): Update the parameter profile. Add processing for
concurrent subunits that are rewritten as null statements.
(End_Keyword_Location): New routine.
(Find_Enclosing_Scope): New routine.
(In_Instance_Visible_Part): Code cleanup.
(In_Subtree): Update the parameter profile. Add new version.
(Is_Preelaborable_Aggregate): New routine.
(Is_Preelaborable_Construct): New routine.
(Mark_Elaboration_Attributes): New routine.
(Scope_Within): Update the parameter profile.
(Scope_Within_Or_Same): Update the parameter profile.
* sem_util.ads (Begin_Keyword_Location): New routine.
(Defining_Entity): Update the parameter profile and the comment on
usage.
(End_Keyword_Location): New routine.
(Find_Enclosing_Scope): New routine.
(In_Instance_Visible_Part): Update the parameter profile.
(In_Subtree): Update the parameter profile. Add new version.
(Is_Preelaborable_Aggregate): New routine.
(Is_Preelaborable_Construct): New routine.
(Mark_Elaboration_Attributes): New routine.
(Scope_Within): Update the parameter profile and the comment on usage.
(Scope_Within_Or_Same): Update the parameter profile and the comment on
usage.
* sem_warn.adb (Check_Infinite_Loop_Warning): Use Has_Condition_Actions
to determine whether a loop has meaningful condition actions.
(Has_Condition_Actions): New routine.
* sinfo.adb (ABE_Is_Certain): Removed.
(Is_Declaration_Level_Node): New routine.
(Is_Dispatching_Call): New routine.
(Is_Elaboration_Checks_OK_Node): New routine.
(Is_Initialization_Block): New routine.
(Is_Known_Guaranteed_ABE): New routine.
(Is_Recorded_Scenario): New routine.
(Is_Source_Call): New routine.
(Is_SPARK_Mode_On_Node): New routine.
(No_Elaboration_Check): Removed.
(Target): New routine.
(Was_Attribute_Reference): New routine.
(Set_ABE_Is_Certain): Removed.
(Set_Is_Declaration_Level_Node): New routine.
(Set_Is_Dispatching_Call): New routine.
(Set_Is_Elaboration_Checks_OK_Node): New routine.
(Set_Is_Initialization_Block): New routine.
(Set_Is_Known_Guaranteed_ABE): New routine.
(Set_Is_Recorded_Scenario): New routine.
(Set_Is_Source_Call): New routine.
(Set_Is_SPARK_Mode_On_Node): New routine.
(Set_No_Elaboration_Check): Removed.
(Set_Target): New routine.
(Set_Was_Attribute_Reference): New routine.
* sinfo.ads: Remove attribute ABE_Is_Certain. Attribute
Do_Discriminant_Check now utilizes Flag3. Attribute
No_Side_Effect_Removal now utilizes Flag17. Add new node
N_Call_Marker. Update the structure of various nodes.
(ABE_Is_Certain): Removed along with pragma Inline.
(Is_Declaration_Level_Node): New routine along with pragma Inline.
(Is_Dispatching_Call): New routine along with pragma Inline.
(Is_Elaboration_Checks_OK_Node): New routine along with pragma Inline.
(Is_Initialization_Block): New routine along with pragma Inline.
(Is_Known_Guaranteed_ABE): New routine along with pragma Inline.
(Is_Recorded_Scenario): New routine along with pragma Inline.
(Is_Source_Call): New routine along with pragma Inline.
(Is_SPARK_Mode_On_Node): New routine along with pragma Inline.
(No_Elaboration_Check): Removed along with pragma Inline.
(Target): New routine along with pragma Inline.
(Was_Attribute_Reference): New routine along with pragma Inline.
(Set_ABE_Is_Certain): Removed along with pragma Inline.
(Set_Is_Declaration_Level_Node): New routine along with pragma Inline.
(Set_Is_Dispatching_Call): New routine along with pragma Inline.
(Set_Is_Elaboration_Checks_OK_Node): New routine along with pragma
Inline.
(Set_Is_Initialization_Block): New routine along with pragma Inline.
(Set_Is_Known_Guaranteed_ABE): New routine along with pragma Inline.
(Set_Is_Recorded_Scenario): New routine along with pragma Inline.
(Set_Is_Source_Call): New routine along with pragma Inline.
(Set_Is_SPARK_Mode_On_Node): New routine along with pragma Inline.
(Set_No_Elaboration_Check): Removed along with pragma Inline.
(Set_Target): New routine along with pragma Inline.
(Set_Was_Attribute_Reference): New routine along with pragma Inline.
* sprint.adb (Sprint_Node_Actual): Add an entry for N_Call_Marker.
From-SVN: r253559
|
|
2017-09-12 Bob Duff <duff@adacore.com>
* sem_ch6.adb (Analyze_Expression_Function): Initialize Def_Id to
Empty.
2017-09-12 Georges-Axel Jaloyan <jaloyan@adacore.com>
* debug.adb: Reserving flag -gnatdF for safe pointer checking.
* gnat1drv.adb (gnat1drv): Adding the call to the analysis on
dF flag.
* sem_spark.adb, sem_spark.ads: Implementation of the analysis,
in preparation for the evolution of the SPARK language that
includes a pointer analysis for checking non-aliasing of access
types. The Check_Safe_Pointers function is the entry point, and
will traverse the AST and raise compile-time errors everytime
it detects non-begign aliasing. Detailed comments are present
in the sem_spark.ads file.
* sem_util.adb, sem_util.ads (First_Global, Next_Global): New
functions to iterate over the list of globals of a subprogram.
* libgnat/system.ads: Add restriction No_Finalization.
* gcc-interface/Make-lang.in: Add new file sem_spark.adb and
dependency on g-dynhta.adb.
From-SVN: r252000
|
