SofCheck Inspector User Guide

## SofCheck Inspector™ for Ada User Guide

### Version 2.1

As of November 2010

Copyright © 2004—2010 SofCheck, Inc. All rights reserved.

The use and distribution of this material is subject to licensing terms.

### Abstract

This document describes how to run the SofCheck Inspector, the advanced static error detection tool, and interpret its output.

### Table of Contents

- About SofCheck Inspector
- How to Run SofCheck Inspector

- System Requirements
- Inspector Console Manages Inspector Projects

- Launching the SofCheck Inspector Console
- Console Project Menu

- New Projects
- Existing Projects

- Console Run Menu
- Console Help Menu

- How to View SofCheck Inspector Output

- Browser Requirements
- Location and Format of Output
- Back and Forward Buttons
- Main Window
- Race Conditions Window
- Message History Window
- Module List Window
- Message Status
- Annotation Report
- Help Window
- Non-Web Output (list subdirectory)

- Messages and Annotations

- Description of Messages
- Race Condition Messages
- Categorization of Inspection Messages
- Description of Annotations

- Preconditions
- Presumptions
- Postconditions
- Unanalyzed calls
- Other Annotations

- SofCheck Inspector Usage Scenarios

- Find Defects in Code
- Use Annotations for Code Reviews
- Identify Possible Race Conditions

- Pragmatic Limitations of static Error Detection

- SofCheck Inspector Presumptions

- Appendix

- Command Line Invocation
- Command Line Options
- Advanced Command Line Options
- return Codes
- SofCheck Inspector Library File
- Troubleshooting
- Frequently Asked Questions (FAQ)

### About SofCheck Inspector | top

SofCheck Inspector is a static error detection tool that automatically identifies possible programming errors and verifies logical correctness, without relying on labor-intensive run time testing. It integrates into existing development tools and processes.

SofCheck Inspector performs line-by-line testing in a fully automated way, and guarantees full path coverage. SofCheck Inspector finds defects early in the development process—in conjunction with compilation—when they are least costly to repair. In addition, it should be run on existing code to find latent defects before they become a problem in the field.

SofCheck Inspector is designed to support large systems and to detect a wide range of programming errors such as misuse of pointers, indexing out of arrays, buffer overflows (a prevalent source of security storage leaks,) numeric overflows, numeric wraparounds, and improper use of Application Programming Interfaces (APIs). It pinpoints the root cause of each error down to the source line of code.

Even in the absence of explicit errors, SofCheck Inspector provides a thorough characterization of every component of the system in terms of its inputs, outputs, heap object creations, the preconditions on the inputs necessary to preclude run-time failures, the presumptions about return values of external subprograms, and the postconditions that characterize the range of outputs.

An inspection may be launched from the command line or interactively, using the SofCheck Inspector Console or one of our plugins for popular IDEs.

### How to Run SofCheck Inspector | top

### System Requirements | top

SofCheck Inspector runs on machines with the Intel x86, Intel x64, Sun Sparc, and Sun x64 CPUs with the Microsoft Windows (x86) and Solaris (Sparc, x64) operating systems. Static error detection is complex and time consuming, and will benefit from all the speed (CPU) and memory (RAM) that can be made available. Dual core 2.0 GHz or greater CPUs can inspect about 1,000 lines of code per minute. SofCheck recommends 2 GB of RAM or more. More complex inspections will require more memory. Four GB of RAM is a practical limit for many 32-bit operating systems. Most 64-bit operating systems can take advantage of more than 4 GB of physical RAM, if available.

SofCheck Inspector analyzes Ada that has been compiled into JVM bytecodes. JVM byte codes are the intermediate compiled representation used by Java compilers and certain other compilers that generate code to run on a Java virtual Machine (JVM). The JVM byte code representation is useful because it is well documented and machine independent. Included with the Inspector is an Ada compiler (adajava/adajbuild) that produces JVM .class files as its output. if using the Inspector Console, this step is done automatically. if not, there is a separate manual provided that explains how to use this Ada compiler. Be sure to provide the "-inspector" flag when invoking adajava or adajbuild to ensure the compiler includes the most possible information in the generated JVM .class files. A future release of the product may use a different compiled representation for Ada.

The .class files which contain the JVM bytecodes define the scope of the inspection. for the best results, inspect bytecodes compiled with full debugging information (automatic if using the SofCheck Inspector Console). Corresponding Ada source files are not required, but should be provided if possible so pre- and postconditions and inspection messages may be interspersed within source listings for ease of understanding.

### SofCheck Inspector Console | top

The SofCheck Inspector Console may be used to interactively manage inspections as projects, allowing you to

- interactively select source files for inspections
- automatically create .library files
- save run time command line options for later recall
- launch and monitor inspections
- halt inspections
- readily view inspection output

### Launching Console | top

Launch the Console by selecting the Start > Programs > SofCheck Inspector > Inspector Console menu item. Alternately, you may execute the RUNCONSOLE.BAT file from the command line. The Inspector Console main window will appear.

The Project drop-down menu lets you create, open, edit and save Inspector project files. The Run drop-down menu lets you launch SofCheck Inspector, monitor its execution, and view its output. The Help drop-down menu lets you view this document and other helpful information.

The Console text area displays diagnostic output from the SofCheck Inspector. The other output of the inspection is written to the file system in the form of HTML files, text files, and the Inspector Database.

### Console Project Menu | top

#### New Projects | top

Select Project > new… (or press Ctrl+N) to create a new Inspector project. You will be asked to select the Project Type:

If you select Ada Project, you will see the following Project Description dialog:

If you select Java Project or Ada and Java Project, you will see the following Project Description dialog:

Enter a Project Name for your Inspector project. The Project Name should conform to an acceptable directory name to be saved to the native file system. Click on the Create button to the right of the edit box, and the Project Name will be used to complete the Project Information fields; at this time, the Project Directory and error.txt log file are also created. For example, type "MyInspection1" in the Project Name edit box and click the Create button. The Project Information fields will be completed as in the following dialog:

You may accept the default names for the project files and directories listed in Project Information or select the Customize Project check box to change them. for each entry you may type new values into the edit boxes or click on the Browse buttons to select existing files. For example, you may wish to have multiple projects use the same database, or you may have an alternate Message Pattern File which you wish to use.

- The Project Directory is the root directory of an Inspector project. By default, the directory is created in the shared documents workspace on the file system (derived from the environment variable %SOFCHECK_PROJECTS%) when you click the Create button. (When you click the Save button, a project file with the name projectname.prj is also created in the Project Directory.)
- The Output Directory is the directory where Inspector generates its output. It is created when an inspection is run for the first time.
- The Database Directory is the directory where Inspector stores a history of inspection messages for a particular project (or set of projects) so it may compare the current inspection to a previous one, and also show trends across multiple inspections. The Database Directory and its contents are created when an inspection is run for the first time.
- The Message Pattern File is used to characterize and filter the inspection messages. The Inspector comes with a default Message Pattern File. This default file is designed to serve most customer needs and as such shouldn't require any modification

Selecting Files to Inspect | top

For an Ada Project, click the Source Files Select button to select one or more source files to be inspected. You will be able to browse a source tree and select source directories or source files. It is important that the files chosen are in a compilable state.

The Inspector analysis engine processes JVM “.class” files, which, for Ada, are produced by the SofCheck Ada Front End (also known as AppletMagic). When the project is saved and Validate Mode is selected, and also right before the project is inspected, the Console invokes the necessary AppletMagic tools (specifically, adareg and adajbuild) to create class files from the selected Ada sources.

For a Java project, click the Source Files Select… button to select one or more source files that correspond to the class files being inspected. You will be able to browse a source tree and select source directories, source files, and archives. For Java, it is the class files that determine the scope of the inspection. As such, selecting source files is optional, but is recommended so that the Inspector can display inspection messages in-line with the source for better context.

The following is an example of a Java Project Source Files selection dialog:

Inspector is able to match source files to their associated class files properly. If you select source files that do not correspond to selected class files, corresponding entries will be listed in the Source Directories that lack classfiles pane. Inspector cannot analyze source files without corresponding class files. Similarly, if you select class files without selecting their associated source files, corresponding entries will be listed in the Class Directories that lack sources pane. In this example, the appropriate class files haven’t been selected yet, which is why there are mismatched sources/classes.

Click on the Show Project Issues button to display a text list of file-selection issues (such as duplicate .java files).

Click the Done button to return to the Project Description dialog.

From the Project Description dialog, click the Class Files Select… button to select one or more class files to be inspected. You will be able to browse a source tree and select class files and archives (including .zip, .jar, .ear and .war files). You must select at least one class file for an inspection to succeed.

The following is an example of a Java Project class Files selection dialog. In this example, corresponding source files have already been selected.

In the source tree, if a class file lacks debug information, that file and its parent directory are highlighted in yellow. If an archive contains a nested archive, that archive and its parent directory are highlighted in red. Inspector does not analyze nested archives; if any are found, they should be extracted to the file system before running Inspector.

As mentioned above, if you select source files that do not correspond to selected class files, corresponding entries will be listed in the Source Directories that lack class files pane. Similarly, if you select class files without selecting their associated source files, corresponding entries will be listed in the Class Directories that lack sources pane.

Click on the Show Project Issues button to display a text list of file-selection issues (such as duplicate .java files).

Click the Done button to return to the Project Description dialog.

The Project Description dialog will indicate that source and class files have been selected, by changing the status message from Not Selected& to Selected, as shown below.

Click on the Options button to modify the project’s run time parameters. The following dialog will appear:

Find out more about Inspector run time parameters in the “ Command Line Options” section. Brief explanations are given below.

- cutoff inspection id: type the inspection id of a previous inspection to use as a cutoff. The selected inspection will be used as the base inspection for this run.
- global (do not partition): By default, the Inspector automatically partitions the system into groups of files (if necessary), to perform the analysis without exceeding the limits of main memory; it then integrates the output from all partitions. Check the “global” checkbox to cause the Inspector to analyze the entire system in the same single partition. This may allow more error-checking to be performed and more errors to be detected, but may also cause the limits of main memory to be exceeded and the analysis of some of the larger files in the system to be skipped.
- allow-duplicates: check this to allow Inspector to continue running if it finds more than one source file that could be associated with a single class file. When duplicate source files are found, one will be arbitrarily chosen.
- additional command options: you may type in a free-form, space-delimited list any additional command line options which should be passed to Inspector. See the SofCheck Inspector User Guide for a complete list.
- identify race conditions: By default, the Inspector identifies potential race conditions in your system; uncheck this box to bypass race-condition analysis.
- singleton task entry points: type in space-delimited patterns in the form “<class>:<method>” that match entry points for singleton, or daemon, threads. Inspector recognizes some common defaults, so this edit box may be left blank.
- reentrant entry points: type in space-delimited patterns in the form “<class>:<method>” that match reentrant entry points. Inspector recognizes some common defaults, so this edit box may be left blank.

