User manual MATLAB POLYSPACE PRODUCTS FOR C 7

[. . . ] PolySpace® Products for C 7 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 C 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. [. . . ] Consider using -unit-by-unit verification. Manually generate a main for the application. Yes Application > 10K lines? Yes If you have passed level 0, you have meaningful results at level 0; open the PolySpace Viewer. Reduce procedure complexity. Yes Still blocked? 7-35 7 Troubleshooting Verification Problems Reducing Code Complexity To reduce code complexity, The MathWorks recommends that you try the following techniques, in the order listed: · "Reducing Procedure Complexity" on page 7-47 · "Reducing Task Complexity" on page 7-49 · "Reducing Variable Complexity" on page 7-50 After you use any of these techniques, restart the verification. Turning Antivirus Software Off Disabling or switching off any third-party antivirus software for the duration of a verification can reduce the verification time by up to 40%. Tuning PolySpace Parameters Impact of Parameter Settings Compromise to balance the time required to perform a verification and the time required to review the results. Launching PolySpace verification with the following options reduces the time taken for verification. However, these parameter settings compromise the precision of the results. The less precise the results of the verification, the more time you can spend reviewing the results. Recommended Parameter Tuning The MathWorks suggests that you use the parameters in the sequence listed. If the first suggestion does not increase the speed of verification sufficiently, then introduce the second, and so on. · Switch from -O2 to a lower precision; · Set the -respect-types-in-globals and -respect-types-in-fields options; · Set the -k-limiting option to 2, then 1, or 0; · Manually stub missing functions which write into their arguments. 7-36 Reducing Verification Time · If some code uses some large arrays, use the -no-fold option. For example, an appropriate launching command is polyspace-c -O0 -respect-types-in-globals -k-limiting 0 Subdividing Code · "An Ideal Application Size" on page 7-37 · "Benefits of Subdividing Code" on page 7-37 · "Possible Issues with Subdividing Code" on page 7-38 · "Recommended Approach" on page 7-39 · "Selecting a Subset of Code" on page 7-41 An Ideal Application Size People have used PolySpace software to analyze numerous applications with greater than 100, 000 lines of code. There always is a compromise between the time and resources required to analyze an application, and the resulting selectivity. The larger the project size, the broader the approximations PolySpace software makes. Broader approximations produce more oranges. Large applications can require you to spend much more time analyzing the results and your application. These approximations enable PolySpace software to extend the range of project sizes it can manage, to perform the verification further, and to solve traditionally incomputable problems. Balance the benefits derived from verifying a whole large application against the loss of precision that results. Benefits of Subdividing Code Subdividing a large application into smaller subsets of code provides several benefits. You: · Quickly isolate a meaningful subset · Keep all functional modules 7-37 7 Troubleshooting Verification Problems · Can maintain a high precision level (for example, level O2) · Reduce the number of orange items · Get correct results are correct because you do not need to remove any thread affecting change shared data · Reduce the code complexity considerably Possible Issues with Subdividing Code Subdividing code can lead to these problems: · Orange checks can result from a lack of information regarding the relationship between modules, tasks, or variables. · Orange checks can result from using too wide a range of values for stubbed functions. · Some loss of precision; the verification consider all possible values for a variable. When the code consists of a small subset of a larger project, PolySpace software automatically stubs many procedures. PolySpace bases the stubbing on the specification or prototype of the missing functions. PolySpace verification assumes that all possible values for the parameter type are returnable. Consider two 32-bit integers a and b, which are initialized with their full range due to missing functions. [. . . ] For more information, see "Managing Verification Jobs Using the PolySpace Queue Manager" on page 6-7 in the PolySpace Products for C User Guide. 12-6 Glossary Glossary Atomic In computer programming, 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 Graphical User Interface. Category One of four types of orange check: potential bug, inconclusive check, data set issue and basic imprecision. [. . . ]