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=0.6 required=5.0 tests=BAYES_20,INVALID_MSGID autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,934d920f8c38f830 X-Google-Attributes: gid103376,public From: sgb@erlang.praxis.co.uk (Stephen Bull) Subject: Re: static code analysis Date: 1997/01/20 Message-ID: #1/1 X-Deja-AN: 211195243 distribution: inet sender: sgb@praxis.co.uk references: <5bnt03$2bj@news1.mnsinc.com> to: wfrye@mnsinc.com cc: pna@praxis.co.uk, denton@praxis.co.uk organization: Praxis plc newsgroups: comp.lang.ada Date: 1997-01-20T00:00:00+00:00 List-Id: wfrye@mnsinc.com (William Frye) writes: A few months ago I posted here asking for information on a tool to create a listing of the conditional clauses in an Ada program (the intent is to create a test matrix for existing code.) Someone suggested that I look at a "static code analyzer" on The Home of the Brave Ada Programmer web site. I have not been able to find such a thing, perhaps someone could give me more info so I can find it. The SPARK Examiner is capable of producing this sort of information; however, as your source code is probably not written in the SPARK subset, significant effort may be required to convert it. The SPARK Examiner performs static code analysis on programs written in the SPARK language, which is a secure subset of Ada, augmented by annotations. SPARK is formally defined and SPARK programs are predictable and can be rigorously analysed. The SPARK Examiner checks the conformance of a program to the rules of SPARK, carries out a flow analysis of the code, and supports formal verification. Absence of run-time errors can be demonstrated rigorously. SPARK is a product of Praxis, a Software Engineering firm specialising in complex systems in a variety of markets. To learn more please visit the following web sites: SPARK technology: http://www.praxis.co.uk/technols/spark/spark.htm Praxis Critical Systems: http://www.praxis.co.uk/services/critsys/critsys.htm or contact: Denton Clutterbuck Praxis Critical Systems 20 Manvers Street Bath BA1 1PX UK email: sparkinfo@praxis.co.uk tel: +44 (0)1225 444700 fax: +44 (0)1225 465205 -- ----------------------------------------------------------------------------- Stephen Bull Praxis Critical Systems 20 Manvers Street BATH BA1 1PX UK +1225 444700 (switchboard) +1225 739286 (direct) +1225 739281 (fax) ----------------------------------------------------------------------------- -- ----------------------------------------------------------------------------- Stephen Bull Praxis Critical Systems 20 Manvers Street BATH BA1 1PX UK +1225 444700 (switchboard) +1225 739286 (direct) +1225 739281 (fax) -----------------------------------------------------------------------------