In the Project Options dialog, click on the Cancel button to return to the Project Description dialog without preserving any changes. Click on the OK button to preserve changes and return to the Project Description dialog

Saving a Project. | top

In the Project Description dialog, click the Save button to preserve all changes made in the dialog.

For an Ada Project, if the Validate Mode check box is checked, the Console will invoke the SofCheck Ada Front End to generate class files for the Ada sources, when the project is saved. The class files (and intermediate files) are generated in the ada_classes subdirectory of the main project directory area. Suppose your project is named Sudoku and is located in the default location e.g. C:\Documents And Settings\All Users\Documents\sofcheck\inspector\projects\Sudoku; ada_classes would be a subdirectory of Sudoku.

If there are any errors during this build process the messages are logged in the Ierror.txt file. You can view the errors by selecting Show Project Issues… from the Run menu or by pressing Ctrl +I.

You may be warned that the validation process may take a long time with the following dialog box. This it typically not a problem with small projects.

If you see the above dialog, click Yes to proceed with validation and save the selected classes and source files; you will return to the Console main window. Click No to save the class and source selections but return to the Console main window without validating them. Click Cancel to return to the Project Description dialog and continue to make changes. If you click Yes, the Console main window will display the summary of the validation, and the details are saved in error.txt. If you have not already specified a name for the Console Project File (with a .prj suffix by default), the Console will prompt you to enter one (See Project > Save As...), below.

In the above example, some problems were found with the class and source file selections and the reults were written to error.txt.

#### Existing Projects | top

Select Project > Open... (or press Ctrl+O) to open a project file that has been previously saved. You will be prompted to browse for a file on the file system. By default, Inspector project files end in the suffix .prj. When a project file is opened, the Project Description dialog will appear.

Select Project > Edit... (or press Ctrl+E) to edit the current project file. The Project Description dialog will appear.

Select Project > Save As… (or press Ctrl+A) to save the project you are currently editing. You will be prompted to type a filename for saving.

When you are satisfied with the location and name of the project file, click the Save button to save it.

Select Project > Quit (or press Alt+F4) to exit the Inspector Console. If you quit the Console while an inspection is running, the inspection will be terminated.

### Console Run Menu | top

Select Run > Inspect Project … to start the inspection as defined in the currently open project. First, the Estimated Run Time dialog will show an estimated count of lines and classes and give a rough estimate of the expected run time for the inspection. The actual run time may vary by an order of magnitude from the estimate due to variations in code complexity and server hardware, but changes in the estimate from inspection to inspection on the same hardware should give a more reliable indication of relative time. Note that if the class files have not been compiled with debug information, the Console will not be able to estimate a run time. When you run an inspection for the first time, the Output Directory and the Database Directory are created.

Select Run > Regenerate Reports … to regenerate text and html reports for an existing Inspector analysis. This is useful if you have modified the Message Pattern File, or if you specify a new cutoff inspection id against which to compare the current inspection results. It does NOT perform a new analysis of the code.

In the Estimated Run Time dialog, click the Run Now button to begin the inspection or the Cancel button to return to the Console run menu.

When you click on the Run Now button to start the inspection, progress messages will be displayed in the Console main window, as shown below.

Select Run > Clear Console (or press Ctrl+C) to clear any text in the Console text area.

Select Run > Browse Output (or press Ctrl+B) to launch a dialog that will open the “./html/index.html” file in this project's output directory, which enables you to easily browse all output from the run of this project. this option will only work if output has already been generated to the output directory specified in the project information settings. If an inspection is still running, you will see a warning dialog box.

Click OK to dismiss the dialog; any running inspection will continue. if an inspection is complete, you will be allowed to select the output index.html file as shown below.

In the Browse Output Folder dialog, click on the OK button to browse the specified index.html file in your system's default browser. Optionally, click the Browse button to select another HTML file. Click the Cancel button to dismiss the dialog without launching the browser.

Select Run > Show Project Issues... (or press Ctrl+I) to open the error.txt file in your default text editor. The error.txt file captures the results of validating a project file after class and source selection, and in particular points out any duplicate or missing files. For an Ada Project, it includes error messages for the Ada Front End.

### Console Help Menu | top

Select Help and then one of the following Help Menu items for more information.

- SofCheck Inspector Console Help (F1): view this help document.
- SofCheck Inspector User Guide (Alt+U): view the SofCheck Inspector User Guide.
- About SofCheck Inspector Console (Alt+A): view an About dialog box with version information about SofCheck Inspector and the Console.

### How to View SofCheck Inspector Output | top

#### Browser Requirements | top

The output of SofCheck Inspector may be browsed via recent versions of Internet Explorer, Netscape Navigator, Mozilla, or Firefox. Verify that your browser's security level is set to enable JavaScript, to allow popup windows, and to allow the JavaScript to raise and lower windows (see below).

On more recent versions of Internet Explorer, you will need to allow windows to use active content (i.e. JavaScript) by going to Tools->Internet Options->...Advanced, scrolling down to the Security check boxes, and checking the box that says "Allow active content to run in files on My Computer".

On more recent versions of Firefox, you will need to allow JavaScript to raise and lower windows. This is done by going to Tools-->Options-->Content-->Advanced button next to the Enable JavaScript (which should be checked also), and then making sure that the "Raise or lower windows" box is checked.

