From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.3 required=5.0 tests=BAYES_00,INVALID_MSGID autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,3d3f20d31be1c33a X-Google-Attributes: gid103376,public From: stt@houdini.camb.inmet.com (Tucker Taft) Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/07/20 Message-ID: #1/1 X-Deja-AN: 257832746 Sender: news@inmet.camb.inmet.com (USENET news) X-Nntp-Posting-Host: houdini.camb.inmet.com References: Followup-To: comp.lang.ada Organization: Intermetrics, Inc. Newsgroups: comp.lang.ada Date: 1997-07-20T00:00:00+00:00 List-Id: Robert A Duff (bobduff@world.std.com) wrote: : In article , : Jon S Anthony wrote: : >In article bobduff@world.std.com (Robert A Duff) writes: : > : >> >> In article , : >> >> jsa@alexandria.organon.com says... : >> >> : >> >> > type Require is boolean range True..True; : >> >> >... : >> >> > : >> >> > Assert : Require := Complex_Precondition(X); : >> : >> This isn't quite right, because RM-11.6 allows the check to be : >> eliminated. : > : >Bob, could you clarify this? : Suppose Complex_Precondition(X) returns False. Normally, you would : expect a range check on the assignment, and that would raise C_E. : However, 11.6(5) says the implementation does *not* have to raise C_E, : since *in the absence of raising it*, the result has no external effect. ... The way I like to think about 11.6(5) is that if a range-check fails, the expression returns a special "undefined" value (equivalent to "bottom" in some formal languages). The compiler can then perform its normal "dead assignment"/"dead variable" elimination on uses of this "undefined" value. For example, if you have a local variable that is assigned some value, but then never used again, many compilers will remove the assignment, and parts of the evaluation of the expression that have no side effects (failing a language-defined check is *not* considered a side-effect -- its effect is captured entirely in the "undefinedness" of the result). The purpose of raising an exception like Constraint_Error as a result of a check failure is to prevent some undefined value from causing some externally visible "junk" output. If the undefined value makes no contribution to external output, then its calculation can be removed like any other piece of dead code. On the other hand, if the undefined value is used as input to some external effect (which includes any output, assigning into a volatile variable, passing to an imported subprogram, returning from the main subprogram, etc.), then an exception is raised to prevent the bad value from producing a bad external effect. The simplest way to use this rule is to mark the target of an assignment as "volatile." Alternatively, create a subprogram that stores its parameter into a volatile global of range True .. True, or that bumps some global error counter (which you ultimately print out). Or use "pragma Assert" which I believe is supported in almost all Ada 95 compilers. -- -Tucker Taft stt@inmet.com http://www.inmet.com/~stt/ Intermetrics, Inc. Burlington, MA USA