This is the mail archive of the gcc-patches@gcc.gnu.org mailing list for the GCC project.
Index Nav: | [Date Index] [Subject Index] [Author Index] [Thread Index] | |
---|---|---|
Message Nav: | [Date Prev] [Date Next] | [Thread Prev] [Thread Next] |
Other format: | [Raw text] |
This patch provides the initial implementation of aspect Depends. This construct is intended for formal verification proofs. The syntax of the aspect is as follows: DEPENDENCY_RELATION ::= null | DEPENDENCY_CLAUSE {, DEPENDENCY_CLAUSE} DEPENDENCY_CLAUSE ::= OUTPUT_LIST =>[+] INPUT_LIST OUTPUT_LIST ::= null | OUTPUT | (OUTPUT {, OUTPUT}) INPUT_LIST ::= null | INPUT | (INPUT {, INPUT}) OUTPUT ::= NAME | FUNCTION_RESULT INPUT ::= NAME where FUNCTION_RESULT is a function Result attribute_reference The semantics of the aspect are as follows: Every input and output of a dependency_relation of a Depends aspect of a subprogram denotes a state abstraction, an entire variable or a formal parameter of the subprogram. An input must have a mode of in or in out and an output must have an mode of in out or out. [Note: As a consequence an entity which is both an input and an output shall have a mode of in out.] For the purposes of determining the legality of a Result attribute_reference, a dependency_relation is considered to be a postcondition of the function to which the enclosing aspect_specification applies. There can be at most one output_list which is a null symbol and if it exists it must be the output_list of the last dependency_clause in the dependency_relation. An input which is in an input_list of a null output_list may not appear in another input_list of the same dependency_relation. The entity denoted by an output in an output_list shall not be denoted by any other output in that output_list or any other output_list. The entity denoted by an input in an input_list shall not be denoted by any other input in that input_list. Every output of the subprogram shall appear in exactly one output_list. Every input of the subprogram shall appear in at least one input_list. ------------ -- Source -- ------------ -- types.ads package Types is type Rec is record Comp : Natural; end record; type Arr is array (1 .. 5) of Rec; function Get_Comp (Obj : Rec) return Natural; end Types; -- types.adb package body Types is function Get_Comp (Obj : Rec) return Natural is begin return Obj.Comp; end Get_Comp; end Types; -- semantics.ads with Types; use Types; package Semantics with Abstract_State => State is Arr_Obj : Arr; Rec_Obj : Rec; -- Renaming chain of an object Ren_1 : Rec renames Rec_Obj; Ren_2 : Rec renames Ren_1; -- Renaming of a record component Ren_3 : Natural renames Rec_Obj.Comp; -- Renaming of an array element Ren_4 : Rec renames Arr_Obj (3); -- Renaming of a function call result Ren_5 : Natural renames Get_Comp (Rec_Obj); -- Legality rules -- 1. Every input and output of a dependency_relation of a Depends aspect -- of a subprogram denotes a state abstraction, an entire variable or a -- formal parameter of the subprogram. procedure OK_1a (Formal : Natural; Result : out Natural) with Depends => (Result => (State, -- abstract state Arr_Obj, -- object Rec_Obj, -- object Formal)); -- formal procedure OK_1b (Result : out Natural) with Depends => (Result => Ren_1); -- renaming of object procedure OK_1c (Result : out Natural) with Depends => (Result => Ren_2); -- renaming of renaming of object procedure Error_1 (Result : out Natural) with Depends => (Result => (Arr_Obj (3), -- element Rec_Obj.Comp, -- component Get_Comp (Rec_Obj), -- function call Ren_3, -- renaming of component Ren_4, -- renaming of element Ren_5, -- renaming of function call result 1234)); -- junk -- Legality rules -- 3. For the purposes of determining the legality of a Result -- attribute_reference, a dependency_relation is considered to -- be a postcondition of the function to which the enclosing -- aspect_specification applies. function OK_3 return Natural with Depends => (OK_3'Result => Rec_Obj); -- 'Result is an output function Error_3a (Result : out Natural) return Natural with Depends => (Result => Error_3a'Result); -- 'Result is an input function Error_3b (Formal : Natural) return Natural with Depends => (Get_Comp (Rec_Obj)'Result => Formal); -- 'Result must apply to the -- enclosing function -- Legality rules -- 4. There can be at most one output_list which is a null symbol and if it -- exists it must be the output_list of the last dependency_clause in the -- dependency_relation. procedure OK_4a (Formal : Natural; Result : out Natural) with Depends => (Result => Formal, null => Rec_Obj); -- null is last output_list function Error_4a (Formal : Natural) return Natural with Depends => (null => Arr_Obj, -- null is not the last output_list Error_4a'Result => Formal); -- Legality rules -- 4. An input which is in an input_list of a null output_list may not -- appear in another input_list of the same dependency_relation. procedure OK_4b (Formal : Natural; Result : out Natural) with Depends => (Result => Ren_1, null => Formal); procedure Error_4b (Formal : Natural; Result : out Natural) with Depends => (Result => Formal, null => Formal); -- Formal appears in both output_lists -- Legality rules -- 5. The entity denoted by an output in an output_list shall not -- be denoted by any other output in that output_list or any other -- output_list. procedure OK_5a (Result_1 : out Natural; Result_2 : out Natural) with Depends => ((Result_1, Result_2) => Ren_2); procedure OK_5b (Result_1 : out Natural; Result_2 : out Natural) with Depends => (Result_1 => Arr_Obj, Result_2 => Rec_Obj); procedure Error_5 (Result_1 : out Natural; Result_2 : out Natural) with Depends => ((Result_1, Result_2, Result_1) => Arr_Obj, -- Result_1 appears twice Result_2 => Ren_1); -- Result_2 is already in the first input_list -- Legality rules -- 6. The entity denoted by an input in an input_list shall not be denoted -- by any other input in that input_list. function OK_6 (Result : out Natural) return Natural with Depends => (Result => (Rec_Obj, Arr_Obj), OK_6'Result => Rec_Obj); procedure Error_6 (Result : out Natural) with Depends => (Result => (Rec_Obj, Ren_1, Ren_2)); -- All inputs are the same object -- Extra checks procedure Error_E1 (Formal : Natural; Result_1 : out Natural; Result_2 : out Natural; Result_3 : out Natural) with Depends => ((Result_1, (Result_2, Result_3)) => (Formal, (Arr_Obj, Rec_Obj))); -- Cannot have nested groupings such as (Result_2, Result_3) end Semantics; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c -gnat12 -gnatd.V semantics.ads semantics.ads:48:12: item must denote variale, state or formal parameter semantics.ads:49:19: item must denote variale, state or formal parameter semantics.ads:50:12: item must denote variale, state or formal parameter semantics.ads:51:12: item must denote variale, state or formal parameter semantics.ads:52:12: item must denote variale, state or formal parameter semantics.ads:53:12: item must denote variale, state or formal parameter semantics.ads:54:12: item must denote variale, state or formal parameter semantics.ads:68:28: function result cannot act as input semantics.ads:72:28: prefix of attribute "Result" must denote the enclosing function semantics.ads:87:10: null output list must be the last clause in a dependency relation semantics.ads:102:20: input of a null output list appears in multiple input lists semantics.ads:120:31: duplicate use of item semantics.ads:121:11: duplicate use of item semantics.ads:135:21: duplicate use of item semantics.ads:135:28: duplicate use of item semantics.ads:145:19: nested grouping of items not allowed semantics.ads:145:53: nested grouping of items not allowed Tested on x86_64-pc-linux-gnu, committed on trunk 2013-04-11 Hristian Kirtchev <kirtchev@adacore.com> * aspects.ads, aspects.adb: Add Aspect_Depends to all the relevant tables. * elists.ads, elists.adb (Contains): New routine. * par-prag.adb: Pragma Depends does not need any special treatment by the parser. * sem_ch13.adb (Analyze_Aspect_Specifications): Transform aspect Depends into a corresponding pragma. (Check_Aspect_At_Freeze_Point): Aspect Depends does not need inspection at its freeze point. * sem_prag.adb (Analyze_Pragma): Perform analysis and normalization of pragma Depends. Remove the use of function Is_Duplicate_Item. Use End_Scope to uninstalle the formal parameters of a subprogram. Add a value for pragma Depends in table Sig_Flags. (Is_Duplicate_Item): Removed. * snames.ads-tmpl: Add predefined name for Depends as well as a pragma identifier.
Attachment:
difs
Description: Text document
Index Nav: | [Date Index] [Subject Index] [Author Index] [Thread Index] | |
---|---|---|
Message Nav: | [Date Prev] [Date Next] | [Thread Prev] [Thread Next] |