Re: static code analysis

[sgb@erlang.praxis.co.uk (Stephen Bull)]

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)
-----------------------------------------------------------------------------