* SPARK Question @ 2013-05-01 8:35 M. Enzmann 2013-05-01 13:35 ` Phil Thornley 2013-05-02 5:48 ` M. Enzmann 0 siblings, 2 replies; 13+ messages in thread From: M. Enzmann @ 2013-05-01 8:35 UTC (permalink / raw) Hi all, I have a question regarding post- and pre-conditions for subprograms that use private types as arguments / return values. I am trying the following: I want to encapsulate a vector type in a private tagged record. Attempting to access "internals" of the tagged type in PRE / POST annotations is then clearly not feasible. I can use getter / setter functions in the annotations, there is however a problem regarding the sequence in which I declare these subprograms. I read in the Proof-Manual, that I should be using proof-functions, yet I am not quite sure I know how to do this. Especially the part about writing rules for the given proof-function is hard to grasp for me... Let me clarify what I want to do using an example: First I declare an unconstrained vector-type, then I declare an constrained type, that is then being encapsulated in the tagged type. > Number_Of_Elements : constant Positive := 100; > subtype Basis_Type is Float; > > -- ----------------------------------------------------------------------- > -- Type declarations > -- ----------------------------------------------------------------------- > > -- declare an unconstrained array to exchange vectors of different sizes > type Uncon_Array is array (Positive range <>) of Basis_Type; > > -- define the range of the array index > subtype Array_Range is Integer range 1 .. Number_Of_Elements; > > -- array constrained to the index range > subtype Basic_Array is Uncon_Array (Array_Range); > > -- declare the primary vector type as tagged private record > type Basic_Vector is tagged private; and in the private part > type Basic_Vector is tagged > record > Values : Basic_Array; > Length : Natural; > end record; The vector can now hold a maximum of "Number_Of_Elements" Values, although the actually used length will in most cases be smaller. This "true" length is shown by the component "Length" in the record. Reading a single element of the vector now needs a function > function Get_Value > (The_Vector : in Basic_Vector; > At_Position : in Positive) > return Basis_Type; > --# PRE At_Position in Array_Range; which clearly will not work if "At_Position" is larger than "Number_Of_Elements". Furthermore it will however not give a useful result, if "At_Position" is larger than "The_Vector.Length". How can I express this in a pre-condition? I can write a function > function Vector_Length (The_Vector : in Basic_Vector) return Positive; and use this in the pre-condition. This leaves however a couple of questions open, so I'd prefer to do this in a different way. As far as I understand, a proof-function > --# function Vec_Length (The_Vector : in Basic_Vector) return Positive; could do the trick in the specification and a more elaborate version of the pre-condition will then be used in the body. I have however no idea, how the two are linked and how I can express the relationship in the rules file. Any help will be appreciated! TIA, Marc ^ permalink raw reply [flat|nested] 13+ messages in thread
* Re: SPARK Question 2013-05-01 8:35 SPARK Question M. Enzmann @ 2013-05-01 13:35 ` Phil Thornley 2013-05-07 6:59 ` Yannick Duchêne (Hibou57) 2013-05-02 5:48 ` M. Enzmann 1 sibling, 1 reply; 13+ messages in thread From: Phil Thornley @ 2013-05-01 13:35 UTC (permalink / raw) In article <0efb385b-279a-49b7-8289-86b0e99e7930@googlegroups.com>, enzmann.m@googlemail.com says... [snip] > The vector can now hold a maximum of "Number_Of_Elements" Values, although the actually used length will in most cases be smaller. This "true" length is shown by the component "Length" in the record. > > Reading a single element of the vector now needs a function > > > function Get_Value > > (The_Vector : in Basic_Vector; > > At_Position : in Positive) > > return Basis_Type; > > --# PRE At_Position in Array_Range; > > which clearly will not work if "At_Position" is larger than "Number_Of_Elements". Furthermore it will however not give a useful result, if "At_Position" is larger than "The_Vector.Length". > > How can I express this in a pre-condition? I can write a function > > > function Vector_Length (The_Vector : in Basic_Vector) return Positive; > > and use this in the pre-condition. This leaves however a couple of questions open, so I'd prefer to do this in a different way. > > As far as I understand, a proof-function > > > --# function Vec_Length (The_Vector : in Basic_Vector) return Positive; > > > could do the trick in the specification and a more elaborate version of the > pre-condition will then be used in the body. I have however no idea, how the > two are linked and how I can express the relationship in the rules file. Assuming you are using the latest version of SPARK, the simplest way to do this is to also include the proof function Vec_Length in the body, and give it a return annotation. So in the spec put: --# function Vec_Length (The_Vector : in Basic_Vector) --# return Positive; function Get_Value (The_Vector : in Basic_Vector; At_Position : in Positive) return Basis_Type; --# PRE At_Position in Array_Range'First .. Vec_Length(The_Vector); and in the body put: --# function Vec_Length (The_Vector : in Basic_Vector) --# return Positive; --# return The_Vector.Length; With the other code as you have it in your post, this leaves one unprovable VC for Get_Value, as the value of Length in the record is declared as Natural. If this is changed to Array_Range it makes the VC provable, and proved by the Simplifier. (But this then means that you cannot have an empty vector - which can be fixed by declaring another subtype for Length that includes 0). You need to be aware that by doing it this way rather than having a coded function for Vec_Length (which you say you don't want to do) you are making a claim for Vec_Length that cannot be validated by the proof tools. (See section 3.3 of the document "Calling functions in SPARK proof contexts"). Cheers, Phil ^ permalink raw reply [flat|nested] 13+ messages in thread
* Re: SPARK Question 2013-05-01 13:35 ` Phil Thornley @ 2013-05-07 6:59 ` Yannick Duchêne (Hibou57) 2013-05-07 7:54 ` Georg Bauhaus 0 siblings, 1 reply; 13+ messages in thread From: Yannick Duchêne (Hibou57) @ 2013-05-07 6:59 UTC (permalink / raw) Le Wed, 01 May 2013 15:35:20 +0200, Phil Thornley <phil.jpthornley@gmail.com> a écrit: > Assuming you are using the latest version of SPARK, the simplest way to > do this is to also include the proof function Vec_Length in the body, > and give it a return annotation. So in the spec put: > > --# function Vec_Length (The_Vector : in Basic_Vector) > --# return Positive; > > function Get_Value > (The_Vector : in Basic_Vector; > At_Position : in Positive) > return Basis_Type; > --# PRE At_Position in Array_Range'First .. Vec_Length(The_Vector); > That's exactly the kind of thing I miss with Ada 2012's Pre/Post: ability to define something for use in pre/post only, without injecting it in the real program. That's finally what the above do. -- “Syntactic sugar causes cancer of the semi-colons.” [1] “Structured Programming supports the law of the excluded muddle.” [1] [1]: Epigrams on Programming — Alan J. — P. Yale University ^ permalink raw reply [flat|nested] 13+ messages in thread
* Re: SPARK Question 2013-05-07 6:59 ` Yannick Duchêne (Hibou57) @ 2013-05-07 7:54 ` Georg Bauhaus 2013-05-07 20:44 ` Jacob Sparre Andersen news 0 siblings, 1 reply; 13+ messages in thread From: Georg Bauhaus @ 2013-05-07 7:54 UTC (permalink / raw) On 07.05.13 08:59, Yannick Duchêne (Hibou57) wrote: > Le Wed, 01 May 2013 15:35:20 +0200, Phil Thornley <phil.jpthornley@gmail.com> a écrit: >> Assuming you are using the latest version of SPARK, the simplest way to >> do this is to also include the proof function Vec_Length in the body, >> and give it a return annotation. So in the spec put: >> >> --# function Vec_Length (The_Vector : in Basic_Vector) >> --# return Positive; >> >> function Get_Value >> (The_Vector : in Basic_Vector; >> At_Position : in Positive) >> return Basis_Type; >> --# PRE At_Position in Array_Range'First .. Vec_Length(The_Vector); >> > > That's exactly the kind of thing I miss with Ada 2012's Pre/Post: ability to define something for use in pre/post only, without injecting it in the real program. That's finally what the above do. > In practical cases, contract-only predicates might well vanish during optimization phases in compilers, I think, in case the programmers decide that assertion checking can be turned off. ^ permalink raw reply [flat|nested] 13+ messages in thread
* Re: SPARK Question 2013-05-07 7:54 ` Georg Bauhaus @ 2013-05-07 20:44 ` Jacob Sparre Andersen news 2013-05-19 18:54 ` phil.clayton 0 siblings, 1 reply; 13+ messages in thread From: Jacob Sparre Andersen news @ 2013-05-07 20:44 UTC (permalink / raw) [-- Warning: decoded text below may be mangled, UTF-8 assumed --] [-- Attachment #1: Type: text/plain, Size: 2699 bytes --] "Georg Bauhaus" <rm.dash-bauhaus@futureapps.de> wrote in message news:5188b317$0$6555$9b4e6d93@newsspool4.arcor-online.net... > On 07.05.13 08:59, Yannick Duchêne (Hibou57) wrote: >> Le Wed, 01 May 2013 15:35:20 +0200, Phil Thornley >> <phil.jpthornley@gmail.com> a écrit: >>> Assuming you are using the latest version of SPARK, the simplest way to >>> do this is to also include the proof function Vec_Length in the body, >>> and give it a return annotation. So in the spec put: >>> >>> --# function Vec_Length (The_Vector : in Basic_Vector) >>> --# return Positive; >>> >>> function Get_Value >>> (The_Vector : in Basic_Vector; >>> At_Position : in Positive) >>> return Basis_Type; >>> --# PRE At_Position in Array_Range'First .. Vec_Length(The_Vector); >>> >> >> That's exactly the kind of thing I miss with Ada 2012's Pre/Post: ability >> to define something for use in pre/post only, without injecting it in the >> real program. That's finally what the above do. >> > > In practical cases, contract-only predicates might well vanish > during optimization phases in compilers, I think, in case the > programmers decide that assertion checking can be turned off. I agree. Compilers do not include dead code in programs, regardless of why that code is dead. So there is little practical difference between having some sort of contract-only predicate functions and having them generally available. Moreover, I'm very skeptical that having contract-only functions is a good idea, especially for preconditions. For a precondition, the caller is supposed to ensure that the precondition is true before making the call. How can a programmer do this if the predicate is not available to them? For instance, it's common to have code like: if Is_Open (Log_File) then Put_Line (Log_File, ...); -- else don't log, file has failed for some reason. end if; where the precondition on Put_Line includes "Is_Open (File)". If the programmer can't write Is_Open in their code, they cannot avoid the failure nor program around it. All they can do is handle the exception, which is often the worst way to handle the situation. Similarly, postconditions often include conditions that hold true after the call, and it's quite common for those conditions to feed into following preconditions (as in Post => Is_Open(File) after a call to Open). So, as much as possible, postconditions should use the same functions that are used in preconditions. (The more that's done, the more likely that the compiler can completely eliminate the pre- and post- condition checks even when they're turned on.) Randy. ^ permalink raw reply [flat|nested] 13+ messages in thread
* Re: SPARK Question 2013-05-07 20:44 ` Jacob Sparre Andersen news @ 2013-05-19 18:54 ` phil.clayton 2013-05-20 23:40 ` Randy Brukardt 0 siblings, 1 reply; 13+ messages in thread From: phil.clayton @ 2013-05-19 18:54 UTC (permalink / raw) On Tuesday, 7 May 2013 21:44:12 UTC+1, Jacob Sparre Andersen news wrote: > "Georg Bauhaus" <...@futureapps.de> wrote in message > news:...@newsspool4.arcor-online.net... > > On 07.05.13 08:59, Yannick Duch�ne (Hibou57) wrote: > >> Le Wed, 01 May 2013 15:35:20 +0200, Phil Thornley > >> <...@gmail.com> a �crit: > >>> Assuming you are using the latest version of SPARK, the simplest way to > >>> do this is to also include the proof function Vec_Length in the body, > >>> and give it a return annotation. So in the spec put: > >>> > >>> --# function Vec_Length (The_Vector : in Basic_Vector) > >>> --# return Positive; > >>> > >>> function Get_Value > >>> (The_Vector : in Basic_Vector; > >>> At_Position : in Positive) > >>> return Basis_Type; > >>> --# PRE At_Position in Array_Range'First .. Vec_Length(The_Vector); > >>> > >> > >> That's exactly the kind of thing I miss with Ada 2012's Pre/Post: ability > >> to define something for use in pre/post only, without injecting it in the > >> real program. That's finally what the above do. > >> > > > > In practical cases, contract-only predicates might well vanish > > during optimization phases in compilers, I think, in case the > > programmers decide that assertion checking can be turned off. > > I agree. Compilers do not include dead code in programs, regardless of why > that code is dead. So there is little practical difference between having > some sort of contract-only predicate functions and having them generally > available. > > Moreover, I'm very skeptical that having contract-only functions is a good > idea, especially for preconditions. For a precondition, the caller is > supposed to ensure that the precondition is true before making the call. How > can a programmer do this if the predicate is not available to them? For > instance, it's common to have code like: > > if Is_Open (Log_File) then > Put_Line (Log_File, ...); > -- else don't log, file has failed for some reason. > end if; > > where the precondition on Put_Line includes "Is_Open (File)". > > If the programmer can't write Is_Open in their code, they cannot avoid the > failure nor program around it. All they can do is handle the exception, > which is often the worst way to handle the situation. > > Similarly, postconditions often include conditions that hold true after the > call, and it's quite common for those conditions to feed into following > preconditions (as in Post => Is_Open(File) after a call to Open). So, as > much as possible, postconditions should use the same functions that are used > in preconditions. (The more that's done, the more likely that the compiler > can completely eliminate the pre- and post- condition checks even when > they're turned on.) Addressing the last paragraph above, the basis of the point is that reusing the same syntactic form of predicate in pre- and postconditions makes it easy for a compiler to spot that a predicate is a consequence of an earlier predicate. I certainly agree with that! But surely this would allow only the _subsequent_ occurrences of the predicate to be optimized out? Above, you seem to suggest that both the initial and subsequent occurrence of a predicate can be optimized out. In the example above example, it may be possible for the initial occurrence, the postcondition Is_Open(File) of subprogram Open, to be optimized out but that is surely for different reasons - the compiler having special knowledge about the subprogram Open. In general, for user-defined subprograms, determining statically whether a predicate P(X) holds is, in general, difficult. Once established, it is straightforward to use the theorem P(X) ⇒ P(X) to establish that subsequent occurrences of the same form hold. Separately, even when reusing the same syntactic form of predicate in pre- and postconditions, optimizing out subsequent occurrences of the predicate may not be possible as often as one would hope. Given two occurrences of the predicate P(X), to establish that the subsequent occurrence holds, it necessary (for the theorem above) to establish that the X is the same in both occurrences. In the case that X is visible outside its package and between the two occurrences of P(X) there is a call to a subprogram in another package, I can't see how a compiler would know that X won't be changed. (I'm assuming that compilers don't look at the bodies of other packages when compiling a package.) To avoid such issues, formal methods tools typically require subprograms to have a 'frame' annotation that indicates which variables a subprogram may change. So, in summary, optimizing out predicates in pre- and postconditions may not be that easy. Phil ^ permalink raw reply [flat|nested] 13+ messages in thread
* Re: SPARK Question 2013-05-19 18:54 ` phil.clayton @ 2013-05-20 23:40 ` Randy Brukardt 0 siblings, 0 replies; 13+ messages in thread From: Randy Brukardt @ 2013-05-20 23:40 UTC (permalink / raw) <phil.clayton@lineone.net> wrote in message news:68e3b5b0-db45-4aeb-b6c4-817fe6845e5e@googlegroups.com... On Tuesday, 7 May 2013 21:44:12 UTC+1, Randy Brukardt wrote: ... >> Similarly, postconditions often include conditions that hold true after >> the >> call, and it's quite common for those conditions to feed into following >> preconditions (as in Post => Is_Open(File) after a call to Open). So, as >> much as possible, postconditions should use the same functions that are >> used >> in preconditions. (The more that's done, the more likely that the >> compiler >> can completely eliminate the pre- and post- condition checks even when >> they're turned on.) >Addressing the last paragraph above, the basis of the point is that reusing >the >same syntactic form of predicate in pre- and postconditions makes it easy >for a >compiler to spot that a predicate is a consequence of an earlier predicate. >I >certainly agree with that! But surely this would allow only the >_subsequent_ >occurrences of the predicate to be optimized out? Above, you seem to >suggest >that both the initial and subsequent occurrence of a predicate can be >optimized out. You're right that only the "subsequent" occurrences can be optimized out - but, in well-designed abstractions, the initial state also has a well-known set of predicates. This might be hard to model in Ada 2012, although invariants certainly would help. Starting out with undefined properties is not a good idea, so the only issue is whether there is a clear way to communicate that. For instance, a file starts out with Is_Open = False. The compiler and static analyzer need to know this! It's too late to wait until Open is called. > In the example above example, it may be possible for the initial > occurrence, > the postcondition Is_Open(File) of subprogram Open, to be optimized out > but that is surely for different reasons - the compiler having special > knowledge > about the subprogram Open. Postconditions get optimized out based on the actual contents of the body. This sort of optimization should be trivial (it is made with complete knowledge of the implementation, presuming the implementation is contained in a single package body, which normally should be the case). At the call site, they're assumptions (they've either been checked or proved, either way you don't need to recheck them). > In general, for user-defined subprograms, determining statically whether a > predicate P(X) holds is, in general, difficult. Once established, it is > straightforward to use the theorem P(X) ? P(X) > to establish that subsequent occurrences of the same form hold. It's certainly true "in general", where predicate contents include functions with and depending on side-effects, where the initial state of objects is not defined, where privacy is not used properly. But why should we care about the optimization and performance of poorly designed software? > Separately, even when reusing the same syntactic form of predicate in > pre- and postconditions, optimizing out subsequent occurrences of the > predicate may not be possible as often as one would hope. Given two > occurrences of the predicate P(X), to establish that the subsequent > occurrence holds, it necessary (for the theorem above) to establish that > the X is the same in both occurrences. In the case that X is visible > outside its package and between the two occurrences of P(X) there is > a call to a subprogram in another package, I can't see how a compiler > would know that X won't be changed. (I'm assuming that compilers > don't look at the bodies of other packages when compiling a package.) > To avoid such issues, formal methods tools typically require > subprograms to have a 'frame' annotation that indicates which variables > a subprogram may change. First of all, compilers do this all the time. Any compiler that takes advantage of 10.2.1(18/3) [and most do] have been doing this for many years. In addition, this is essentially the same problem as identifying common subexpressions, a problem that optimizers have been doing since the beginning of (computer) time. So there is absolutely nothing new here. (The only part of this that would be new in Janus/Ada is the idea of assumptions, and that fits in very well with our existing optimization technology.) Secondly, one hopes that most that "predicates" are good, that is that they don't violate the Implementation Permission 11.4.2(27/3). One also hopes that most objects are of private types and are not modified "out-of-band" (whether this is possible is determinable from the declaration of the type, so it doesn't require looking into bodies to figure out - ignoring Chapter 13 effects of course, which are usually erroneous if they have this sort of effect). And I'm assuming that function side-effects are declared somehow. (Without these things, you can't do any call optimizations without either looking in bodies or appealing to the Pure permissions of 10.2.1 - which are rarely applicable.) I agree that Ada 2012 doesn't go far enough to define these things. The global in/global out contracts that we worked on but ended up abandoning as insufficiently fully baked certainly would have helped a lot. We actually tried to come up with a rule for 11.4.2 that would have allowed such optimizations in all cases (that is certainly the intent -- that "assertions" that contain any sort of side-effects are bad). We didn't put it into the Standard because we weren't able to draft one that didn't throw out good things with the bad. But the intent is still there, and it's possible that such a rule (a version 10.2.1(18) for 11.4.2) will appear in the future. >So, in summary, optimizing out predicates in pre- and postconditions may >not be that easy. That's probably true in Ada 2012, especially if you don't use implementation-defined stuff like Pure_Function (in GNAT). That's why I was babbling about an Ada-like language with an extension to constraints that could carry the missing information. Perhaps there is a way to get that information into Ada as well (I'm not as sure). Randy. ^ permalink raw reply [flat|nested] 13+ messages in thread
* Re: SPARK Question 2013-05-01 8:35 SPARK Question M. Enzmann 2013-05-01 13:35 ` Phil Thornley @ 2013-05-02 5:48 ` M. Enzmann 1 sibling, 0 replies; 13+ messages in thread From: M. Enzmann @ 2013-05-02 5:48 UTC (permalink / raw) Phew! VCs are tough cookies. For me at least... Thanks for the help Phil! ^ permalink raw reply [flat|nested] 13+ messages in thread
* SPARK question @ 2018-08-27 14:10 Simon Wright 2018-08-27 16:39 ` Shark8 0 siblings, 1 reply; 13+ messages in thread From: Simon Wright @ 2018-08-27 14:10 UTC (permalink / raw) With SPARK CE 2018, I'm seeing commander.ads:103:08: high: "memory accessed through objects of access type" must be a global Output of "Commander_Watchdog" Google tells me nothing, any clues here? (and, obvs, where _should_ I be asking?) ^ permalink raw reply [flat|nested] 13+ messages in thread
* Re: SPARK question 2018-08-27 14:10 SPARK question Simon Wright @ 2018-08-27 16:39 ` Shark8 2018-08-27 20:19 ` Simon Wright 0 siblings, 1 reply; 13+ messages in thread From: Shark8 @ 2018-08-27 16:39 UTC (permalink / raw) On Monday, August 27, 2018 at 8:10:13 AM UTC-6, Simon Wright wrote: > With SPARK CE 2018, I'm seeing > > commander.ads:103:08: high: "memory accessed through objects of > access type" must be a global Output of "Commander_Watchdog" > > Google tells me nothing, any clues here? (and, obvs, where _should_ I be > asking?) I think it's saying that you need a "Global" aspect on "Commander_Watchdog", see https://blog.adacore.com/spark-2014-rationale-data-dependencies -- in particular: procedure Add (X, Y : in Integer) with Global => (Output => Global_Variable); ^ permalink raw reply [flat|nested] 13+ messages in thread
* Re: SPARK question 2018-08-27 16:39 ` Shark8 @ 2018-08-27 20:19 ` Simon Wright 2018-08-27 21:36 ` Randy Brukardt 0 siblings, 1 reply; 13+ messages in thread From: Simon Wright @ 2018-08-27 20:19 UTC (permalink / raw) Shark8 <onewingedshark@gmail.com> writes: > On Monday, August 27, 2018 at 8:10:13 AM UTC-6, Simon Wright wrote: >> With SPARK CE 2018, I'm seeing >> >> commander.ads:103:08: high: "memory accessed through objects of >> access type" must be a global Output of "Commander_Watchdog" >> >> Google tells me nothing, any clues here? (and, obvs, where _should_ I be >> asking?) > > I think it's saying that you need a "Global" aspect on > "Commander_Watchdog", see > https://blog.adacore.com/spark-2014-rationale-data-dependencies -- in > particular: > > procedure Add (X, Y : in Integer) with > Global => (Output => Global_Variable); Yes, but! similar messages say e.g. commander.ads:103:08: high: "Current_System_Status" must be a global Output of "Commander_Watchdog" and I can't see any "objects of access type" used in Commander_Watchdog. ^ permalink raw reply [flat|nested] 13+ messages in thread
* Re: SPARK question 2018-08-27 20:19 ` Simon Wright @ 2018-08-27 21:36 ` Randy Brukardt 2018-08-28 19:05 ` Simon Wright 0 siblings, 1 reply; 13+ messages in thread From: Randy Brukardt @ 2018-08-27 21:36 UTC (permalink / raw) "Simon Wright" <simon@pushface.org> wrote in message news:lyk1oblfz7.fsf@pushface.org... > Shark8 <onewingedshark@gmail.com> writes: > >> On Monday, August 27, 2018 at 8:10:13 AM UTC-6, Simon Wright wrote: >>> With SPARK CE 2018, I'm seeing >>> >>> commander.ads:103:08: high: "memory accessed through objects of >>> access type" must be a global Output of "Commander_Watchdog" >>> >>> Google tells me nothing, any clues here? (and, obvs, where _should_ I be >>> asking?) >> >> I think it's saying that you need a "Global" aspect on >> "Commander_Watchdog", see >> https://blog.adacore.com/spark-2014-rationale-data-dependencies -- in >> particular: >> >> procedure Add (X, Y : in Integer) with >> Global => (Output => Global_Variable); > > Yes, but! similar messages say e.g. > > commander.ads:103:08: high: "Current_System_Status" must be a global > Output of "Commander_Watchdog" > > and I can't see any "objects of access type" used in Commander_Watchdog. I'd guess that it comes from some dereference, and that might be in some subprogram that you called. (But I'm reasoning from the proposed Ada 2020 rules and not the slightly different SPARK rules.) It's also possible that some Ada feature you used is internally implemented with an access type, but I wouldn't have expected SPARK to pick that up. Randy. ^ permalink raw reply [flat|nested] 13+ messages in thread
* Re: SPARK question 2018-08-27 21:36 ` Randy Brukardt @ 2018-08-28 19:05 ` Simon Wright 0 siblings, 0 replies; 13+ messages in thread From: Simon Wright @ 2018-08-28 19:05 UTC (permalink / raw) "Randy Brukardt" <randy@rrsoftware.com> writes: > "Simon Wright" <simon@pushface.org> wrote in message > news:lyk1oblfz7.fsf@pushface.org... >> Shark8 <onewingedshark@gmail.com> writes: >> >>> On Monday, August 27, 2018 at 8:10:13 AM UTC-6, Simon Wright wrote: >>>> With SPARK CE 2018, I'm seeing >>>> >>>> commander.ads:103:08: high: "memory accessed through objects of >>>> access type" must be a global Output of "Commander_Watchdog" >>>> >>>> Google tells me nothing, any clues here? (and, obvs, where _should_ >>>> I be asking?) >>> >>> I think it's saying that you need a "Global" aspect on >>> "Commander_Watchdog", see >>> https://blog.adacore.com/spark-2014-rationale-data-dependencies -- in >>> particular: >>> >>> procedure Add (X, Y : in Integer) with >>> Global => (Output => Global_Variable); >> >> Yes, but! similar messages say e.g. >> >> commander.ads:103:08: high: "Current_System_Status" must be a global >> Output of "Commander_Watchdog" >> >> and I can't see any "objects of access type" used in >> Commander_Watchdog. > > I'd guess that it comes from some dereference, and that might be in > some subprogram that you called. (But I'm reasoning from the proposed > Ada 2020 rules and not the slightly different SPARK rules.) It's also > possible that some Ada feature you used is internally implemented with > an access type, but I wouldn't have expected SPARK to pick that up. I think you must be right. I had thought that gnatprove would choke on any use of 'access', this is clearly not so (now). ^ permalink raw reply [flat|nested] 13+ messages in thread
end of thread, other threads:[~2018-08-28 19:05 UTC | newest] Thread overview: 13+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2013-05-01 8:35 SPARK Question M. Enzmann 2013-05-01 13:35 ` Phil Thornley 2013-05-07 6:59 ` Yannick Duchêne (Hibou57) 2013-05-07 7:54 ` Georg Bauhaus 2013-05-07 20:44 ` Jacob Sparre Andersen news 2013-05-19 18:54 ` phil.clayton 2013-05-20 23:40 ` Randy Brukardt 2013-05-02 5:48 ` M. Enzmann -- strict thread matches above, loose matches on Subject: below -- 2018-08-27 14:10 SPARK question Simon Wright 2018-08-27 16:39 ` Shark8 2018-08-27 20:19 ` Simon Wright 2018-08-27 21:36 ` Randy Brukardt 2018-08-28 19:05 ` Simon Wright
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox