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,6405eefbf080daa6 X-Google-Attributes: gid103376,public From: "George Romanski" Subject: Re: Is an RTOS Required for Ada? Date: 1999/05/26 Message-ID: #1/1 X-Deja-AN: 482362991 Sender: news@sd.aonix.com (USENET News Admin @flash) X-Nntp-Posting-Host: 192.157.137.176 References: <373B2927.7B22F898@pop.safetran.com> <19990514155120.03860.00000396@ng-cr1.aol.com> <7hmc18$jr6$1@nnrp1.deja.com> <7i1b7p$3nb$1@nnrp1.deja.com> <7ifapi$lf1$1@nnrp1.deja.com> Organization: Aonix, San Diego, CA, USA Newsgroups: comp.lang.ada X-Mimeole: Produced By Microsoft MimeOLE V4.71.1712.0 Date: 1999-05-26T00:00:00+00:00 List-Id: Robert Dewar wrote in message <7ifapi$lf1$1@nnrp1.deja.com>... >In article , > "George Romanski" wrote: >> >> If the compiler inserts code for you, then this inserted code >> must also be verified at level A. (you will need >> requirements design, source code tests and all appropriate >> reviews) > >Right! Of course the line between generating code for the source >you write, and "inserting code" is a very difficult, perhaps >impossible line to draw. Agreed > >Let's take two extremes. The only inlining that goes on in GNORT >for example is very simple stuff. For example, if someone writes >a call to To_Address (XYZ) from System.Storage_Elements, then >this is inlined, but it also generates no code at all (it is >basically an unchecked conversion). There is no place in the >GNORT generated code where you see anything other than >straightforward code generation that corresponds exactly to >what you would expect from the source code. > >Let's assume on the other hand that a GNORT like compiler >decides that it would be really nice to implement tasking. >It does it by including the entire code of the tasking run time >in your generated program. You can't simply decide that this >is inlining, though it could be technically achieved by >inlining. An attempt to say that this code did not need >independent certification would indeed be completely bogus >and would be considered cheating! Agreed > >Drawing the precise line between these two extremes would not >be an easy task. In the case of GNORT itself, we keep the subset >so simple thatno such bogus insertions of code ever occur. You >don't typically want fancy language features anyway in a >safety-critical application! Let's take an array assignment as an example. If the arrays do not overlap (slicing is forbidden) then a single decision may be present (for the loop - assuming the loop is not unrolled) Providing the assignment is completed the decision would have been evaluated both true and false. If the arrays overlap, then a decision may be required to decide the direction of the indexing, and a decision for the loop. If the array has a smaller component size than a normal addressed memory unit (e.g. we can move a word quicker than 4 bytes) then the loop may move words until it gets to the edges. This will require more decisions for the operation. For Level B code, ALL decisions must be shown to have been taken in both directions. ( or the code must be identified and analysed explicitly). It may be hard to write test conditions that evaluate all inlined decisions in both directions. My personal view (there is majority, but no concensus on this at present) is that inserted code which includes decisions must be identified and verified, for level B. For level A multiple conditions would require additional verification. Inserted code that includes no branches will be verified with the application itself, it must be shown that it has been executed, but may not require specific tests. If the language is so restricted that there are no branches in non-user developed code ( the run-time system which includes code to initialise the target processor, and any code generator suport routines) then verification of the application becomes easier. Of course this must be balanced with the cost of the user having to write and verify more code to compensate for the reduced functionality offered by the subset. > >Robert Dewar >Ada Core Technologies > > >--== Sent via Deja.com http://www.deja.com/ ==-- >---Share what you know. Learn what you don't.---