User manual MATLAB POLYSPACE PRODUCTS FOR ADA 5

[. . . ] PolySpace® Products for Ada 5 User's Guide How to Contact The MathWorks Web Newsgroup www. mathworks. com/contact_TS. html Technical Support www. mathworks. com comp. soft-sys. matlab suggest@mathworks. com bugs@mathworks. com doc@mathworks. com service@mathworks. com info@mathworks. com Product enhancement suggestions Bug reports Documentation error reports Order status, license renewals, passcodes Sales, pricing, and general information 508-647-7000 (Phone) 508-647-7001 (Fax) The MathWorks, Inc. 3 Apple Hill Drive Natick, MA 01760-2098 For contact information about worldwide offices, see the MathWorks Web site. PolySpace® Products for Ada User's Guide © COPYRIGHT 1999­2010 by The MathWorks, Inc. The software described in this document is furnished under a license agreement. The software may be used or copied only under the terms of the license agreement. [. . . ] The PolySpace software now provides a specific option for the Green Hills Ada compiler. For more information, see "Operating system target for Standard Libraries compatibility". The $POLYSACE_ADA/adainclude/greenhills folder contains the Green Hills compiler include files. Package Analysis Limitation Problem. Suppose you have a types package that defines a task to a pointer type. Other packages include this type package using the with clause. When you use that pointer type in the package, you cannot analyze that package. Take these steps: 7-15 7 Troubleshooting Verification 1 Copy package specifications that have unsupported construction from the includes folder to the include-modified folder. 2 In these file, comment out every unsupported construction. 3 Use the -ada-include-dir options in the correct order to use the modified files during analysis. If a package is defined in two different folders, the file compiled and analyzed by the PolySpace Verifier is the last one in the list to be compiled and analyzed. For example: polyspace-ada95 \ -ada-include-dir $HERE/includes \ -ada-include-dir $HERE/includes-modified \ -extensions-for-spec-files "*. a??" Explanation. By taking these steps, you do not have to modify the original files. You must maintain copies of the original files in the includes-modified folder. These types of includes do not change very often. Use this workaround for any Ada compiler standard include. 7-16 Reducing Verification Time Reducing Verification Time In this section. . . "PolySpace Verification Duration" on page 7-17 "An Ideal Application Size" on page 7-17 "Optimum Size" on page 7-18 "Selecting a Subset of Code" on page 7-19 "Benefits of These Methods" on page 7-24 PolySpace Verification Duration The following items impact the duration of a verification: · The size of the code · The number of global variables · The nesting depth of the variables (the more nested that the variables are, the longer the verification takes) · The depth of the application call tree · The "intrinsic complexity" of the code, particularly the arithmetic manipulation There are so many factors, that it is impossible to derive a precise formula to calculate verification duration. The following section provides information that might help you reduce the time of a verification. An Ideal Application Size There is a compromise between the time and resources required to verify an application, and the resulting selectivity. The larger the project size, the broader the approximations made by PolySpace. These approximations enable PolySpace to extend the range of project sizes that it can manage and solve incomputable problems. You must balance the benefits from verifying the whole of a large application against the resulting loss of precision. 7-17 7 Troubleshooting Verification Begin with package by package verifications. The maximum recommended application size is 100, 000 lines of code. Sometimes the duration of a verification may not be reasonable. Experience suggests that subdividing an application prior to verification typically has a beneficial impact on selectivity--that is, more red, green, and gray checks, fewer orange warnings, and therefore more efficient bug detection. % of oranges Oranges due to complexity Oranges due to missing parts of the software Size (lines of code) Best usage: 100 KB - 120 KB lines of code A compromise between selectivity and size Optimum Size PolySpace software verifies numerous applications with greater than one hundred thousand lines of code. [. . . ] To open the spooler, select PolySpace > Open Spooler . For more information, see "Managing Verification Jobs Using PolySpace Queue Manager" on page 6-6 in the PolySpace Products for Ada User Guide. 11-11 11 Verifying Code in the EclipseTM IDE 11-12 Glossary Glossary Atomic In computer programming, the adjective atomic describes a unitary action or object that is essentially indivisible, unchangeable, whole, and irreducible. Atomicity In a transaction involving two or more discrete pieces of information, either all of the pieces are committed or none are. Batch mode Execution of PolySpace from the command line rather than via the Launcher GUI. [. . . ]