#### Location and Format of Output | top

  SofCheck Inspector's output is generated in the Output_Directory. Output is generated in two formats, both of which preserve the Ada package/source file hierarchy. The recommended format is HTML, suitable for display by a browser. It is produced under the html subdirectory of the Output_Directory. A more traditional interleaved source and inspection message listing is produced under the list subdirectory of the Output_Directory. The contents of the list subdirectory may be displayed with any ASCII text viewer.

  To look at the output, point your browser at html/index.html, in the Output_Directory.

  #### Back and Forward Buttons | top

  The back button (<<) and forward button(>>) are located in SofCheck Inspector's titlebar. Use these buttons to navigate through the command history associated with the large right panel of the main window. These buttons will work more predictably than the browser's built-in back and forward buttons, because of the multi-frame user interface provided by SofCheck Inspector. The browser's built-in back and forward buttons work fine with the other windows (Message History, Race Conditions, Module List, and Help windows).

  #### Main Window | top

  The Main Window is composed of up to four panels, with a titlebar across the top. The Partition panel in the upper-left panel contains a list of the partitions into which the Inspector has broken up the system for more efficient analysis. Click on All Partitions to display all directories and files, or click on a named partition to filter directories and files to those inspected within that partition. The Partition panel will not be present if the inspection was performed as a whole and no partitions are created. The -global command line flag instructs Inspector to avoid making partitions; Inspector may not create partitions if the analysis is small.

  The Directories panel on the left, below the Partitions panel (if your project has partitions), lists all directories in which the Inspector found source code. Click on All Files to list all files associated with all directories in the Files panel, below. If you are viewing only a single partition, click on “Partition n Files” to list only those files within partition n in the files panel. Click on a single directory to list only its files in the Files panel.

  The Files panel on the left, below the Directories panel, lists source files analyzed by the Inspector. A “-” to the left of the file indicates that the file has been dropped since the base inspection; a “+” indicates that the file has been added since the base inspection. Initially, the Files panel shows all of the source files in the system, across directories and partitions. Filter the list by selecting a single partition in the Partitions panel. You may also filter the list by selecting Partition n Files or a single directory in the Directories panel. Click on a file name to view the File Summary, described below.

  In the Main panel on the right, you may click on one of three tabbed views: Inspection Overview, File Summary, and File Source.

  The Inspection Overview view shows the inspection's File Hot Spots, a sorted list of files, those with the most important inspection messages listed first. Importance is ranked according to an algorithm that considers the number, a calculated degree of priority, and newness of inspection messages. In the header, the Current Inspection shows the date and number of the inspection run that generated this output, whereas the Base shows the date and number of the base inspection. The base inspection is a prior inspection against which the current inspection is compared, to determine changes since a prior run.

  For each of the files, a set of columns show the numbers of high, medium, and low probability inspection messages. The higher the probability, the greater the likelihood the indicated line of code would fail when executed. Each probability category has three columns: base, deltas, and now. The base shows the total number of inspection messages that were found in the base inspection in each file. The now column shows the total number of inspection messages that are found in each file for the current inspection. The deltas column shows how many unique inspection messages were dropped and/or added between the base and current inspection in the form dropped/added, e.g. “-2/+5” means that two messages were dropped and five new ones were added. Click on an individual file name to display its File Summary.

  If any of the files have been added (“+”) or dropped (“-”) since the base inspection, the File Hot Spots table will have a “-/+” column to mark the file in this way. Dropped files (i.e., files that were present in the base inspection, but are not in the current inspection) appear at the end of the table, after the files for the current inspection. Clicking on the name of a dropped file will bring you to its File Summary view, but because the file is not part of the current inspection, you will not be able to access its File Source view.

  The File Summary view shows a file's Method Hot Spots, a sorted list of methods, those with the most important inspection messages listed first. As for the Inspection Overview, importance is ranked according to an algorithm that considers the number, a calculated degree of priority, and newness of inspection messages. The following section will list a method summary table for each method that has inspection messages. If there are no inspection messages for the file, there will be no Hot Spots or Method Summary tables. The last section lists all methods, even those with no inspection messages, with links to jump to the source for each method. If a method name has a hyperlink, clicking on it will bring you to the Method Summary table in the File Summary view.

  The File Source view shows an annotated source file listing for the current file. If no source was available for a .class file that was inspected, only the annotations will be displayed. The source is interspersed with preconditions and postconditions, lines with added inspection message indicators (“+” to the left of the line number), and color-coded hyperlinks to the inspection messages. Click on the Precondition/Postcondition indicator (“P/P”) near the top of a method's definition to show a list of all preconditions and postconditions in the bottom view pane.

  Click on a color-coded, hyperlinked line to show the associated inspection message(s) in the bottom view pane. The colors are assigned according to the highest probability message associated with any one line, red for high, yellow for medium, green for low. Each inspection message will show a blank or “+” indicator (“+” indicating this message is new in the current inspection), a message category, a high/medium/low probability indicator, and a detailed text description. Click on Prev Msg or Next Msg to view the previous or subsequent inspection message for the file, respectively. Click on the Edit Icon, the image of a pencil-and-paper to the left of the probability indicator, to open the Per File Message Status Window.

  Click on the Inspection Overview, File Summary, or File Source tabs to alternate between views. Remember to use the << and >> buttons in the Inspector titlebar to navigate back and forward, respectively, between viewed pages. (Avoid using the browser's default back and forward buttons, since they may lose track of your view state information.)

  #### Race Conditions Window | top

  Click on the Race Conditions button in the titlebar to view the Race Conditions report. The button is suppressed if the inspection was performed with the -no-race-conditions command line option. See the section Identify Possible Race Conditions for a description of how to interpret the results of the race condition analysis.

  #### Message History Window | top

  Click on the History button in the titlebar to view the Message History report. This button is visible only if a Database_Dir has been specified in the library file (see above) for the current inspection and the user has not specified the -no-error-history command line option. This report contains a table of the number of messages identified in every inspection, in total and grouped by each directory of sources, since the database was created. Each row corresponds to an inspection. Rows of baseline inspections appear darker.

  At the bottom of the Message History report is a histogram of the total number of errors over time, with one column per inspection.

  Note: for the Message History Report, each message in the database is evaluated relative to the current inspection, the current base inspection, and the current MessagePatterns.xml file. As a result, the message counts for prior inspections may vary from those counts that were reported at the time of the actual inspection.

  #### Module List Window | top

  Click on the Module List button in the titlebar to view a list of all modules inspected in the current run. Click on a module in the left pane, and the right pane will display detailed information on each type or module, its parent type, its derived types, its components, and its subprograms. The primitive subprograms and components of each type inherited from its parent type are displayed using an italic font. Subprograms and components directly defined on a type are displayed using normal font. In the right pane, click on the superclass or a reference to another class to jump to it in the Module List. Procedures with inspection messages will have hyperlinks. Click on a subprogram hyperlink or the source file hyperlink to jump to the File Source view.

  #### Message Status | top

  Click the Messages button in the titlebar to open the Message Status Overview window. This window contains a system-wide summary of the messages organized by Message Category, and again by source file. The Message Status Overview allows you to sort/filter system-wide summaries of inspection messages and to access per-file summaries.

  ##### Message Category Table

  For each row in the Message Category Table, the message count for each category is further broken down by High/Medium/Low probability.

  Uncheck the Select box for a message category to suppress that category from appearing in the Source File Table.

  ##### Source File Table

  Each row in the Source File Table is uniquely defined by source file and message category. The message counts are subtotaled for each category of messages in a source file. As with the Message Category Table, each file-category row has High/Medium/Low probability columns. File-category rows with zero inspection messages are not shown.

  Click on a column header to sort the display by that criterion. Sorting large tables can take a long time. While the sort is being performed, the column header will be highlighted, and a Stop Sort button will appear at the top of the window. You may continue working in other areas of the browser while a sort is running, although performance may be slowed. The Stop Sort button will disappear when the sort finishes. Click on the Stop Sort button to stop a sort before it finishes.

  ##### Navigating to the Per-File Message Status Window

  Click on a Source File Name in the Message Status Overview window to navigate to the detailed message list for that file.

  Alternately, open the detailed message list for a file by clicking on the edit icon which also appears

  - in the bottom pane of the File Source view, preceding each message's probability, and
  - in the top index tab for a selected file, if the file has any inspection messages

  ##### Per-File Message Status Window/Editing Messages

  The Per-File Message Status window provides a detailed, sortable list of messages for a single source file. It also allows you to modify the status of a message, by changing its probability and/or adding comments to it. These changes persist, and will be incorporated into the results of subsequent inspections. Additionally, the complete change history for a message is displayed.

  Note : This message-edit functionality requires that Google Gears be installed on your system. Google Gears is an open source browser extension that enables web applications to provide offline functionality using JavaScript APIs. Google Gears is supported on Firefox 1.5+ and Internet Explorer 6.0+ on Windows Vista/XP. If Google Gears has not been installed and you try to edit a message, a button will be provided for you to Get Google Gears. At that website, simply click the "Install Google Gears" button to download it and run the Google Gears installer. After the installation, you will need to exit your current browser session, and then start a new one, for the message-edit functionality to be available.

  At the upper-left of the window, the Filter Options grid contains checkboxes to control which messages are displayed. for History options, check added to select messages that were not in the base inspection but appear in the current inspection, dropped to display messages that appear in the base but not in the current inspection, and unchanged to display messages that appear both in the base and current inspections. For probability, check High, Medium, and Low to display messages with corresponding current probabilities.

  By default, added, unchanged, and dropped messages are displayed, for High and Medium probabilities; Low probability messages are hidden. You may check a box to show the corresponding messages, or uncheck the box to hide them. The filtering options selected affect all files, not just the one whose messages are currently being displayed.

  Click on any of the hyperlinked column headers to sort by that column, which can be Status, +/-, Msg Id, Method, Line, or Message Category. Sorting columns in this window uses your browser's build-in sorting capability, and may be unresponsive during a sort. Most sorts should complete in a reasonable amount of time.

  The Status column displays the current probability for a message. The Review button indicates that the message has yet to be reviewed, while the Edit button indicates that the message has already been reviewed/modified. Both buttons bring up a popup window through which the user can change the probablity of the message and/or add comments to it. The history of all changes made to the message is also displayed. for a message that has yet to be reviewed, click on the Mark As Reviewed button to confirm the probability assigned by the Inspector; this will also automatically add a comment to the message, with the timestamp of the review.

  Changes which you make during your current browser session will be reflected in the Message Status window and corresponding File Source view; however, they will not be fully incoporated into the output (i.e., in any of the Overview tables, or in the message-status Change History) until the Inspector is re-run. From the Inspector Console, choose the Run->Regenerate Reports menu item to fully incorporate the latest message edits *without* rerunning the analysis engine. This will also pick up any changes made by others on your system who have been examining the same output. (Note : Even if you do not re-run the Inspector, changes that you make in one browser session will be available in subsequent browser sessions. However, the color-coding of source lines in the File Source view (based upon message probability) may not be accurate until the corresponding Message Status window is loaded.)

  The Msg Id column contains Inspector-generated message identifiers used to uniquely identify each inspection message. Click on a Msg Id to jump to the File Source view for that message.

  #### Annotations Report | top

  Click the Annotations button in the titlebar to open the Annotations Report window. This window contains a system-wide summary of annotations per file, with deltas.

  Click on a file to get a detailed view of annotations per subprogram, including some history information, filterable by annotation kind, and whether the annotation is new, unchanged or dropped.

  #### Help Window | top

  Click on the Help button in the titlebar to view this SofCheck Inspector User Guide.

  #### Non-Web Output (list subdirectory) | top

  In addition to the files in the html subdirectory, there are listing files in the list subdirectory of the Output_Directory, each with the suffix .txt. These files contain source listings interleaved with SofCheck Inspector messages. Some of the information in these listings is at a lower-level than that displayed in the browser. We suggest initially viewing the output through the browser interface. The listings may be used for more detailed analysis, if desired.

  The overview.txt file in the list subdirectory provides aggregated message information in a series of tables using comma-separated list format, each intended to be suitable for import into a spreadsheet.

  #### Run-Time Test Vectors

  The Inspector creates a test_vectors.txt file directly in the output directory (as opposed to in the list or html subdirectory). This file contains a report which, for subprograms that have any significant control flow (if/while/for statements), identifies the distinct ranges of values for inputs (or combinations of inputs) that will ensure that each block of code is executed. for example, if the report includes:

        Graph.Util:Get_Value
          X: {0..2}, {3..2_147_483_650}
          X - Y: {-inf..0}, {1..+inf}

  This means that if you want to have run-time tests that exercise all blocks of code in the Get_Value routine in the Graph.Util package, you will need to write tests where there is at least one test that has X in the range 0 to 2, and a separate test where X is greater than 2. Similarly, you will need to write at least one test with X <= Y, and one with X > Y. And to be safe, all combinations of these two alternatives should be tried (leading to a total of at least four tests of Get_Value).

  The Inspector determines these test vectors as a side-effect of its control and data flow analysis of each subprogram. The test vector report can help a project achieve higher coverage in run-time functionality tests to complement the full coverage static error detection tests provided by the Inspector.

  ### Messages and Annotations | top

  SofCheck Inspector output is comprised of messages and annotations. The types of messages and annotations produced are described below. For an overview of SofCheck Inspector's output, refer to the How to View SofCheck Inspector Output section.

  #### Description of Messages | top

  SofCheck Inspector uses static analysis to track possible run-time values of all variables, parameters, and components at each point in the source code. using this information, it identifies conditions under which a Ada run-time check might fail (null pointer, array out of bounds, etc.), an exception might be raised, a user-written assertion might fail, or a numeric calculation might overflow or wraparound.

  The messages that the Inspector emits, when it detects one of the above conditions, are referred to as Check-Related Messages. The Inspector's titlebar displays the Total Checks Analyzed (i.e., the total number of such checks that it performs as part of its static analysis over the entire program), as well as the Total Checks Passed (i.e., the number of such checks that it determines will pass). The Percentage Passed statistic is an important metric to help you track the overall quality of your code, or determine the quality of third-party or outsourced code. Each file's File Summary page will also display the same check-statistics, on a per-file basis.

  Some messages that the Inspector emits do not fall into the Check-Related category. These messages are "suspicious preconditions", as well as the race-condition messages and the code redundancy messages (see below). The Hots Spots tables, in both the Inspection Overview and File Summary pages, display the total error-counts using a breakdown of Check-Related Messages and Other Messages.

  The messages produced by SofCheck Inspector indicate particular lines of source code that could cause a crash or questionable behavior at run time. The reason is given (such as “array index out of bounds”), along with a rough indication (based on heuristics) of the likelihood that this message identifies a defect that could lead to incorrect results in actual usage of the program. Occasionally a message contains too much information to fit conveniently on the screen. In that case the message will be truncated and will be replaced with an ellipsis (“...”) as indication that truncation has occurred. The complete text of the message is available for viewing in the corresponding .txt file.

  #### Caveat: Messages and Ada indexed components

  Within the adajava preprocessor, all Ada array declarations are converted into zero-based arrays. In addition, all multidimensional Ada array declarations are converted into one-dimensional arrays. Inspector messages which refer to indexed components will retain the Ada source name of the array object, but the indexing expressions will appear in the message using square brackets, and the computation of the single array index expression will be visible in the message.

  As an example, consider the following Ada code which declares a one-dimensional array type, Arr_1D, a one-dimensional array type, ZArr_1D, and a two-dimensional array type, Arr_2D. An Inspector message which refers to the Ada indexed componnet A1D(I) will appear as A1D[I-23]. (The index expression I-23 computes the zero-based index.) An Inspector message which refers to the two-dimensional Ada indexed componnet A2D(I,J) will appear as A2D[(I-23)*10 + (J-223)].Since the array Z1D(I) is already zero-based and one-dimensional, Inspector messages which refer to indexed components of Z1D(I) will not have their indexing expressions adjusted, but the Inspector message will also use square brackets for indexed components of Z1D(I).

         I,J: Integer;
         type ZArr_1D is array( 0..9 ) of Integer;
         type Arr_1D is array( 23..32 ) of Integer;
         type Arr_2D is array( 23..32, 223..232 ) of Integer;
         A1D : Arr_1D;
         A2D : Arr_2D;
         Z1D : ZArr_1D;

  These are the messages produced by SofCheck Inspector. NOTE: CWE refers to the Common Weakness Enumeration, a community-developed dictionary of common software weaknesses, hosted on the web by The MITRE Corporation. The numbers following CWE are the indices into the CWE dictionary, for weaknesses that correspond to the given Inspector message.

  Inspection Messages
  Message | Description
  array index out of bounds | Index value could be outside the bounds of the array (CWE 124, 125-127, 129, 130, 131, 132, 135, 193).
  null dereference | Attempting to dereference an access value that could be null (CWE 252-253, 476).
  precondition failure | A subprogram call that might violate the subprogram's preconditions. NOTE: in the message in the frame at the bottom of the window, the precondition being checked is expressed in terms of the variables of the called subprogram, rather than the calling subprogram. this means that it is wise to click on the link provided to view the preconditions and local parameter names of the called subprogram, and then click the Back button ("<<"), before trying to understand in what way the caller might be violating the precondition. See Description of Annotations, below, for more information on preconditions.
  divide by zero | Second operand of a divide or mod operation could be zero (CWE 189).
  raise exception | An exception is being raised on a reachable path.
  conditional raise | An exception could be raised depending on the outcome of a conditional test or assertion in the code.
  overflow | A calculation may overflow the bounds of a numeric type and wrap around. The likelihood this will affect operation of the program depends on how narrow is the range of the numeric value (CWE 128, 190-192, 197).
  out of range | Indicates that an Ada Constraint_Error could be raised, due to a Range_Check.
  incorrect variant | Indicates that an Ada Constraint_Error could be raised due to a Discriminant_Check. this may occur when a component is referenced that is not the current variant.
  use of default init | The code is relying on the default initialization of an object to zero or null. (An explicit initialization to zero or null would not produce this message.) (CWE 232, 236, 475)
  call too complex; analysis skipped | Indicates that the Inspector skipped analyzing the subprogram call to avoid exhausting resources needed for analyzing the remainder of the system. The Inspector will report any presumptions it makes about the results/effects of the otherwise unanalyzed call. These should be reviewed to be sure they are appropriate.
  subprogram not available; call not analyzed | Indicates that the Inspector cannot analyze the call because the called subprogram is not available. There are two possible reasons for this: the .class file for the called subprogram is not supplied in the library file, or the called subprogram is analyzed in a different partition. The Inspector will report any presumptions it makes about the results/effects of the otherwise unanalyzed call. These should be reviewed to be sure they are appropriate.
  subprogram fails for all possible inputs | Indicates that a run-time problem is likely to occur on every execution of the subprogram.
  subprogram does not return | The subprogram will never return, presumably because of an infinite loop.
  suspicious precondition | The precondition has a form that indicates there might be a problem with the algorithm. if the allowable value set of a given input expression is not contiguous, that is, there are certain values of the expression that might cause a run-time problem inside the subprogram in between values that are safe, then this might be an indication that certain cases are not being properly handled by the code. In other situations, this might simply reflect the inherent nature of the algorithm involved. In Ada, if there is a precondition on 'First of an unconstrained array requiring that it be, for example, no greater than one, then this is a strong indication that the algorithm is not properly dealing with the case when the array represents a slice that does not start with the "normal" first index (typically one or zero), and where 'Length is not the same as 'Last.
  unused assignment | Indicates redundant assignment. this may be an indication of unintentional loss of result or unexpected flow of control (CWE 563).
  dead code | Indicates logical errors as the programmer assumed the unreachable code could be executed (CWE 561).
  test always goes same way | Indicates redundant conditionals, which could flag logical errors (CWE 561).
  test always goes same way (T) " | Same as above, with an additional indication that the test always evaluates to true.
  test always goes same way (F) | Same as above, , with an additional indication that the test always evaluates to false.

  #### Race Condition Messages | top

  SofCheck Inspector produces three sorts of race condition messages. See Identify Possible Race Conditions for details on using the SofCheck Inspector to perform race condition analysis. Note that when the Inspector indicates that no lock is held, it actually means that no lock visible to multiple tasks is held. There may in fact be a local lock held. See Identify Possible Race Conditions for more information on the handling of local locks. See above for an explanation of the CWE references.

  Race Condition Messages
  Message | Description
  --- | ---
  unlocked reentrant update | A reentrant external entry point updates a potentially shared object without holding a lock. The message is associated with places where the object is updated in the absence of any lock, or with non-overlapping lock configuration (CWE 366-367, 373-374).
  unlocked shared daemon update | A daemon entry point updates a potentially shared object without holding a lock, and this object is also referenced (read or updated) by some other entry point. The message is associated both with places the daemon updates the object, and places that reference the object outside the daemon (CWE 366-367, 373-374).
  mismatched locked update | An entry point updates a potentially shared object while holding a lock, and this object is also referenced (read or updated) by a second entry point without holding the same lock. Any messages are associated with the second entry point's references (CWE 366-367, 373-374).

  If Inspector indicates a race condition at a particular line in your program, it is best to refer to the Race Conditions report by clicking on the Race Conditions button in the titlebar. The Race Conditions report is organized by the affected object, and gives an overall perspective on how the various task entry points are involved in creating the potential race condition on the given object. See Identify Possible Race Conditions for more information on how to interpret this report. Note that the current release of Inspector does not detect deadlocks between tasks(sometimes called “deadly embraces”). Rather it identifies data objects that are potentially referenced without adequate synchronization.

  #### Categorization of Inspection MessagesCategorization of Inspection Messages | top

  SofCheck Inspector makes conservative assumptions in order to avoid missing potential problems. Because of these assumptions, SofCheck Inspector might generate inspection messages that a programmer would decide are not true problems, or that are problems that would not occur during a normal execution of the program. for example, a given numeric overflow might occur only if the program ran continuously for decades. Inspection messages that are not true problems are called false positives.

  To help deal with false positives, SofCheck Inspector categorizes inspection messages into three levels, according to the likelihood the message corresponds to a true problem. For example, a "divide by zero" error might be categorized as "high." An "overflow" that only occurs near the limits of the maximum long integer value, however, might be categorized as "medium," especially if there are intermediate exit points in the loop that would prevent the overflow. Use of a global pointer variable that is not explicitly initialized might be categorized as "low" because Ada provides well-defined default initial values for all pointers. These levels are determined by matching against patterns provided in a MessagePatterns.xml file. With guidance from SofCheck, this MessagePatterns.xml file may be used to tune the categorization of messages to the needs of a particular project.

  Inspection Message Probabilities
  Probability | Description
  High | High likelihood there is a defect on this line of code. It is likely to cause a problem on every execution.
  Medium | Moderate likelihood there is a defect on this line of code. It may cause a problem on some executions.
  Low | There is a small chance there is a defect on the given line of code. It is worth investigating when trying to eliminate any possibility of incorrect execution.

  The following terms are used to distinguish between different inspections and messages when an historical database is being maintained for a body of code.

  Inspection Message Qualifiers
  Qualifier | Description
  current (now) | A current inspection message is one that appears in the current inspection, regardless of whether it appeared in any prior inspection. if no historical database is being kept, all inspection messages are current. The current inspection is always the inspection currently being viewed though the SofCheck Inspector browser interface.
  new (added) | A new (or added) inspection message is one that appears in the current inspection but not the base inspection. new inspection messages have a "+" indicator in the left column in the File Source view and in the +/- column in the Per-File Message Status Window. If no historical database is being kept, the new designation is not made.
  dropped | A dropped inspection message is one that appears in the base inspection but not in the current inspection. Dropped inspection messages have a "- quot; indicator in the +/- column in the Per-File Message Status window. if no historical database is being kept, no dropped messages will be displayed.
  base (baseline) | A base inspection message is one that appears in the base inspection, regardless of whether it appears in the current inspection. The base inspection is a prior inspection against which the current inspection is compared, in the Inspection Overview. Any Inspection Overview has exactly one base inspection, or none, if no historical database is specified. A baseline inspection is an inspection run with the -baseline run time option. this makes the inspection eligible for being used as the default base inspection for future inspections, in the absence of an explicit -cutoff parameter. There may be many baseline inspections over time, but not all inspections are baseline inspections.
  deltas | The deltas column contains the count of messages dropped (-) and/or added (+) between the base and the current inspection.

  Where an historical database is specified, the Inspection Overview's base inspection defaults to be the second most recent baseline inspection, one run with the -baseline command-line flag. Use the -cutoff flag to override the default base inspection by assigning the inspection ID of an arbitrary inspection to be the base.

  Inspector uses the historical database, the message type, and the line number on which the message is associated to determine whether a base message matches a current message or the current message is new. Each new inspection message is assigned a unique identifier, and that identifier is maintained across subsequent runs. If the source file has been modfied significantly between base and current inspections, Inspector may not be able to determine that a current message matches a base message. In this case it will designate the current message as new. Similarly, if Inspector cannot read the historical database for any reason, it will determine that all current messages are new.

  #### Description of Annotations | top

  SofCheck Inspector generates the following kinds of annotations on each Ada subprogram. See Use Annotations for Code Review below for a discussion of how annotations can be used to aid in source code review.

  - Preconditions specify requirements that the subprogram imposes on its inputs. for example, a subprogram might require a certain parameter to be non-null for proper operation of the subprogram. These preconditions are checked at every call site. A message is given for any precondition that a caller might violate.
    - The notation “init'ed(X)” means that X is expected to be initialized prior to calling the subprogram, but no further requirement is imposed on its value.
    - The notation “(soft)” means that the precondition is associated with code that might not be executed on certain calls to the subprogram, so violating the precondition might be safe under those circumstances. However, violating the precondition on every call would not be wise, as there are values for other inputs that could cause a violation of the precondition to lead to a run-time failure.
    - The notation “base...fld” refers to the “fld” component of any object accessible by following one or more levels of indirection starting at “base,” not including “base.fld” itself. this notation is used to handle iterative or recursive algorithms that walk recursive data structures. for example, in an algorithm that walks a linked list, a possible precondition might be “init'ed(X...next)” meaning that the “next” component of any object reachable from X must be initialized (not including X.next itself—there will be a separate “init'ed(X.next)” precondition if appropriate).
  - Presumptions display what SofCheck Inspector presumes about the results of an external subprogram whose byte codes are unavailable for inspection, or are in a separate partition. There are separate presumptions for each call site, with a string in the form “@<line-number-of-the-call>” appended to the name of the subprogram. Presumptions are not generally used to determine preconditions of the calling routine, but they might influence postconditions of the calling routine. See below for further discussion of presumptions.
  - Postconditions characterize the behavior of the subprogram in terms of its outputs and the presumptions made.
    - The notation “X'in” in a postcondition refers to the value X had on entry to the subprogram.
    - The notation “possibly_updated(X)” is used to convey that X is a possible output, but there is no specific set of values that it is known to have after the subprogram completes.
    - The notation “new My_Type(Subp#N)” refers to the My_Type object created by the Nth allocator within Subp. The notation “new My_Type(Subp#N) <num objects>” refers to the number of times this allocator might be invoked at run-time for each call of the subprogram. if an asterisk (“*”) follows the index (e.g. “new My_Type(Subp#3*)”) then the allocator arises from a nested call on “Subp,” which may represent a recursive call, or simply a nested call on a same-named subprogram.
  - Unanalyzed calls display the external calls to subprograms that the SofCheck Inspector has not analyzed, and so participate in the determination of presumptions. Note that these annotations include all directly unanalyzed calls as well as the unanalyzed calls in the call graph subtree that have an influence on the current subprograms.

  - The following annotations are not present in the .html output but are presented in the more detailed .txt files. However, every Input in a .txt file appears at least once in some precondition in a .html file, and every Output and new Object in a .txt file appears at least once in some postcondition in a .html file.
    - Inputs comprise a list of all variables (parameters, components of objects, global objects) referenced by each subprogram.
    - Outputs comprise a list of all variables (components of objects, global objects, subprogram results) modified by each subprogram.
    - New Objects comprise a list of heap-allocated objects, created by a subprogram, that are not reclaimed during the execution of the subprogram itself; these are new objects that are accessible after return from the subprogram.

  ### SofCheck Inspector Usage Scenarios | top

  SofCheck Inspector ideally should be used early in the development cycle, as soon as there is code that compiles. Thereafter it may be run every day, or as often as there is a build of some part of the system. In general, SofCheck Inspector is best suited to be used during periodic (daily) system builds, with its output made available to all relevant parties. It requires compiled JVM byte codes, but can operate on less than an entire system. Since static analysis does not require running code, SofCheck Inspector may perform its analysis at the point of unit, integration, or system build—even before any run time testing has been performed. By using SofCheck Inspector to find defects before they enter run time testing, it will minimize the number of crashes encountered during testing, allowing functional tests to run to completion and thereby provide usable output for test engineers.

  Various types of users may take advantage of SofCheck Inspector. Here are some examples:

  Software Developer
    Use the File Summary and File Source views to focus on potential problem areas. Review the preconditions and postconditions of your code to ensure conformance with specifications. Review preconditions and postconditions of others' code to ensure you are integrating with it without making unwarranted assumptions.
  Quality Assurance Engineer
    Use preconditions and postconditions to assist with boundary test design. Identify potentially blocking bugs before the effort of setting up complex tests.
  Integrator
    Use the Overview and Total Checks Analyzed/Total Checks Passed statistics to rapidly evaluate the quality of third party or outsourced code. Review Hot Spots to identify areas of concern for your integration—even in the absence of third party source.
  Manager
    Use the Inspection Overview, Hot Spots lists, Total Checks Analyzed/Total Checks Passed statistics, and Message History to monitor codebase health and quality assurance progress.

  The following scenarios illustrate how SofCheck Inspector can be used to:

  - Find Defects in Code
  - Use Annotations for Code Reviews
  - Identify Possible Race Conditions

  #### Find Defects in Code | top

  SofCheck Inspector helps the review of inspection messages by categorizing them into High, Medium, and Low probability, reflecting the descending likelihood that a given message corresponds to a defect that will cause a problem during actual use. In addition, High probability messages are less likely to be false positives, while it is more likely that a Low probability message might correspond to a false positive. When starting to inspect a codebase, we recommend focusing on High probability messages, while initially ignoring Medium and Low probability messages. When High probability messages have been understood or remedied, consider the Medium probability messages. Only those developing mission critical systems might eventually want to systematically review all the Low probability messages. As discussed below, by taking advantage of the Inspector's historical database capability, you can easily identify just new messages that correspond to recently modified code. In addition, since the Message_Patterns file that determines how inspection messages are categorized can be tuned, most users can focus their attention on High and Medium probability messages.

  By specifying a Database_Dir in the Library File, you can request that SofCheck Inspector keep an historical database of inspection messages, to allow it to differentiate messages that appear as added (not present in an historical base inspection, but present in the current inspection), dropped (present in a base inspection, but not in the current inspection), and unchanged (present in both a base inspection and the current inspection). The base inspection is either the most recent inspection (prior to the current inspection) run with the -baseline parameter or a prior inspection identified by the -cutoff parameter in the current run.

  For a library with an historical database, it is reasonable to investigate just the new Medium and Low probability messages rather than reviewing all such messages. There are generally far fewer new messages, and new messages should be related to recent code changes. Therefore, even Low probability messages might be worth reviewing when marked new.

  For inspection messages that are not deemed to be critical errors, revising code to alleviate the identified issue might still be useful, to make the code easier to understand for human readers, and to help make the code less vulnerable to future problems as it undergoes maintenance.

  #### Use Annotations for Code Reviews | top

  Whether it is a formal team process or an ad-hoc, one-person activity, manually reviewing source code is a good way to identify problems early in the development cycle. Unfortunately, it can also be quite time consuming, especially when the reviewer is not the author of the code. SofCheck Inspector reduces the effort required for understanding source code by characterizing the input requirements and the net effect of each component of the code base.

  Specifically, SofCheck Inspector determines preconditions and postconditions for every Ada subprogram it analyzes. It also makes presumptions about external subprograms it calls whose byte codes are not available for inspection, or which are so complex that they threaten to exhaust the available machine resources. SofCheck Inspector displays preconditions, presumptions, and postconditions in its web-based source listings as a Ada comment block immediately preceding the first executable line of the subprogram. if a large number of conditions are found, the display list will be truncated and an ellipsis ("...") substituted for the undisplayed messages. You may display all of the preconditions, presumptions, and postconditions in the bottom pane of the File Source view by clicking on the P/P link at the top of the comment block or on the ellipsis (...) at the bottom of a truncated comment block.

  The preconditions displayed by the Inspector are implicit requirements that are imposed on the inputs to a subprogram, as determined by analyzing the algorithms used within the subprogram. Violating preconditions might cause the subprogram to fail or to give meaningless results. During code review, the reviewer can verify that the preconditions determined by the Inspector for the code as written are appropriate, and meet the underlying requirements for the subprogram.

  Early in a development cycle, system documentation might be missing or incomplete. Since SofCheck Inspector generates preconditions for each module without requiring that the entire enclosing system be available, it can be used before system integration to understand subprograms as they are developed. In a mature, maintained codebase the system documentation might no longer agree with current code's behavior. In either case, SofCheck Inspector's generated preconditions can be used to verify both the written and unwritten assumptions made by the codewriters.

  Presumptions represent assumptions made by the Inspector about the results of a call on a subprogram whose code is unavailable for analysis. A separate presumption is made for each call site to the unanalyzed subprogram, with a string in the form “@<line-number-of-the-call>” appended to the name of the subprogram. Presumptions do not generally affect the preconditions of the calling routine, but they might influence postconditions of the calling routine.

  Postconditions are characteristics of the output which a subprogram could produce, presuming its preconditions are satisfied and the presumptions made about unanalyzed calls are appropriate. Postconditions can help a reviewer understand the purpose and effect of code, even in the absence of other documentation. Likewise, postconditions can be helpful to software developers making use of a subprogram. Comparing postconditions to either preconditions or the context of calling routines can provide valuable insight into the workings of the code which might not be obvious from solely a manual review.

  #### Identify Possible Race Conditions | top

  SofCheck Inspector detects common forms of race conditions. A race condition may exist if there are two or more concurrent tasks that attempt to access the same object, and at least one of them is doing an update. for example, if a Reader task makes a copy of a List Object at the same time a Writer task is modifying the List Object, the copy of the List Object may be corrupt. Languages such as Ada use synchronization or locking as a means to guard against race conditions. SofCheck Inspector identifies race conditions where synchronization is not used or is used incorrectly. (Note that the current release of Inspector does not identify potential deadlocks, also known as deadly embraces, where two tasks are stuck waiting on locks held by the other.)

  A lock is held during any protected subprogram or protected entry call. Any variable that can be accessed by more than one referencing task simultaneously must be locked at every reference to guard against race conditions. Furthermore, the referencing lock should match the lock used by other tasks to prevent updates during access. If locking is absent, or if one reference uses a different lock than some other reference, SofCheck Inspector identifies a possible race condition. Note that an identified race condition is not guaranteed to create problems on every execution, but it might cause a problem, depending on specific run time circumstances.

  Note that if a lock is associated with an object that is newly created each time a subprogram is called, it does not actually provide any synchronization between distinct calls on that subprogram. A lock is only effective if it is associated with an object that is visible to multiple tasks. The Inspector essentially ignores locks on objects that are not visible to multiple tasks, as they have no synchronizing effect. this means that the Inspector may indicate that there are no locks held at the point of a reference to a potentially shared object, even though there are in fact some local locks held. A future release will identify any potential problems associated with local locks more explicitly.

  SofCheck Inspector must understand the tasking structure of the program being analyzed to detect race conditions. There are two types of entry points that are important to race condition analysis: Reentrant entry points and Daemon entry points. A Reentrant entry point represents code that can be invoked by multiple tasks concurrently. A Daemon entry point (also called a singleton) is presumed to be invoked only by a single task at a time.

  Identify reentrant entry points with the -reentrant "module:subp" option on the SofCheck Inspector command line. Use the -daemon "module:subp" to identify daemon entry points. See Command Line Invocation above for the syntax for these options. if no -daemon or -reentrant options are specified, SofCheck Inspector uses a default set of entry points for the analysis, presuming the standard Ada tasking model is used for multi-tasking applications.

  Normally you should specify your own entry points explicitly, unless you have verified that the default entry points include all relevant external entry points, including call backs from external subsystems and interrupt entry points.

  For partitions that include one or more task entry points, an indication of zero detected race conditions ensures that there is no path within that partition from one of these entry points to any of the three kinds of unsynchronized access to shared data objects identified by SofCheck Inspector.

  SofCheck Inspector performs race condition analysis by default. this helps to ensure that potential race conditions are identified early. Locating race conditions with run-time testing can be difficult given that they normally show symptoms only intermittently, or under heavy load. Note that you may use the -no-race-conditions command line parameter to suppress race condition analysis.

  The Race Condition report gives complete details about the shared objects in your program that might be subject to unsafe access. The Race Condition report is divided into three panes. The upper right pane, which runs horizontally, summarizes which subprograms Inspector has determined are daemon-task entry points or reentrant entry points. The narrow pane which runs along the left shows the shared objects that might be involved in a race condition. The third pane, which is the large pane taking up the lower right of the report, has a table that summarizes the kinds of race conditions associated with each object, and then provides further information below, reached by clicking on the name of a particular object. For each shared object there is a summary report and a detailed report. The summary report identifies which entry point is associated with each possible race condition. The detailed report goes further by identifying every reference to the object organized by task entry point, locks held (L1, L2, etc.), and whether it is a read (R) or a write (W) access. A key at the bottom indicates the actual Ada object associated with each lock.

  As mentioned above, the Inspector only concerns itself with locks that are visible to multiple tasks, so an indication of None in the locks held column means no task-visible locks are held. There may be locks associated with locally created objects, but these provide no effective synchronization between distinct tasks.

  See Race Condition Messages for details on the messages produced by race condition analysis.

  ### Pragmatic Limitations of static Error Detection | top

  The most accurate static error detection is possible when the entire program representation is available to SofCheck Inspector. There are two reasons why the entire program might not be available: a portion of the program might simply not be available: perhaps it hasn't been written yet or perhaps it's from a restricted library; the other reason is that SofCheck Inspector might have to partition the program representation into manageable sized partitions.

  SofCheck Inspector performs static error detection by holding in main memory a representation of the entire subsystem being analyzed. It is possible that the subsystem being analyzed is so large that its representation cannot be contained in the memory of the host machine on which SofCheck Inspector is running. SofCheck Inspector automatically divides the system under inspection into partitions that are more likely to be analyzable within the memory constraints of the host machine. A user can override this automatic partitioning process by specifying the -global command line option. This will force SofCheck Inspector to perform a global analysis of all of the code identified in the library.

  Note that it is more likely that a global analysis might run out of memory during the processing of some source file. In that case, the source file is skipped and analysis proceeds as though that file was not present in the library.

  #### SofCheck Inspector Presumptions | top

  Sometimes the entire program is not available to SofCheck Inspector, either because the program source is simply not available for inspection, or because the program was so large it needed to be partitioned. In either of these cases, important information about a subprogram invocation might not be available to SofCheck Inspector at the point of subprogram invocation. SofCheck Inspector will not be able to calculate the preconditions of the subprogram being called and it will not be able to precisely characterize the return value nor the effects of calling that subprogram. Invocations of subprograms that haven't been processed by SofCheck Inspector are referred to as unanalyzed subprogram calls.

  SofCheck Inspector makes presumptions about the return values and other side effects of unanalyzed subprogram calls. The presumptions of each unanalyzed subprogram call are displayed in the subprogram information block of the calling subprogram. The source line number of the unanalyzed subprogram call is shown after an @ sign, and information about its presumed return value or other side effect is displayed.

  The actual unanalyzed call might be directly on the line specified in the presumption (by the @nnn) or it might be a call that occurs inside the subprogram called on the given line. You can tell if it's an indirect call or a direct call by the name given in the presumption. If it doesn't correspond to the name of the subprogram directly called on the given line, then it must be something called indirectly.

  Sometimes the presumptions made by SofCheck Inspector are overly "optimistic", such as a given call will never return a null, when in fact it can return a null. For example, suppose that under some circumstances, an unanalyzed subprogram call can return a null, but that the calling subprogram never checks for this possibility, and instead dereferences the return value without checking. This could cause an exception when the program is run, and implies that the program being analyzed contains a latent defect. If the Inspector makes the presumption that the called subprogram does not return null, then it would not identify this latent defect. for this reason, the programmer should check the presumptions about unanalyzed subprogram calls and verify that they are appropriate.

  Alternatively, the presumptions made by SofCheck Inspector might be "insufficient". For example the Inspector might presume that some unanalyzed subprogram call could return null, when in fact it never does. Later, in some use of the returned value, far away from the unanalyzed call, the Inspector might complain that a possibly-null value is being dereferenced. The original presumption was insufficient in this case, because it didn't match the actual behavior of the unanalyzed call, and thereby led to the complaint. The programmer can eliminate such a complaint by adding code immediately after the point of the call to assert that the returned value is not null. This will cause the Inspector to tighten up its presumption about the unanalyzed call to satisfy the assertion, and the complaints at other points in the code will go away.

  ### Appendix | top

  #### Command Line Invocation | top

  Inspections may be run from the SofCheck Inspector Console, as described earlier , or from the command line. SofCheck Inspector is invoked on the command line as follows:

          inspector[.exe] -lib <library-file>
            [-all | <name> ...]
            [-allow-duplicates]
            [-background | -log]
            [-baseline]
            [-cutoff <inspection_id>]
            [-global]
            [-max-procs ]
            [-messages [ min | normal | max] ]
            [ {-daemon "<module>:<subp>"} ...
               {-reentrant "<module>:<subp>"} ... ]
            [-output-only]
            [-no-race-conditions]
            [-no-error-history]
            [ [-at-file <directory>] ... @<filename> ... ]
            [-quiet]
            [-repartition]
            [-status-codes]

          inspector[.exe] [ -help | -v | -version ]

  #### Command Line Options | top

  -lib <library-file>
    Specify the library file name. The library file is a text file that can be generated by the SofCheck Inspector Console or edited manually with a text editor. If a directory name is given, use the default file name (i.e., inspector.library) in that directory.
  -all
    Run SofCheck Inspector on all modules specified in the library file.
  <name> ...
    Run SofCheck Inspector on all specified names (i.e., module names or .class file names). SofCheck Inspector also processes those modules or files on which the specified names depend.
  -allow-duplicates
    Run SofCheck Inspector in the presence of duplicate source files. By default the Inspector will stop if it found more than one source file to associate with a .class file.
  -background
    Useful when running the Inspector from a script. The output to standard output is minimal, and the Inspector creates a file called "Inspection.log" in the output directory. In addition to status information, this log file contains useful data to help SofCheck diagnose any problems that might occur during the execution of the Inspector.
  -log
    Like -background, this option creates a file called "Inspection.log" in the output directory. However, the Inspector also produces a running indication of its progress on standard output. (The -log option is on by default; it is listed here for backward compatibility.)
  -baseline
    Specify that this inspection is a baseline inspection and that the prior baseline inspection becomes the default cutoff for the base message column.
  -cutoff <inspection_id>
    Specify that this inspection should use inspection_id as the cutoff for the base message column. Refer to the Message History Report in the web-based Inspector output to determine which inspection-ids correspond to which prior inspection dates.
  -global
    In the default mode of operation (-no-global), SofCheck Inspector automatically partitions the source code of the system into groups of files so that SofCheck Inspector can complete the analysis without exceeding the limits of main memory. Subsequent to the analysis of each partition, the output is reintegrated to produce a single set of web-based summaries and listings. The -global option causes Inspector to create a single global partition containing all the source code of the system. This option allows SofCheck Inspector to have more information available for error checking and may allow more errors to be detected, including the detection of more race conditions. The disadvantage of using the -global option is that it may cause the limits of main memory to be exceeded and SofCheck Inspector may have to skip the analysis of some of the larger files in the system.
  -max-procs <num>
    Specify the maximum number of simultaneous processes launched during an analysis. This switch is useful on systems with multiple processors and sufficient memory available to reduce significantly the processing time. The default value of is 1. If -global is specified, then this switch will be ignored.
  -messages [min | normal | max]
    In the default mode of operation (-messages normal), SofCheck Inspector suppresses messages that are based on information that may not be known with certainty, due to, for example, code being unavailable for analysis, or preconditions that are relevant only under some circumstances. The -messages max option causes Inspector to show messages based on uncertain information, which is appropriate once all the messages shown in the default (normal) mode have been reviewed. The -messages min option causes Inspector to show only messages that are the least likely to be false positives.
  -daemon "<module>:<subp>"
    Specify that the named subprogram is the entry point of a daemon task (also sometimes called a singleton). "*" is permitted as first character of module name, or last character of subprogram name, as a wildcard. See the section on Race Conditions for more information.
  -quiet
    Be quiet/terse. Do not display progress information.
  -reentrant "<module>:<subp>"
    Specify that the named subprogram is a reentrant entry point. "*" is permitted as a wildcard, as with -daemon. See the section on Race Conditions for more information.

  Subprograms are identified by prefixing the name of the subprogram with the name of the module in which the subprogram is defined. Wildcard matching of the string providing the module and subprogram name (via the asterisk character) is available at the beginning or end of the specification, for example: "*module:subp(*".

  -help
    Display help file. Running SofCheck Inspector with no options invokes this behavior.
  -v
    Display version information.

  #### Advanced Command Line Options | top

  -output-only
    Generate text and html output without re-analyzing the code. Useful if the MessagePatterns.xml file has been modified, or if you want to use the -cutoff switch to specify a different base inspection ID to compare against the current inspection output, or if you want to change the setting of the -messages option.
  -no-race-conditions
    Suppress analysis and reporting of race conditions. This may result in faster inspections.
  -no-error-history
    If the .library file specifies a database, this option suppresses generating of the Message History report; historical data on messages produced is still maintained in the database. if no database is declared in the .library file, this option is ignored.
  @<filename>
    Specifies an ASCII file containing command-line parameters, one parameter per line, which are passed to SofCheck Inspector. <filename> is located in the current directory or an alternate location specified with -at-file.
  -at-file <directory>
    Directory in which to search for @<filename>. default is the SofCheck Inspector current working directory.
  -repartition
    Force the inspection to recalculate the file sets used in the inspection. By default, Inspector reuses the partition definitions within a project from one inspection to another.
  -status-codes
    By default, a successful inspection will terminate with a status of zero (success). Likewise by default, an inspection will terminate with nonzero status only if an internal error has occurred. However, the Inspector has some additional status codes that may be useful to a user (see Appendix). this option causes these codes to be generated rather than zero to indicate the more detailed result. In particular, when at least one inspection message is generated, a non-zero status will result if this option is specified.
  -version
    Display version information. Output is more succinct than -v.

  #### Return Codes

  When SofCheck Inspector finishes, it returns a return Code according to the following table. Note: return codes 25 and 29 are not generated unless the -status-codes command line option is given.

  SofCheck Inspector return Codes
  return Code | Description
  0 | Inspection completed. No errors found.
  25 | Inspection completed. Some messages were emitted. Note: this return code is generated only if the -status-codes command line option has been given.
  27 | Input Error. Inspection halted before finishing. Likely cause: a corrupt .library, MessagePatterns.xml, or .class file.
  29 | Inspector Internal Error. this is most likely due to exhaustion of host memory. Inspection continued with possible omissions. Review the standard output or log file to determine which files were skipped. Note: this return code is generated only if the -status-codes command line option has been given.
  100 | Inspection Interrupted. Likely cause: the operating system may have terminated the process, as with a "control-C interrupt" or "end process" directive.
  110 | Database Error. Likely cause: Database corrupted. Please contact Technical Support.
  123 or 124 | Inspector Internal Error. Inspection halted before finishing. Likely cause: insufficient memory. Please contact Technical Support.

  #### SofCheck Inspector Library File | top

  Each invocation of SofCheck Inspector requires a library file. The library file is a text file that can be generated by the SofCheck Inspector Console or edited manually with a text editor. The default name of the library file is inspector.library in the current working directory. When running an inspection you can specify a different file with the -library-file (or -lib) command-line parameter.

  Here is an example of a library file and an explanation of its contents:

        OUTPUT_DIR=>
        Output_Dir := "AFL.OUTPUT"="afl.output" ;
        DATABASE_DIR=;
        Database_Dir := "AFL.DB"="afl.db" ;
        MESSAGE_PATTERNS=;
        Message_Patterns := "AFL_MSG_PATTERNS.XML"="afl_msg_patterns.xml" ;

        SOURCE(DIRECTORY=;

        Source(Directory => "SRC"="src" ,=, INCLUDE_SUBDIRECTORIES=Include_Subdirectories => true,=true, FILES=Files => ("*.ADS"=("*.ads" ,"*.ADB"=,"*.adb" ),=), LANGUAGE=Language => TEXT);

        SOURCE(DIRECTORY=Text);

        Source(Directory => "CLASSES"="classes" ,=, INCLUDE_SUBDIRECTORIES=Include_Subdirectories => true,=true, FILES=Files => ("*.CLASS"=("*.class" ),=), LANGUAGE=Language => JBC);

        SOURCE(DIRECTORY=JBC);

        Source(Directory => "AFL.ZIP"="afl.zip" ,=, INCLUDE_SUBDIRECTORIES=Include_Subdirectories => true,=true, FILES=Files => ("*.CLASS"=("*.class" ),=), LANGUAGE=Language => JBC);

  Output_Dir (or Output_Directory)
    The directory in which Inspector output is produced. if a relative path is used, the name is relative to the current working directory when Inspector is run, not relative to where the library file resides. Inspector creates the directory if it doesn't exist, in which case the parent directory must be writable. The Inspection.log file and two subdirectories, html and list, are created in the output directory. See How to View SofCheck Inspector Output for more details on the output produced by Inspector.
  Database_Dir
    The directory in which the historical database is kept. if a relative path is used, the name is relative to where the library file resides. The database is used to persistently store inspection message histories across mulitple runs. The Message History report provides a summary of inspection messages from every use of SofCheck Inspector since the database was created. if this field is not provided in the library file then no information is preserved, no distinction between base and current/now message counts is presented, and no Message History report will be generated.
  Message_Patterns
    The file in which the XML-formatted Message Probability Rules Specification is kept. if a relative path is used, the name is relative to where the library file resides. If the file is not provided, SofCheck Inspector will use a default Message Probability specification. A detailed description of the Message Probability Rules specification is not provided in this document. Contact SofCheck Customer Support if you require more information.
  Source
    This directive specifies the set of files which SofCheck Inspector analyzes. A .library file must contain one or more Source directives. In the case of Ada inspections, at least one Source directive with Language JBC(JVM Bytecodes -- .class files) must be present.

    Note that the current Ada product uses JVM byte codes as an intermediate compiled representation. JVM byte codes are the representation used by Java compilers and certain other compilers that generate code to run on a Java virtual Machine (JVM). The JVM byte code representation is useful because it is well documented and machine independent. Included with the Inspector is an Ada compiler (adajava/adajbuild) that produces JVM .class files as its output. if using the Inspector Console, this step is done automatically after selecting the source files. if not, there is a separate manual provided that explains how to use this Ada compiler. Be sure to provide the "-inspector" flag when invoking adajava or adajbuild to ensure the compiler includes the most possible information in the generated JVM .class files. A future release of the product may use a different compiled representation for Ada.

    Typically, one or more Source directives will specify the JBC (.class) files, and one or more Source directives of Language Text will specify the Ada source files from which the .class files were compiled. SofCheck Inspector automatically matches Ada source files to their corresponding .class files. If a .class file does not have corresponding Ada source, inspection messages will be generated in a tabular format, rather than being interspersed into the corresponding Ada source file. if an Ada source file does not have corresponding .class files, no analysis can be performed on that file since Inspector reads .class files to determine the semantics of the Ada code. You should use the provided Ada compiler (adajava/adajbuild) to generate the .class files for this Ada code if it is desired that it be included in the inspection.

    Directory
      This is the root of the directory tree in which the corresponding input Files reside (see below). If a relative path is used, the name is relative where the library file resides. This allows SofCheck Inspector to be run from various places using the same library file. The “Directory” directive may also specify the name of a .zip archive. In this case, the .zip archive behaves as though it were a directory containing the input Ada source or .class files. Parts of such an archive may be named by simply appending further pathname components after the archive name, such as DIRECTORY=>Directory => “lib/containers.zip/ada/containers”.
      Note: currently, the specification of a nested .zip file (i.e., nested within another .zip file) is not allowed; you must expand the outer archive, and then specify the .zip file as indicated above.
    Include_Subdirectories
      If Include_Subdirectories is true, then Inspector includes all the subdirectories of “Directory” when expanding any wildcards in “Files”. If Include_Subdirectories is not present, its value defaults to false.
    Files
      These are the pathnames of the files to be processed by SofCheck Inspector, relative to the specified Directory. Each must be in double quotes. Conventional “*” wildcard notation may be used -- a “*” matches any number of characters, including directory separator characters (‘/’ or ‘\’). Note that the Files list must be parenthesized, even if there is only one pathname pattern specified.
    Language
      One Language must be specified per Source directive. The language identifiers that are used are:
      JBC
        JVM Bytecode (i.e., the intermediate compiled representation, so-called .class files)
      Text
        textual source files that SofCheck Inspector will use to provide interspersed source listings (i.e. the Ada or other-language source files that were compiled to produce the .class files)

  #### Troubleshooting | top

  A valid license key is required to unlock the full functionality of SofCheck Inspector. The license key is normally installed along with the binary executable as part of the installation procedure. If the license key is invalid or if your license has expired or will soon expire, Inspector will produce a notification message. Please contact SofCheck to obtain a viable license key.

  SofCheck Inspector uses the environment variable SOFCHECK_INSPECTOR to determine the location of the program executable installation directory. Certain predefined support files used by Inspector to generate error messages and other documentation are located in the installation directory. if this environment variable is not set correctly, a warning message will be produced and Inspector will terminate. To remedy this problem, make sure that the SOFCHECK_INSPECTOR environment variable is set to the correct value.

  We strongly suggest that you familiarize yourself with the file ReleaseNotes.txt, in the SOFCHECK_INSPECTOR installation directory (see above). These release notes contain invaluable tips about both running the Inspector and examining its output; known limitations are also described.

  The library file determines which .class files and which source files are available to the Inspector for analysis (see Sofcheck Inspector Library File). if the output produced seems to be missing certain files, check that the library file correctly identifies the directories or zip archives containing the source and .class files, and that "INCLUDE_SUBDIRECTORIES => True" is specified when appropriate. Note that the Files list in a Source directive must be parenthesized, even if there is only one name pattern specified.

  Occasionally, due to deeply nested Java source files, Inspector encounters a host limitation on the length of file names created for Inspector's browsable output. For example, the limit on the PC host is 259 characters. In this case an internal error message will be produced which gives the name of the output file that cannot be created. A possible workaround to this problem is to locate the Inspector library closer to the leaves of the source tree so that the file pathname will fit into the 259 character limitation. Please contact Technical Support for further information.

  #### Frequently Asked Questions (FAQ) | top

  - Q: Will the Console run if I didn't install my LicenseKey.txtfile?
    A:When the Console runs, it will warn if a valid SofCheck Inspector license key is not installed on this machine.

    Press the OK button, and you will be allowed to continue running the Console. Be aware that the features of SofCheck Inspector will be limited. Follow the instructions in the dialog box or contact your software reseller to obtain a current license key. If you have a license key and did not install it during the SofCheck INspector installation process, you need can install it by hand by naming it LicenseKey.txt and copying it into the Inspector installation directory e.g. C:\Program Files\SofCheck\Inspector-2.1

  - Q: Where can I find an audit log of my Console session?
    A:When you create a project, the Console creates the file error.txt in the project directory. The Console writes information to error.txt that might be helpful to SofCheck support. In the Console main window, select Run > Show Project Issues ..., or press Ctrl+I, to open and view the error.txt file.

  - Q: Why are some of the items highlighted in yellow, in the File Selection window?
    A:If a class file lacks debug information, that file and its parent directory are highlighted in yellow. A .jar file containing a class lacking debug information will also be highlighted in yellow. SofCheck Inspector makes extensive use of the debug information in Java .class files, to produce the most readable inspection messages. To generate debugging information, pass the -g option to javac.

  - Q: What does it mean when items are highlighted in red, in the File Selection window?
    A:If an archive contains a nested archive, that archive and its parent directory are highlighted in red. SofCheck Inspector does not analyze nested archives; if any are found, they should be extracted to the file system before running Inspector.

  - Q: Why are there files in the Class Directories that lack sources pane of the File Selection window? do I really need source files?
    A: Although SofCheck Inspector can work with .class files alone, it generates more meaningful data when it can cross-reference the .java source files. Use the Console to select both class files and their corresponding source files. The File Selection window will identify folders containing mismatched sources and class files. Individual mismatched files will be listed in the error.txt file.

  - Q: Why does an information bar complaining about active content appear when trying to display output in Internet Explorer?
    A:On more recent versions of Internet Explorer, you will need to allow windows to use active content (i.e. JavaScript) by going to Tools->Internet Options ...->Advanced, scrolling down to the Security check boxes, and checking the box that says Allow active content to run in files on My Computer.

  - Q: Inspector wants to pop up a window in my browser; should I allow it?
    A:Yes, you should. Inspector relies on window creation in the browser; suppressing pop-up windows may prevent you from accessing some data.

  - Q: using a recent version of Firefox (version 2.0 and above), clicking on a link is not causing the desired window to appear.
    A: On more recent versions of Firefox, you will need to allow JavaScript to raise and lower windows. This is done by going to the Tools->Options->Content, choosing Advanced next to Enable JavaScript, and then making sure that the Raise or lower windows box is checked.

  - Q: Where can I find information about the status of an inspection run?
    A: By default, a text file summarizing the status of an inspection is included in the output directory, in a file called “Inspection.log” this includes error traceback information that can be helpful to SofCheck in diagnosing any tool problems that are encountered during the inspection. Please include it with any error report you send to support@sofcheck.com.

  - Q: I am getting messages from Inspector about files being skipped. What do such messages mean?
    A:The static error detection analysis performed by Inspector is space- and time-intensive, because Inspector tracks the value of all program expressions across all possible execution paths. The present implementation of Inspector holds all this information in main memory on the host machine.

    Certain Ada programs are too large or too complex to analyze within the memory constraints of the host machine. When Inspector detects this circumstance, Inspector will skip analyzing the JVM .class files which are too complex. No annotations or error messages will be generated for these files, and calls to subprograms which were skipped will be analyzed as though the subprogram body were not available. Detailed information about which files were skipped is available in the “Inspection.log” file.

    As an example, certain syntax parsers can be too complex to analyze within the memory constraints of the host machine. The parsing routine will typically contain a loop and deeply nested switch or if-then-else statements with complex conditional expressions. These can introduce a very large number of paths and distinct computations into the program graph, which may bump into the host machine memory limit.
    A future release of the Inspector will make use of disk-based caching to allow Inspector to handle much larger systems without partitioning or skipping.

  - Q: Why does Inspector divide my project into partitions for analysis?
    A:If the SofCheck Inspector reaches the limits of host memory or other resources during its analysis, its default behavior is to skip portions of its analysis. You may notice that some .class files or individual subprograms are skipped during inspection.

    Verify that your paging file size is optimized for your operating system and amount of system memory.

    To minimize the likelihood of running out of memory, Inspector automatically breaks large test cases into "partitions," typically of about thirty to fifty thousand lines of code (KLOC) each. The "-global" flag may be used to override this partitioning, in which case you may see more files skipped during the analysis.

    You can manually partition your code if you so wish. The separate library files created as part of automated partitioning are preserved in the project directory (with names of the form "part-00X-*.library"), and these may be edited as desired to construct your own partitioning scheme. You can also control automated partitioning by increasing or decreasing the default size of each partition with the "-dbg-partition-limit" command-line flag. Please contact support@sofcheck.com for appropriate use of this option.

  - Q: Inspector has produced a postcondition stating "clFuchsia = &new Color(ColorUtils__static_init#13)". What does this mean?
    A:The Ada compiler generates a class initialization subprogram automatically for every class. In this particular case, ColorUtils__static_init is the name Inspector uses for this automatically generated subprogram for module ColorUtils. The global object named clFuchsia is initialized via an allocator. if you examine the Ada source, you should find that the 13th allocator (#13) provides an initial value for clFuchsia. Note that in messages for other subprograms, this same allocator might be referenced, rather than the name of the global object.

  - Q: Inspector is producing a message saying "Duplicate original source file". What does this mean?
    A:Inspector uses the "Source" directives from the library file to find the files that you want processed. Inspector does all its processing from the .class files (with Language => JBC) and uses the Ada source files (with Language => Text) only for the purposes of producing output which interleaves annotations and error messages with the Ada source. For example, if the Language => JBC Source directives identifies a directory containing a file named My_Download.class and that file was compiled from a file called my_download.ada, then Inspector will look for a file named my_download.ada somewhere within the directories identified with Language => Text. The Source directives in your library file may result in Inspector finding more than one file named tsi/my_download.java. When this happens, Inspector doesn't know which file is the correct Ada source for classes/my_download.class. The ambiguity in the library file must be corrected before Inspector will process the files. Alternatively, if it is determined that the files are two instances of the same file, the "-allow-duplicates" flag can be used.

    These are some of the circumstances where Inspector would find two original source files: it could be that the sources are duplicated because the source file is in a specified directory, and is also in a specified .zip file. Or you might have more than one zip archive that include the same sources files. Or it could be that there is a test and a release directory with the same sources and both appear in the zip file, etc. A solution could be to be more specific in the library file by adding a few more levels to the path, or removing the source files from the zip archive, or extracting the sources from the zip files, or combinations of these strategies.

  - Q: Inspector is producing a message saying "Duplicate module name". What does this mean?
    A:Inspector uses the "Source" directives with Language => JBC from the library file to find the .class files that you want processed. this message means that Inspector found two .class files with the same name. this message is a warning and the Inspector will choose to process the first file encountered. The ambiguity in the library file should be corrected. Please read the FAQ concerning "Duplicate original source files" for strategies to correct the ambiguity.

  - Q: There is a message in the Inspector html output saying "No source file available." What does this mean?
    A:Inspector uses the "Source" directives from the library file to find the .class files that you want processed. this message means that Inspector found a .class file to inspect, but could not find the Ada source file corresponding to the class file. When this happens, Inspector will produce tabular output for the subprograms in the .class file, rather than an interspersed listing. The “P/P” links are provided as a way to view the pre- and postconditions for each method.

  - Q: In the File Source window, some of the lines of my Ada program appear in italics. What does this mean?
    A:A source line that is displayed in italics contains a call to a Subprogram that the Inspector was unable to analyze. if you click on the italicized line, further details will be displayed in the scrollable message area at the bottom of the Main window. There are two messages that cover this situation:
    - subprogram not available; call not analyzed
    - call too complex; analysis skipped
    A future release of the Inspector will make use of disk-based caching, to allow Inspector to handle much larger systems without partitioning, as well as more complex systems without skipping.
    Note that calls to subprograms in the Ada run-time system are normally not analyzed, but do not appear in italics to avoid cluttering the listing. In all cases of unanalyzed subprograms, the Inspector will report any presumptions it makes about the results or side-effects of the otherwise unanalyzed call. These should be reviewed to make sure they are appropriate.

  - Q: When I scroll the File Source display to the last line of the source file, I see an HTML-link for “Other Messages”. What does this mean?
    A:The “Other Messages” link indicates that the Inspector has generated messages for line numbers that are not within the range of the source file being displayed. There are several possible reasons for this:
    - The .class file contains code that originated from some other source file (typically the package specification, a subunit, a generic instantiation, or an inlined call). A current limitation of JVM .class files is that at most one Ada source file may be associated with a given .class file. The JVM byte codes associated with Ada package specifications with dynamic elaboration, subunits, generic instantiations, and inlined subprogram calls, may all end up in the same JVM .class file as the JVM byte codes associated with the Ada package body. Because only one file may be recorded in the JVM .class file as the origin of the byte codes, typically it is the library unit package body that is identified. Messages associated with byte codes originating from other source files end up as Other Messages.
    - The Ada source file does not “match” the .class file. this could occur if the Ada source file was edited but not recompiled, so the .class file is out-of-date. Or perhaps the Inspector chose the wrong Ada file to associate with the .class file (refer to the product's release notes for more details).
    - The code uses a preprocessor, which may cause JVM bytecodes (and, therefore, Inspector messages) to be associated with unusual places in the source file, such as just past its end.

  - Q: Is there a way to focus on inspection messages that have appeared since a prior inspection?
    A:An XML-based database tracks inspection results over time. By specifying a directory for the database in the library file, and giving the “-baseline” command line flag on inspections of regular nightly or weekly builds, the database can be used to help highlight messages that are added or dropped since a base inspection was performed. Click here for more information on how to understand the Inspector's historical viewpoint for messages; additionally, refer to the Message History Window section.

  - Q: How can I quickly see the most serious errors in my program?
    A:The Inspection Overview shows the inspection's “File Hot Spots”, with those files containing the most important inspection messages listed first. Importance is ranked according to an algorithm that considers the message count, the calculated degree of priority, and the newness of the messages. In addition, each file's File Summary contains a “Hot Spots” table for its subprograms.

  - Q: How can I tell if the overall quality of my code is improving?
    A:An overall score card is provided in the upper right corner of the main output window, which indicates the total number of checks performed by Inspector on the analyzed code, and the number of checks that were proved to succeed under all possible inputs. Any checks that cannot be proved to succeed in all conditions result in messages, which are categorized in the various tables, and interspersed into the source listing. Typically Inspector performs one to three checks per line of source, thereby providing a significant level of validation on the logical consistency of the code.

  $Revision: 1.58 $ | top