14. Appendix

14.1. Inspector Reference

14.1.1. How Does Inspector Work?

At its heart, Inspector's technology is most like a whole-program "optimizer": it uses extended versions of algorithms familiar to those writing compiler optimizers. First, a conventional compiler front end is used to convert the program into a treelike intermediate language, called "SCIL" (Statically Checkable Intermediate Language). Then, the Inspector "engine" takes over and begins with a global aliasing analysis followed by translation of each subprogram into a static single assignment (SSA) representation and then a global value numbering over the subprogram. At this point, most compiler optimizers would begin the process of generating code. Inspector instead begins the process of determining whether the program might violate any run-time checks or user assertions and whether the algorithms have any "race conditions" or security "holes."

Inspector analyzes each subprogram separately, by taking into account only the information computed for callees of the subprogram. In particular, the analysis of a subprogram does not depend on its callers. To perform this analysis, Inspector, using the global value numbering, determines the possible value set for every variable and expression appearing in the program at every point where it appears. It uses this information to determine where checks or assertions might fail and also uses it to determine the "preconditions" and "postconditions" of every subprogram. The preconditions represent what must be true about the inputs to the subprogram for the subprogram's algorithm to operate without overflowing or failing a run-time check. The postconditions represent what is true about the outputs after the subprogram completes, presuming that the inputs satisfied the preconditions.

Once the pre- and postconditions for a subprogram have been determined, they can be propagated to every point where the subprogram is called, iterating as necessary in the presence of recursion, until the whole program has been analyzed. Once this process stabilizes, a final pass is performed to report any potential run-time or assertion failures, race conditions, or security holes that exist anywhere within the program. During that pass, Inspector may generate error messages whenever a caller could violate the precondition generated for a callee to guard against an error in the callee. As a result, an error may not be reported by Inspector at the point where there is a fault in the program, but rather at the point where this fault results in an inconsistency. Reviewing the preconditions at this point allows identifying whether the caller or the callee is the culprit by matching the preconditions generated by Inspector and the expectations of the programmer. Reviewing the preconditions generated by Inspector is another way of detecting errors before they occur in the program.

The Inspector technology is fundamentally a "bottom up" approach, which provides excellent scalability. The complexity of the analysis is not dependent on the number of paths in the call graph but rather merely on the number of subprograms in the graph, with a factor based on the amount of recursion. The technology is also very precise, in that the pre- and postconditions for every subprogram include information about all inputs and outputs, including all global variables and objects reachable through chains of pointers. This precision helps to reduce the false-positive rate while at the same time avoiding false negatives.

The book Static Analysis of Software: The Abstract Interpretation, published by Wiley (2012), contains a chapter on the mathematics underlying the inner working of Inspector.

14.1.2. Partitioning of Analysis

When analysis a large set of sources and depending on how much memory is available, Inspector may decide to split the analysis into multiple partitions, consisting of a subset of the sources.

The partitioning is done based on the following criteria:

1. When using Inspector's -global switches, the analysis is always done globally, with a single partition.

2. Otherwise, based on the size of the sources the analysis may be split into multiple partitions. This is done using a call-graph based analysis which attempts to minimize the number of cases where a caller and a callee are assigned to different partition elements. The default size of partitions is set per level to use a certain maximum amount of memory:

   Level	Memory limit per partition
   1	1GB
   2	3GB
   3	4GB
   4	Unlimited

   This can be further tuned via Inspector's --partition-memory-limit switch, e.g. --partition-memory-limit 8GB.

Each partition is saved in a file called part-xxx-of-project.library where xxx is the partition number (e.g. 001, 002, etc...).

For subsequent analysis, the previous partition files - if found - are reused from one run to another, except that files no longer present in a new run are removed, and new files are appended at the end of the last partition, or in a new partition if the last partition was already full.

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, unless memory is really stressed too far, in which case the entire analysis may fail.

There is also a switch --project-partitions which is provided. With this switch, in deep analysis mode, at least one partition is created for each project file (.gpr) in your project hierarchy, assuming you are using more than one project file. In other cases (fast analysis mode or a single project file), this switch is ignored. Specification of --project-partitions is not usually recommended unless partitioning compatibility with older versions of Inspector is desired, or if you want to manually influence Inspector's partition selection algorithm. When this switch is used, the partition files are regenerated after each run (as opposed to being reused run after run).

Finally, the optional switch --simple-partitions disables partitioning algorithm based on a call-graph analysis and assigns source files to partitions based on an alphabetical order.

14.1.3. Inspector Limitations and Heuristics

The most accurate static error detection is possible when the entire program representation is available to 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 Inspector might have to partition the program representation into manageable sized partitions.

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 Inspector is running. Inspector automatically divides the subsystem being analyzed into partitions that are more likely to be analyzable within the memory constraints of the host machine. See Partitioning of Analysis for more details on how Inspector decides to partition an analysis.

14.1.3.1. Evaluation Order

Inspector assumes that arguments of calls are evaluated in left-to-right order. In practice, compilers are allowed to choose any evaluation order for arguments of calls. GNAT in particular may evaluate call arguments in different orders depending on the target platform. If the order of evaluation matters for the side effects of the call, then Inspector analysis may not be sound with respect to the behavior observed when executing on the target.

14.1.3.2. Inspector Presumptions

Sometimes the entire program is not available to Inspector, either because the program source is simply not available, 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 Inspector at the point of subprogram invocation. 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 Inspector are referred to as unanalyzed subprogram calls.

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 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 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 Inspector might be "insufficient". For example 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, 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 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. For example:

Result := Call_To_Unknown_Function (...);
pragma Assert (Result /= null);

If you do not like Inspector's default handling of presumptions, you can disable this behavior via the --no-presumptions switch.

14.1.3.3. Handling of Generic Units

Inspector does not analyze generic units per se, since it doesn't have sufficient context in order to perform a precise enough analysis of the generic code (since it is dependent on its generic parameters which can change significantly the code generated).

Instead, Inspector analyzes each instantiation of generic units. This means in particular that if you do not instantiate a generic unit, it won't be analyzed. In addition if there are multiple instantiations of a single generic unit, Inspector will analyze each instantiation separately. Note that this is supported by Inspector, but in general not by the other analysis engines. For example, this is not yet supported by Infer as described in the section Configuring Infer.

Any messages generated during the analysis of one instantiation might very likely be similar or identical to those generated for other instantiations. The net effect is that there may be multiple similar messages associated with a single line in the source listing for a generic unit.

In addition, when using e.g. the --no-subprojects switch (analyze only sources from the root project), since instantiations are analyzed in the context of the client code (where the instantiation is located), you will get an analysis and potentially messages related to source files located outside the root project.

14.1.3.4. Loop Unrolling

In some cases, Inspector may decide that it is worthwhile to unroll a loop when generating the SCIL representation of the loop. For example, given Ada source code

for I in 1 .. 3 loop
   A (I) := I * 100;
end loop;

Inspector might (or might not) choose to represent this in the generated SCIL as something more like

A (1) := 100;
A (2) := 200;
A (3) := 300;

In most cases, this sort of thing is an internal implementation decision which the user need not be aware of. However, Inspector might then go on to emit messages which pertain to one specific iteration of the loop (or, as is discussed later, to iterations other than the first iteration). In such cases, Inspector will include additional text in each message in order to unambiguously identify the subject of the message. This additional text may take either of two forms. In the case of a for loop (or of an implicitly looping construct such as a quantified expression) with static bounds for which Inspector decides full unrolling is desirable, text such as "(iteration 3 of 5)" would be included. In the case of a loop for which only the first iteration (or perhaps only some part of the first iteration, such as the initial test condition evaluation for a while loop) is unrolled, text such as "(initial iteration)" or "(subsequent iterations)" would be included. In either case, such additional text refers to the nearest enclosing loop (or implicitly looping construct).

For example, given the subprogram

function Foo return Integer is
   type Vec is array (1 .. 3) of Integer;
   Nums : Vec := (1, 2, 3);
   Dens : Vec := (-1, 0, 1);
   Result : Integer := 0;
begin
   for I in Vec'Range loop
      Result := Result + (Nums (I) / Dens (I));
   end loop;
   return Result;
end Foo;

Inspector generates the message:

foo.adb:8:38: high: divide by zero (Inspector): check fails here: requires Dens(I) /= 0 (iteration 2 of 3)

In order to decide whether or not to unroll a loop, Inspector uses some heuristics and in particular limits the number of generated statements after unrolling. This limit is 128 statements by default, and can be changed by setting the environment variable CODEPEER_UNROLL_LIMIT to a lower or greater value. Setting this environment variable to 0 will in effect disable loop unrolling. Note that this setting is taken into account when generating SCIL files, so you need to force generation of the SCIL file after enabling it, by e.g. using the GNAT SAS menu GNAT SAS>Advanced>Remove SCIL

14.1.3.5. Calls to Unknown Subprograms

If Inspector encounters calls to subprograms whose body is not available (e.g. imported from another language, or a runtime call not known to Inspector), it will report such calls as part of the info messages.

Unless the --no-presumptions switch is used, Inspector will generate presumptions (see Inspector Presumptions) for each call to unknown subprograms that might need to be reviewed for accuracy. When using --no-presumptions, no such presumptions are generated, at the expense of potentially more false positives.

14.1.3.6. Skipped Subprograms or Files

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, it will skip analyzing the subprograms or files which are too complex. No annotations or error messages will be generated for these subprograms or 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 info messages and may also be found in the low level Inspection.log file when the switch --dbg-on limitations is given.

This kind of limitation is inherent to static analysis, and as for calls to unknown subprograms, calls to these skipped subprograms need to be reviewed manually instead.

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.

If you want Inspector to analyze these subprograms, you can try one of the following solutions:

• increase the number of steps: by default the number of steps for each subprogram is limited to 30 in fast analysis mode, and 1000 in deep analysis mode. You can increase this value by using the --steps switch.

  Note that an exception is made for elaboration procedures, whose analysis is very important in practice. (An analysis failure for an elaboration procedure means that the analysis for the entire module is abandoned.) Consequently, such subprograms are given thrice as many steps as the other ones.

• increase the amount of memory available on your machine: in case of a memory error reported by Inspector, runing on a machine with more main memory should help analyze complex subprograms.

• increase the maximum number of values computed: in case Inspector reports a too many value numbers in Inspection.log (when the switch --dbg-on limitations is given), then you might want to use the debug switch --dbg-vn-limit with a value above 100000, e.g: --dbg-vn-limit 150000. If this is not sufficient, you will need to simplify your subprogram, see below.

• simplify your subprogram: when Inspector reports an inability to analyze a subprogram, it often means that the subprogram is too complex to be analyzed, and should be split into multiple, simpler subprograms which Inspector can analyze separately.

Note that increasing one of the above limits may well run into another limit due to the inherent complexity of these subprograms (e.g. going from a "too many value numbers" limit to a steps limit, to an out of memory limit.

In general our recommendation is to either analyze such complex subprograms manually and let Inspector skip them, or alternatively refactor your code as mentioned above by e.g. splitting it into multiple simpler subprograms.

Since Inspector's analysis is modular, the rest of the code will still be analyzed and produce useful and relevant results.

14.1.3.7. Call Too Complex

When Inspector analyzes a call to a subprogram, it can hit two different kinds of limits. If one of these limits is hit, Inspector will analyze the call as if there were no body available.

If you want Inspector to analyze these calls, you can try to increase the limit. If the switch --dbg-on limitations is given, Inspection.log file contains messages about which limit is hit. By looking for call too complex in a line, you can see two different kinds of limits:

• in the case of hitting the too many possible call targets limit, it means that there are too many targets for a dispatching call or call through an access-to-subprogram value. You can increase the maximum number of targets with the debug switch --dbg-call-target-limit <limit>.

• in the case of hitting the too many obj-ids to import limit, you can increase the limit using debug switch --dbg-obj-ids-import-limit <limit>.

14.1.3.8. Dispatching Calls and Access to Subprograms

When Inspector encounters a dispatching call or a call via an access to subprogram variable, Inspector attempts to identify all possible such target calls by considering all the compatible primitive operations (or subprograms whose address was taken and whose profile is compatible in the case of an access to subprogram object). By default, the effect of these calls is taken into account in the caller, but the preconditions for these multiple targets (which may correspond to subprograms that cannot be called at this point) are ignored, to avoid an undue number of false positives. The net effect is that Inspector may not report certain possible precondition failures for multi-target calls.

When --messages max is used, then Inspector checks that the preconditions of all targets are satisfied at the point of call.

14.1.3.9. Null Array Bounds

In most cases, Ada requires that the high and low bounds of an index constraint for an array must belong to the corresponding index subtype of the array type. For example, because Standard.String is declared as:

type String is array (Positive range <>) of Character;

both bounds of an object or value of type String will usually be positive. There is an exception to this rule in the case of an array which has no elements because the low bound is greater than the high bound. In this case, values outside of the index subtype are permitted. It is not at all unusual to see high bounds outside of the index subtype, as in:

X : String(1 .. 0);

and Inspector handles this case. It is much more unusual to see low bounds outside of the index subtype, as in:

Unlikely  : String (-10 .. -20);

It happens that the possibility of an out-of-index-subtype lower bound significantly impairs Inspector's analysis in some cases that do commonly come up in practice. In order to pragmatically deal with this situation, Inspector will, in some cases, treat an out-of-index-subtype lower bound as an error. An array declaration such as the "Unlikely" example above will elaborate without raising any exception, as specified by the Ada language definition. Inspector, however, may treat it as an error. More importantly, in cases where the bounds of array are not known (e.g., a subprogram with a parameter of an unconstrained array subtype such as String), Inspector may assume for purposes of its analysis that the low bound belongs to the index subtype. Given the following example:

procedure P (X : String) is
   First_Is_Positive : Boolean := X'First > 0;
   Last_Is_Positive  : Boolean := X'Last > 0;

Inspector will assume that the local variable First_Is_Positive is initialized to True, whereas it knows that Last_Is_Positive might be False if X'Length = 0.

14.1.3.10. Handling of 'Valid

Inspector interprets X'Valid as X being in the range of its subtype if the declared range is static and if the subtype does not have any subtype predicates. X'Valid is interpreted as an unknown call in other cases.

Given the following example:

procedure P1 (X : Positive) is
begin
   if X'Valid then
      pragma Assert (X > 10);
   end if;
end P1;

Inspector interprets X'Valid as X in 0 .. 2**31-1. Since for an IN [OUT] parameter of a given subtype, Inspector assumes that the parameter is in its statically declared range, the code above will generate a test always true message and a precondition X > 10. Since such messages concerning 'Valid are in general not useful, Inspector suppresses them unless --messages max is used.

Given the following example:

subtype Even is Integer
   with Dynamic_Predicate => Even mod 2 = 0;

procedure P2 (X : Even) is
begin
   if X'Valid then
       pragma Assert (X > 10);
   end if;
end P2;

Inspector interprets X'Valid as an unknown call. It thus does not know anything about its result and cannot generate a precondition for the assertion. This means that Inspector will emit a message about the potentially failing assertion.

Inspector emits a high-ranking message if the prefix of 'Valid is known to be uninitialized. No message is emitted in the case where the prefix of 'Valid only might be uninitialized, unless --messages max is used.

14.1.4. Advanced Inspector Command Line Switches

14.1.4.1. Advanced Inspector Switches

As described in Analyzer package attributes, these switches should be specified with the for Switches ("inspector") attribute of the project file.

• --additional-patterns <file>

  When present, this file will be merged with MessagePatterns.xml

• --daemon "<package.subp>"

  Specify that the named subprogram is the entry point of a daemon task (corresponding to an Ada task).

  Subprograms are identified by prefixing the name of the subprogram with the name of the package 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: "*package.subp*".

  See Race Condition Messages for more information.

• --dbg-vn-limit <num_vns>

  Specify maximum number of "value numbers" allowed during Inspector analysis of a single method/subprogram. See section Skipped Subprograms or Files for more information.

• --dbg-call-target-limit <limit>

  Specify maximum number of targets for a dispatching call or a call through an access-to-subprogram value. For Inspector analysis only. See section Call Too Complex for more information.

• --dbg-obj-ids-import-limit <limit>

  Specify maximum number of "obj-ids" to import from a callee to the caller. For Inspector analysis only. See section Call Too Complex for more information.

• --message-patterns <file>

  Specify an alternate MessagePatterns.xml file.

• --method-memory-size <megs>

  Specify the maximum memory size in MB to be used by Inspector for analyzing a single method/subprogram. By default, Inspector allocates a maximum of 1/3 of the amount of physical memory on the system to analyze an individual subprogram, to limit memory explosions in some corner cases. For very complex subprograms, this limit may not be sufficient and may be bumped via this switch. See section Skipped Subprograms or Files for more information.

• --method-timeout <seconds>

  Specify the maximum time spent, in seconds, by Inspector to analyze a single method/subprogram, to avoid spending too much time analyzing very complex subprograms. The default value is set to 600 (10 minutes) in fast mode and 1800 (30 minutes) in deep mode. Note that you should in general use the --steps switch instead.

• --steps <num>

  Specify the maximum number of steps for allowed before stopping Inspector's analysis of a method/subprogram, to avoid spending too much time analyzing very complex subprograms. The number of steps is calculated deterministically, which means that it will be the same for each run with the same analysis, regardless of the platform's speed. See section Skipped Subprograms or Files for more information.

• --partition-memory-limit <GB>

  Specify the maximum memory that should be used for each partition of Inspector analysis, in gigabytes. The optional suffix GB may be used explicitly, for example: --partition-memory-limit 8GB or simply: --partition-memory-limit 8

• --no-preconditions

  Do not propagate checks as implicit preconditions during Inspector analysis. This generally means that code within a subprogram that would be identified as a check will not be promoted as a precondition of the subprogram, typically resulting in messages flagged on lines corresponding to the checks rather than flagged on calls. As an exception to implicit precondition suppression, checks that inputs to subprograms (parameters and referenced globals) are initialized will still be propagated as preconditions, because flagging all uses of inputs would result in too many false-positive messages. In addition, any user-defined preconditions will remain as preconditions and be taken into account on calls. See also --no-propagation below.

• --no-presumptions

  Instruct Inspector to not generate any presumptions for unanalyzed subprogram calls. Use of this switch will generally result in additional messages being reported in the vicinity of unanalyzed calls, since assumptions about the result of such calls are no longer made.

• --no-propagation "<package.subp>"

  Instruct Inspector to not propagate checks as implicit preconditions for subprogram "package.subp." This is the same as --no-preconditions, but limited to the named subprogram, which might be a top-level operation for which it is not appropriate to presume the inputs will conform to any non-explicit precondition. The "--no-propagation <package.subp>" switch may appear multiple times, to suppress precondition propagation for more than one subprogram. An asterisk ('*') character may appear at the start or end of the name to indicate a wildcard match.

• --no-race-conditions

  Suppress analysis and reporting of race conditions in deep analysis mode. This may result in faster analysis.

• --project-partitions

  Create partitions based on the project hierarchy. See Partitioning of Analysis for more details.

• --simple-partitions

  Create partitions based on an alphabetical order of package names. See Partitioning of Analysis for more details.

• --reentrant "<package.subp>"

  Specify that the named subprogram is a reentrant entry point (corresponding to an Ada task type).

  Subprograms are identified by prefixing the name of the subprogram with the name of the package 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: "*package.subp*".

  See Race Condition Messages for more information.

14.1.5. Format of MessagePatterns.xml File

MessagePatterns.xml is a file to control the output of Inspector. Internally, Inspector generates a number of messages, each with a message text and ranking set to Low (see the section about ranking below). With MessagePatterns.xml, one can change the ranking of a message from Inspector or even suppress the message. You can either modify the file that is part of the GNAT SAS installation, or better specify a project-specific file or (preferred when possible) specify an additional project-specific file which comes in addition to the predefined file, see Analyzer package attributes.

Note that a simpler way to filter out messages based on message categories is via the --show command line switch.

14.1.5.1. Structure of the File

The file MessagePatterns.xml is simply a list of rules. The structure is the following:

<?xml version="1.0"?>
<Message_Probability_Rules>
   <!--  the list of rules here -->
</Message_Probability_Rules>

Each rule consists of two parts: a pattern and a target ranking. The pattern describes the type of message that this rule matches. The target ranking is the new ranking of the message as it will appear in the GNAT SAS output. In the XML format, a rule looks like this:

<Message_Rule Matching_Probability="RANKING">
  <Message_Pattern>
     <!-- definition of the pattern -->
  </Message_Pattern>
</Message_Rule>

The target ranking is marked RANKING in this rule, and we will describe below how a pattern can be defined.

The following ranking levels can be used as target ranking, in increasing order:

Info	Info messages about e.g. subprogram not being analyzed.
Low	Low ranking messages.
Medium	Medium ranking messages.
High	High ranking messages.
Suppressed	Used to suppress a message from the reports.

14.1.5.2. Matching of rules

For each message, Inspector will try to match each pattern of each rule. If no pattern matches, the ranking of the message remains Low. If a single pattern matches, the target ranking of the corresponding rule becomes the new ranking of the message. If several rules match, the highest ranking wins. Note in particular that Suppressed being the highest ranking, if a matching rule has target ranking Suppressed, the message is suppressed regardless of other matching rules.

14.1.5.3. Defining patterns

A pattern is a list of specifiers. There are three types of specifiers, Boolean specifiers, String specifiers, and computed specifiers. They are written as follows:

<Bool_Specifier Name_Of_Boolean_Attribute="NAME"></Bool_Specifier>

<String_Specifier
   Name_Of_String_Attribute="NAME"
   String_To_Match="REGEXP">
</String_Specifier>

<Computed_Specifier Name_of_Computed_Attribute="NAME"></Computed_Specifier>

For each type of specifier the NAME can be chosen among a predefined set. In addition, each specifier can be negated using the attribute Complement="YES".

14.1.5.3.1. Boolean specifiers

For Boolean specifiers, the following attributes are allowed:

Attribute Name	Description
Is_Big_Int	The message concerns an integer value.
Is_Big_Rat	The message concerns a real value.
Is_Side_Effect	The message is related to a side effect generated after calling a subprogram.
Is_Pointer	The message concerns a pointer.
Bad_Set_Includes_Null_Literal	The message concerns a pointer value which should not be null.
Expected_Set_Is_Subset_Plus_Minus_1000	The message concerns a value that is in -1000 .. 1000.
Expected_Set_Is_Singleton_Set	The message concerns a value that can have only one concrete value.
Valid_Bad_Set_Is_Singleton_Set	The message concerns a value which can take any concrete values except one.
Valid_Bad_Set_Overlaps_Plus_Minus_1000	The message concerns a value that should not be in -1000 .. 1000.
Precondition_Set_Contains_Holes	The message is about a precondition set which is not a contiguous range.
Precondition_Set_Has_Singleton_Hole_At_Zero	The message is about a precondition set which includes the values around zero, but not zero itself.
Check_Is_Soft	The message is soft (see Inspector Annotations)
Check_Is_Loop_Bound_Check	This message concerns a loop bound check
Bad_Set_Only_Invalid	The message is about a possibly uninitialized memory location.
Message_Depends_On_Unknown_Call	Message depends on unknown call.
Exception_Handler_Present	The enclosing basic block contains an exception handler. This is relevant in the context of validity checks when Inspector is checking whether scalar out parameters have been initialized.
Uninteresting_RHS	Uninteresting RHS in the context of dead store message.
Message_About_Implicit_Call	Message is about implicit (internal) call introduced by the compiler.
Message_Is_Uncertain	The message reflects some uncertainty. Alias for: Message_Depends_On_Unknown_Call or Exception_Handler_Present or Uninteresting_RHS or Message_About_Implicit_Call
Message_Depends_On_Object_Merging	Message depends on approximating more objects with one abstract object. This is the case when, e.g., array others or wildcard dereferences are involved.
Message_Involves_Loop_Imprecision	The message depends on a variable modified in a loop for which Inspector was not able to compute a precise range.
Message_Likely_False_Positive	Approximations were involved when computing information relevant for the message meaning that the message is more likely false positive. Is implied by: Message_Is_Uncertain, Message_Depends_On_Object_Merging, and Message_Involves_Loop_Imprecision

14.1.5.3.2. String specifiers

For String specifiers, the chosen attribute name will influence the meaning of the regular expression that is given with the second attribute. The following table gives an overview over the accepted attribute names.

Attribute Name	Description
Text	Regexp applies to text of the message. See below for details.
Subp	Regexp applies to subprogram name
File	Regexp applies to file name
Directory	Regexp applies to directory name
Likelihood	Regexp applies to likelihood of the failure, allowed values are: CHECK_WILL_FAIL, CHECK_MIGHT_FAIL, CHECK_CANNOT_FAIL
Check_Kind	Regexp applies to the kind of check that is described by the message. See below for a list of possible checks. Note that you can use a regular expression to match several kinds of checks at once. The regexp is not case sensitive for the attribute Check_Kind.
Original_Check_Kind	This is only valid for Precondition_Annotations and Precondition_Checks. Regexp applies to the kind of checks that caused the corresponding precondition.

The regexp above are those used in file names by the Unix shell or DOS prompt:

• * matches any string of 0 or more characters

• ? matches any character

• [char char ...] matches any character listed

• [char - char] matches any character in given range

• {elmt, elmt, ...} is an alternation (any of elmt)

A typical Inspector message like

div.adb:7:23: high: divide by zero (Inspector): check fails here; requires I >= 1

starts with the location of the message, followed by its rank, then its kind, and ends with some text with more details. In the case of a regexp with the attribute Text, the regexp applies to the rightmost part of the message which we call text in the following. Depending on the kind of message the regexp might not apply to the whole text. If the text start with requires, like above, the regexp only applies to the text after the requires, here I >= 1. In some cases the kind is not singled out with a colon, as in

main.adb:16:31: medium warning: dead code (Inspector): dead code because (is_equal'Result) = true
test.adb:8:7: medium warning: unused assignment (Inspector): unused assignment into A

In this case the regexp is only applied to the part starting after the kind of the message, here because (is_equal'Result) = true and into A. To get the exact text against which your regexp is applied you can use the debug switch --dbg-on patterns, see below for more information.

The list of Inspector check kind ids in MessagePatterns.xml corresponds mostly to GNAT SAS messages as described in GNAT SAS Messages Reference:

Check Kind	Description
NON_ANALYZED_CALL_WARNING	call not analyzed (due to e.g. tool limitation or code too complex)
SUSPICIOUS_PRECONDITION_WARNING	suspicious precondition
SUSPICIOUS_INPUT_WARNING	suspicious input
SUSPICIOUS_CONSTANT_OPERATION_WARNING	suspicious constant operation
UNREAD_IN_OUT_PARAMETER_WARNING	suspicious in out: could have out mode
UNASSIGNED_IN_OUT_PARAMETER_WARNING	suspicious in out: could have in mode
UNKNOWN_CALL_WARNING	unknown call (due to e.g. partitioning)
DEAD_STORE_WARNING	unused assignment
DEAD_OUTPARAM_STORE_WARNING	unused out parameter
POTENTIALLY_DEAD_STORE_WARNING	unused assignment to global
SAME_VALUE_DEAD_STORE_WARNING	useless reassignment
DEAD_BLOCK_WARNING	dead code
INFINITE_LOOP_WARNING	loop does not complete normally
PLAIN_DEAD_EDGE_WARNING	test predetermined
TRUE_DEAD_EDGE_WARNING	test always true
FALSE_DEAD_EDGE_WARNING	test always false
TRUE_CONDITION_DEAD_EDGE_WARNING	condition predetermined to true
FALSE_CONDITION_DEAD_EDGE_WARNING	condition predetermined to false
DEAD_BLOCK_CONTINUATION_WARNING	continuation of dead code
ANALYZED_MODULE_WARNING	module included in analysis
NON_ANALYZED_MODULE_WARNING	module not included, due to Inspector limitations
NON_ANALYZED_PROCEDURE_WARNING	subprogram not included, due to Inspector limitations
PROCEDURE_DOES_NOT_RETURN_ERROR	subprogram never returns
CHECK_FAILS_ON_EVERY_CALL_ERROR	subprogram always fails
UNLOCKED_REENTRANT_UPDATE_ERROR	unprotected access
UNLOCKED_SHARED_DAEMON_UPDATE_ERROR	unprotected shared access
MISMATCHED_LOCKED_UPDATE_ERROR	mismatched protected access
PRECONDITION_CHECK	precondition
INVALID_OR_NULL_CHECK	access check
DIVIDE_BY_ZERO_CHECK	divide by zero
ARRAY_INDEXING_CHECK	array index check
NUMERIC_OVERFLOW_CHECK	overflow check
USER_ASSIGN_STM_CHECK	overflow check
PRE_ASSIGN_STM_CHECK	overflow check (before a call)
POST_ASSIGN_STM_CHECK	overflow check (after a call)
NUMERIC_RANGE_CHECK	range check
TAG_CHECK	tag check
TYPE_VARIANT_CHECK	discriminant check
ALIASING_CHECK	parameter aliasing
RAISE_CHECK	raise exception
CONDITIONAL_RAISE_CHECK	conditional check
ASSERTION_CHECK	assertion
POSTCONDITION_CHECK	postcondition
INVALID_CHECK	validity check

Note that Inspector issues a warning when a check kind id (or regular expression) does not match any check.

In order to help you come up with correct rules you can use the Inspector debug switch --dbg-on patterns. This switch will make Inspector print all the messages in the following format:

Finding Rule for DEAD_STORE_WARNING: test.adb: test.p: into A

Where the first part is the check kind in the format to be used in a rule, the second part is the file, the third part the procedure containing the message, and the last part the text against which your regexp is matched. The above message is usually printed as:

test.adb:8:7: medium warning: unused assignment (Inspector): unused assignment into A

After each message, the rules that match the corresponding message (if any) are printed, precising the resulting ranking, e.g. :

Finding Rule for DEAD_STORE_WARNING: test.adb: test.p: into A
Rule # 57 matches.
  (first match)
winning probability: MEDIUM

Here you see that rule 57 is the first and only rule that matches the message, and that the resulting ranking is MEDIUM.

14.1.5.3.3. Computed specifiers

For computed specifiers, the allowed set of attribute names is the following:

Attribute Name	Description
Is_Check	The message concerns a check. (see GNAT SAS Messages Reference)
Is_Assign_Stm_Check	The message concerns a check for an assignment.
Is_Assign_Stm_Or_Precond_Check	The message concerns a check for an assignment or a precondition.
Source_Is_Ada	The source for that message is Ada (always true currently).
Message_Is_New	The message is new wrt. the baseline run.
Message_Is_Dropped	The message is in the baseline run, but not this run.
Message_Is_Unchanged	The message is unchanged wrt. the baseline run.
Max_Messages	Switch --messages was given with argument max.
Normal_Messages	Switch --messages was given with argument normal.
Min_Messages	Switch --messages was given with argument min.

14.1.5.4. Example

The following simple example shows a rule which will suppress all messages from the validity check category. Note that a simpler way to achieve the same effect would be to use --be-messages=-validity_check.

<Message_Probability_Rules>
  <Message_Rule Matching_Probability="SUPPRESSED">
    <Message_Pattern>
      <String_Specifier
        Name_Of_String_Attribute="Check_Kind"
        String_To_Match="INVALID_CHECK">
      </String_Specifier>
    </Message_Pattern>
  </Message_Rule>
</Message_Probability_Rules>

The following more complex example shows a rule which will flag as HIGH all check messages which are not soft, will always fail, and which are not user raise statements:

<Message_Probability_Rules>
 <Message_Rule Matching_Probability="HIGH">
   <Message_Pattern>
     <Computed_Specifier Name_Of_Computed_Attribute="Is_Check">
     </Computed_Specifier>

     <Bool_Specifier
       Complemented="YES"
       Name_Of_Boolean_Attribute="CHECK_IS_SOFT">
     </Bool_Specifier>

     <String_Specifier
       Name_Of_String_Attribute="Likelihood"
       String_To_Match="CHECK_WILL_FAIL">
     </String_Specifier>

     <String_Specifier
       Complemented="YES"
       Name_Of_String_Attribute="Check_Kind"
       String_To_Match="RAISE_CHECK">
     </String_Specifier>

   </Message_Pattern>
 </Message_Rule>
</Message_Probability_Rules>

14.2. Inspector By Example

GNAT SAS' Inspector engine is very different from most static analyzers, which execute symbolically the program until a safe approximation is reached. Instead, Inspector works bottom-up from callees to callers, generating a contract for each subprogram along the way. Contracts are the basis for generating error messages related to possible run-time errors and logic errors, and they can be inspected during code reviews to detect further errors. Thus, it is essential to understand how Inspector generates contracts, and how it uses contracts to detect errors. This section aims at providing a deeper insight into how GNAT SAS' Inspector engine works, through a step-by-step exploration of simple code examples. The code for these examples is available in the distribution of GNAT SAS, under <gnatsas install>/share/examples/gnat_sas/inspector_by_example, and in GNAT Studio through menu Help ‣ GNATSAS ‣ Examples ‣ Inspector by Example.

14.2.1. Basic Examples

This section presents the results of running GNAT SAS' Inspector on simple subprograms composed of assignments, branchings and calls.

14.2.1.1. Scalar Assignment

Assign

Inspector is able to follow very precisely the assignments to scalar variables throughout the program. Take a very simple program Assign that assigns the value Y+1 to the variable X:

procedure Assign (X : out Integer; Y : in Integer) is
begin
   X := Y + 1;
end Assign;

On this subprogram, Inspector generates the following contract:

assign.adb:1: (pre)- assign:(overflow check) Y /= 2_147_483_647
assign.adb:1: (post)- assign:X /= -2_147_483_648
assign.adb:1: (post)- assign:X = Y + 1

The precondition on line 1 requires that the value of Y passed in argument to Assign be less than the maximal integer value. This is good advice indeed, because otherwise the addition on line 3 of Assign overflows.

The postcondition on line 3 indicates that the value of X after the call is equal to Y+1. The postcondition on line 2 indicates that this value is different from (hence greater than) the minimal integer value.

On this first example, Inspector is able to generate the most precise contract for subprogram Assign. On more complex subprograms, Inspector will generate a comprehensive and safe approximation.

Bad_Assign

Consider a version of Assign where X is read inside the subprogram before it is assigned a value:

procedure Bad_Assign (X : out Integer; Y : in Integer) is
begin
   X := X + 1;
end Bad_Assign;

Inspector detects that X is not initialized when it is read on line 3, and thus it generates an error:

bad_assign.adb:3:9: high: validity check [CWE 457] (Inspector): X is uninitialized here

Assign_To_Pos

When constrained types are used, for example the type Positive of positive integers in Ada, then Inspector uses this information in the contracts it generates. Take a variation of Assign where parameter X is a positive integer:

procedure Assign_To_Pos (X : out Positive; Y : in Integer) is
begin
   X := Y + 1;
end Assign_To_Pos;

On this subprogram, Inspector generates the following contract:

assign_to_pos.adb:1: (pre)- assign_to_pos:(range check) Y in 0..2_147_483_646
assign_to_pos.adb:1: (post)- assign_to_pos:X = Y + 1
assign_to_pos.adb:1: (post)- assign_to_pos:X'Initialized

Note how the range of Y in the precondition on line 1 has been restricted to positive integers less than the maximal integer value. Note also that the postcondition on line 3 only indicates now that X is initialized on exit, which is the most precise information here given that the type of X already excludes all negative values. The attribute 'Initialized is not an actual Ada attribute. It is used to denote that a location has been initialized. This is different from the Ada attribute 'Valid which only denotes that a location has a valid bit representation. For example, a variable of a machine integer type is always valid, even if it is not initialized.

Bad_Assign_To_Pos

Consider a version of Assign_To_Pos where the assignment to X always results in a constraint error, whatever the precondition:

procedure Bad_Assign_To_Pos (X : out Positive; Y : in Positive) is
begin
   X := -Y + 1;
end Bad_Assign_To_Pos;

Inspector detects that no suitable precondition can be generated for this subprogram, and it generates errors:

bad_assign_to_pos.adb:1:1: high warning: subp always fails (Inspector): bad_assign_to_pos fails for all possible inputs
bad_assign_to_pos.adb:3:12: high: range check [CWE 682] (Inspector): check fails here

Self_Assign

As shown in the examples above, the precondition refers to values of variables before a call, while the postcondition refers to values of variables after a call. In general, though, postconditions may relate values on entry to a subprogram and values on exit to the same subprogram. Consider the code of Self_Assign which increments the value of its parameter X:

procedure Self_Assign (X : in out Integer) is
begin
   X := X + 1;
end Self_Assign;

On this subprogram, Inspector generates the following contract:

self_assign.adb:1: (pre)- self_assign:(overflow check) X /= 2_147_483_647
self_assign.adb:1: (post)- self_assign:X /= -2_147_483_648
self_assign.adb:1: (post)- self_assign:X = X'Old + 1

The precondition on line 1 indeed refers to the value of X before the call, and the postcondition on line 2 refers to the value of X after the call. The interesting case is the postcondition on line 3, which relates the value of X before the call, denoted X'Old, and the value of X after the call.

Bad_Self_Assign

Consider a version of Self_Assign where X is assigned its current value previously copied:

procedure Bad_Self_Assign (X : in out Integer) is
   Y : Integer := X - 1;
begin
   X := Y + 1;
end Bad_Self_Assign;

When --mode=deep is given, Inspector detects that the assignment is useless, and it generates a warning:

bad_self_assign.adb:4:6: medium warning: useless reassignment [CWE 563] (Inspector): useless reassignment of X

14.2.1.2. Aggregate Assignment

Assign_Rec

Inspector is able to follow assignments to variables of composite type as precisely as assignments to scalar variables. Take for example a record type Rec aggregating an integer and a Pair, which is itself aggregating two integers:

package Assign_Rec is
   type Pair is record
      A, B : Integer;
   end record;
   type Rec is record
      C : Integer;
      D : Pair;
   end record;
   procedure Assign (X : out Rec; Y : in Integer);
end Assign_Rec;

The subprogram Assign_Rec.Assign updates some components of its record parameter X:

package body Assign_Rec is
   procedure Assign (X : out Rec; Y : in Integer) is
   begin
      X.C := Y + 1;
      X.D.B := Y - 1;
   end Assign;
end Assign_Rec;

On this subprogram, Inspector generates the following contract:

assign_rec.adb:2: (pre)- assign_rec.assign:(overflow check) Y in -2_147_483_647..2_147_483_646
assign_rec.adb:2: (post)- assign_rec.assign:X.C = Y + 1
assign_rec.adb:2: (post)- assign_rec.assign:X.C >= -2_147_483_646
assign_rec.adb:2: (post)- assign_rec.assign:X.D.B <= 2_147_483_645
assign_rec.adb:2: (post)- assign_rec.assign:X.D.B = Y - 1

The postconditions on lines 2-5 correspond exactly to the most precise postconditions on this subprogram, which one would also get with assignments to scalar variables.

Bad_Assign_Rec

Consider a version of Assign_Rec where Y is multiplied and divided by one million, instead of being incremented and decremented by one:

with Assign_Rec; use Assign_Rec;
procedure Bad_Assign_Rec (X : out Rec; Y : in Integer) is
begin
   X.C := Y * 1_000_000;
   X.D.B := Y / 1_000_000;
end Bad_Assign_Rec;

Inspector detects that the expression Y / 1_000_000 on line 5 always evaluates to zero, and it issues a warning:

bad_assign_rec.adb:5:15: medium warning: suspicious constant operation (Inspector): operation Y/1_000_000 always evaluates to 0

Indeed, since Y is multiplied by one million, its absolute value should be less than 2147, as indicated by the contract generated by Inspector:

bad_assign_rec.adb:2: (pre)- bad_assign_rec:(overflow check) Y in -2_147..2_147
bad_assign_rec.adb:2: (post)- bad_assign_rec:X.C = Y*1_000_000
bad_assign_rec.adb:2: (post)- bad_assign_rec:X.C in -2_147_000_000..2_147_000_000
bad_assign_rec.adb:2: (post)- bad_assign_rec:X.D.B = 0

Then, dividing Y by one million always gives the value zero.

Assign_Arr

Similarly, take an array type Arr aggregating ten integers:

package Assign_Arr is
   type Arr is array (1 .. 10) of Integer;
   procedure Assign (X : out Arr; Y : in Integer);
end Assign_Arr;

The subprogram Assign_Arr.Assign updates some elements of its array parameter X:

package body Assign_Arr is
   procedure Assign (X : out Arr; Y : in Integer) is
   begin
      X (1) := Y + 1;
      X (4) := Y - 1;
   end Assign;
end Assign_Arr;

On this subprogram, Inspector generates the following contract:

assign_arr.adb:2: (pre)- assign_arr.assign:(overflow check) Y in -2_147_483_647..2_147_483_646
assign_arr.adb:2: (post)- assign_arr.assign:X(1 | 4)'Initialized
assign_arr.adb:2: (post)- assign_arr.assign:X(1) = Y + 1
assign_arr.adb:2: (post)- assign_arr.assign:X(4) = Y - 1

The postconditions on lines 2-4 correspond exactly to the most precise postconditions already shown for Assign_Rec.Assign.

Bad_Assign_Arr

Consider a version of Assign_Arr where X is assigned at indexes Y and Y + 10:

with Assign_Arr; use Assign_Arr;
procedure Bad_Assign_Arr (X : out Arr; Y : in Integer) is
begin
   X (Y) := 1;
   X (Y + 10) := -1;
end Bad_Assign_Arr;

Inspector detects that the expression Y + 10 on line 5 is outside of the bounds of X, which ranges from 1 to 10, and it issues an error:

bad_assign_arr.adb:2:1: high warning: subp always fails (Inspector): bad_assign_arr fails for all possible inputs
bad_assign_arr.adb:4:4: medium: array index check [CWE 120] (Inspector): requires Y in 1..10
bad_assign_arr.adb:5:4: high: array index check [CWE 120] (Inspector): check fails here; requires Y in -9..0

Indeed, since index Y is used to access X, its value should be between 1 and 10. Then, Y + 10 is greater than the upper bound of X.

Assign_Arr_Unk

Finally, take an array type Arr aggregating an unknown number of integers:

package Assign_Arr_Unk is
   type Arr is array (Integer range <>) of Integer;
   procedure Assign (X : out Arr; Y : in Integer);
end Assign_Arr_Unk;

The subprogram Assign_Arr_Unk.Assign updates some elements of its array parameter X:

package body Assign_Arr_Unk is
   procedure Assign (X : out Arr; Y : in Integer) is
   begin
      X (1) := Y + 1;
      X (4) := Y - 1;
   end Assign;
end Assign_Arr_Unk;

On this subprogram, Inspector generates the following contract:

assign_arr_unk.adb:2: (pre)- assign_arr_unk.assign:(array index check) X'First <= 1
assign_arr_unk.adb:2: (pre)- assign_arr_unk.assign:(array index check) X'Last >= 4
assign_arr_unk.adb:2: (pre)- assign_arr_unk.assign:(overflow check) Y in -2_147_483_647..2_147_483_646
assign_arr_unk.adb:2: (post)- assign_arr_unk.assign:X(1 | 4)'Initialized
assign_arr_unk.adb:2: (post)- assign_arr_unk.assign:X(1) = Y + 1
assign_arr_unk.adb:2: (post)- assign_arr_unk.assign:X(4) = Y - 1

The postconditions on lines 4-6 correspond exactly to the most precise postconditions already shown.

14.2.1.3. Branching

Cond_Assign

A common limitation of static analyzers is that they cannot follow precisely disjunctions that occur due to branches in the program. Inspector uses advanced techniques to overcome this difficulty and actually follow these branches. Take a simple subprogram Cond_Assign that assigns a different value to parameter X depending on the value of another parameter B:

procedure Cond_Assign (X : out Integer; Y : in Integer; B : in Boolean) is
begin
   if B then
      X := Y + 1;
   else
      X := Y - 1;
   end if;
end Cond_Assign;

On this subprogram, Inspector generates the following contract:

cond_assign.adb:1: (pre)- cond_assign:(overflow check) B or Y /= -2_147_483_648
cond_assign.adb:1: (pre)- cond_assign:(overflow check) not B or Y /= 2_147_483_647
cond_assign.adb:1: (post)- cond_assign:X = One-of{Y + 1, Y - 1}
cond_assign.adb:1: (post)- cond_assign:X'Initialized

The preconditions on line 1 and 2 precisely represent the conditions that input parameters should respect to avoid an integer negative overflow (on line 6 of Cond_Assign) or positive overflow (on line 4 of Cond_Assign). Note how these preconditions are expressed as disjunctions. This is because the negative or positive overflow is only possible for a particular value of B (which differs between the negative overflow and the positive overflow).

The postcondition on line 3 indicates that the value of X on exit either comes from the assignment on line 4, or the one on line 6. This is not the most precise postcondition, as one could state that, on exit:

(B = True and X = Y + 1) or (B = False and X = Y - 1)

As seen with the Call_Assign example below, Inspector actually generates internally this more precise postcondition, from which it outputs on line 3 a more user-friendly postcondition. The internal (more precise) postcondition is used for analyzing callers of Cond_Assign.

Bad_Cond_Assign

Consider a version of Cond_Assign with a modified test:

procedure Bad_Cond_Assign (X : out Integer; Y : in Integer; B : in Boolean) is
begin
   if B or not B then
      X := Y + 1;
   else
      X := Y - 1;
   end if;
end Bad_Cond_Assign;

Inspector detects that the test on line 3 is always true and it issues a warning:

bad_cond_assign.adb:3:9: medium warning: test always true [CWE 571] (Inspector): test always true because B or not B
bad_cond_assign.adb:6:9: medium warning: dead code [CWE 561] (Inspector): dead code because B or not B

Multi_Cond_Assign

The precise analysis of branches seen on Cond_Assign is performed by Inspector on any number of if statements, as shown on Multi_Cond_Assign:

procedure Multi_Cond_Assign (X : out Integer; Y : in Integer; B1, B2 : in Boolean) is
begin
   if B1 then
      X := Y + 1;
   else
      if B2 then
	 X := Y - 1;
      else
	 X := Y * 2;
      end if;
   end if;
end Multi_Cond_Assign;

On this subprogram, Inspector generates the following contract:

multi_cond_assign.adb:1: (pre)- multi_cond_assign:(overflow check) B1 or B2 or Y*2 in -2_147_483_648..2_147_483_647
multi_cond_assign.adb:1: (pre)- multi_cond_assign:(overflow check) B1 or not B2 or Y /= -2_147_483_648
multi_cond_assign.adb:1: (pre)- multi_cond_assign:(overflow check) not B1 or Y /= 2_147_483_647
multi_cond_assign.adb:1: (post)- multi_cond_assign:X = One-of{Y + 1, Y - 1, Y*2}
multi_cond_assign.adb:1: (post)- multi_cond_assign:X'Initialized

The postcondition on line 4 is similar to the one obtained for Cond_Assign, except here it deals with two if statements. Our comment about Inspector generating internally a contract more precise than the one displayed for Cond_Assign is also applicable here.

Bad_Multi_Cond_Assign

Consider a version of Multi_Cond_Assign with modified tests:

procedure Bad_Multi_Cond_Assign (X : out Integer; Y : in Integer; B1, B2 : in Boolean) is
begin
   if B1 or Y < 10 then
      X := Y + 1;
   else
      if B2 and not (Y > 0) then
	 X := Y - 1;
      else
	 X := Y * 2;
      end if;
   end if;
end Bad_Multi_Cond_Assign;

Inspector detects that the test on line 6 is always false and it issues a warning:

bad_multi_cond_assign.adb:6:13: low warning: test always false [CWE 570] (Inspector): test always false because not B2 or Y >= 1
bad_multi_cond_assign.adb:7:12: medium warning: dead code [CWE 561] (Inspector): dead code because not B2 or Y >= 1

Case_Assign

The analysis of case statements is similar to the analysis of if statements. Consider the subprogram Case_Assign.Assign which takes an operation Op in parameter, among three possibilities:

package Case_Assign is
  type Oper is (Incr, Decr, Double);
  procedure Assign (X : out Integer; Y : in Integer; Op : in Oper);
end Case_Assign;

It does the obvious assignment in each case:

package body Case_Assign is
  procedure Assign (X : out Integer; Y : in Integer; Op : in Oper) is
  begin
     case Op is
        when Incr =>
           X := Y + 1;
        when Decr =>
           X := Y - 1;
        when Double =>
           X := Y * 2;
     end case;
  end Assign;
end Case_Assign;

On this subprogram, Inspector generates the following contract:

case_assign.adb:2: (pre)- case_assign.assign:(overflow check) Op /= Decr or Y /= -2_147_483_648
case_assign.adb:2: (pre)- case_assign.assign:(overflow check) Op /= Double or Y*2 in -2_147_483_648..2_147_483_647
case_assign.adb:2: (pre)- case_assign.assign:(overflow check) Op /= Incr or Y /= 2_147_483_647
case_assign.adb:2: (post)- case_assign.assign:X = One-of{Y + 1, Y - 1, Y*2}
case_assign.adb:2: (post)- case_assign.assign:X'Initialized

The postcondition on line 4 is the same as what is obtained for if statements in Multi_Cond_Assign. The same comment about the internally more precise contract still applies.

14.2.1.4. Call Statement

Call_Assign

The modular treatment of calls is a cornerstone of Inspector analysis. Before a caller of subprogram S is analyzed, the body of S is analyzed and Inspector generates a contract for S. Then, this contract is used to completely abstract the calls to S during the analysis of its callers. In fast mode, Inspector uses precise contracts for all the calls in the same library unit and treats other as unknown. In deep mode, Inspector uses precise contracts for all the calls in the same partition - see Partitioning of Analysis for more details. Direct and mutually recursive calls require that a coarser contract is used for bootstrapping. This coarser contract is then iteratively refined. Consider the subprogram Call_Assign.Call:

package Call_Assign is
   type Choice is (Simple, Conditional, Self);
   procedure Call (X : in out Integer; C : in Choice);
end Call_Assign;

It calls one of Assign, Cond_Assign or Self_Assign seen previously, depending on the value of its parameter C:

with Assign, Cond_Assign, Self_Assign;
package body Call_Assign is
   procedure Call (X : in out Integer; C : in Choice) is
   begin
      case C is
         when Simple =>
            Assign (X, 1);
         when Conditional =>
            Cond_Assign (X, 2, True);
         when Self =>
            Self_Assign (X);
      end case;
   end Call;
end Call_Assign;

On this subprogram, when run with --mode=deep, Inspector generates the following contract:

call_assign.adb:3: (pre)- call_assign.call:(overflow check) C /= Self or X /= 2_147_483_647
call_assign.adb:3: (post)- call_assign.call:X /= -2_147_483_648
call_assign.adb:3: (post)- call_assign.call:X = One-of{2, 3, X'Old + 1}

The precondition on line 1 only constrains the input value of X when C is equal to Self. Indeed, the generated preconditions for Assign and Cond_Assign are always satisfied by the values passed in parameters in Call_Assign, while the generated precondition for Self_Assign imposes that X is less than the maximal integer value.

The postcondition on line 3 enumerates the possible values for X on exit. The value 2 corresponds to the call to Assign. The value 3 corresponds to the call to Cond_Assign. Note here that Inspector used the more precise internal contract for Cond_Assign instead of the one displayed, which would have lead to an additional possible value of 1 for X. The value X'Old + 1 corresponds to the call to Self_Assign.

The postcondition on line 2 is a common constraint on X on exit, whatever the procedure called.

Bad_Call_Assign

Consider a version of Call_Assign in which subprograms Assign, Cond_Assign and Self_Assign are all called in contexts that violate their generated preconditions:

with Call_Assign; use Call_Assign;
with Assign, Cond_Assign, Self_Assign;
procedure Bad_Call_Assign (X : in out Integer; C : in Choice) is
begin
   case C is
      when Simple =>
	 Assign (X, Integer'Last);
      when Conditional =>
	 Cond_Assign (X, Integer'Last, True);
      when Self =>
	 X := Integer'Last;
	 Self_Assign (X);
   end case;
end Bad_Call_Assign;

Inspector detects these violations and it issues corresponding precondition errors:

bad_call_assign.adb:3:1: medium warning: unread parameter (Inspector): parameter X could have mode out

Reverse_Call_Assign

You might be wondering whether Inspector computed a more precise internal postcondition for the postcondition of Call_Assign displayed on line 3. This is indeed the case, as shown in the following example. Consider three subprograms for each value of the Choice enumeration:

package Reverse_Call_Assign is
   procedure Call_Simple (X : in out Integer);
   procedure Call_Conditional (X : in out Integer);
   procedure Call_Self (X : in out Integer);
end Reverse_Call_Assign;

Each subprogram calls Call_Assign.Call with the corresponding value for parameter C:

with Call_Assign; use Call_Assign;
package body Reverse_Call_Assign is
   procedure Call_Simple (X : in out Integer) is
   begin
      Call (X, Simple);
   end Call_Simple;
   procedure Call_Conditional (X : in out Integer) is
   begin
      Call (X, Conditional);
   end Call_Conditional;
   procedure Call_Self (X : in out Integer) is
   begin
      Call (X, Self);
   end Call_Self;
end Reverse_Call_Assign;

On these subprograms, when run with --mode=deep, Inspector generates the following contracts:

reverse_call_assign.adb:3: (post)- reverse_call_assign.call_simple:X = 2
reverse_call_assign.adb:7: (post)- reverse_call_assign.call_conditional:X = 3
reverse_call_assign.adb:11: (pre)- reverse_call_assign.call_self:(overflow check) X /= 2_147_483_647
reverse_call_assign.adb:11: (post)- reverse_call_assign.call_self:X /= -2_147_483_648
reverse_call_assign.adb:11: (post)- reverse_call_assign.call_self:X = X'Old + 1

The postcondition on line 1 is indeed the most precise contract on Call_Simple, as it is the same as the contract generated for Assign with the value of 1 for Y.

The postcondition on line 2 is indeed the most precise contract on Call_Conditional, as it is the same as the contract generated for Cond_Assign with the value of 2 for Y and True for B.

The precondition on line 3 and the postconditions on lines 4 and 5 are indeed the most precise contract on Call_Self, as they are the same as the contract generated for Self_Assign.

Inspector could only generate these most precise contracts because it did not lose the relation between the input value of parameter C and the output value of parameter X in Call_Assign.Call. The internal most precise postcondition computed by Inspector for Call_Assign.Call is really:

(C = Simple and X = 2) or (C = Conditional and X = 3) or (C = Self and X = X'Old + 1)

Top_Down

Inspector completely works bottom-up on the call-graph, propagating information gathered from callees in their generated contracts to their callers. This strategy ensures that partial applications can be handled easily, and that the analysis is much faster than the classical top-down approach. Although Inspector does not use knowledge of the calling context when analyzing a subprogram, in many cases it generates contracts precise enough to take this context into account.

Consider the local function Ident which is always called in a context where the content of array A is all ones:

with Assign_Arr; use Assign_Arr;
procedure Top_Down (Y : out Integer) is
   A : Arr;
   function Ident (X : Integer) return Integer is
   begin
      if A (X) > 0 then
         return X;
      else
         return 0;
      end if;
   end Ident;
begin
   A := (others => 1);
   Y := A (Ident (3));
end Top_Down;

Inspector does not use this information in the analysis of Ident, but instead generates a conditional postcondition taking the value of X into account (even though this is not visible in the printable version, internally Inspector knows that One-of{X, 0} really means X when A(X) > 0 and 0 otherwise):

top_down.adb:2: (post)- top_down:Y = 1
top_down.adb:4: (pre)- top_down.ident:(validity check) A(X)'Initialized
top_down.adb:4: (pre)- top_down.ident:(array index check) X in 1..10
top_down.adb:4: (post)- top_down.ident:top_down.ident'Result = One-of{X, 0}
top_down.adb:4: (post)- top_down.ident:top_down.ident'Result in 0..10

Thus, Inspector can then check that the call to Ident(3) returns a positive value since at this point it knows that X(3) > 0.

14.2.2. Loop Examples

This section presents the results of running GNAT SAS' Inspector on subprograms containing loops.

14.2.2.1. Induction Variables

Induction

The first difficulty in analyzing loops is that it is not possible in general to completely unroll the loop, either because the number of iterations is very large, or because it is not known statically. Thus, the static analysis must analyze together all iterations beyond a certain point. This is a source of approximations, in particular for induction variables, that is, those variables assigned in the loop. However, Inspector analyzes precisely those induction variables that are incremented or decremented at each run through the loop.

For example, take a simple subprogram incrementing a variable X 10 times:

procedure Induction (X : out Integer) is
begin
   X := 0;
   for J in 1 .. 10 loop
      X := X + 1;
   end loop;
end Induction;

On this subprogram, Inspector generates the following contract:

induction.adb:1: (post)- induction:X = 10

Inspector manages here to generate the most precise postcondition for the loop.

Bad_Induction

Consider a version of Induction in which X is not initialized before the loop:

procedure Bad_Induction (X : out Integer) is
begin
   for J in 1 .. 10 loop
      X := X + 1;
   end loop;
end Bad_Induction;

Inspector detects that X might be uninitialized on line 4 and it issues an error:

bad_induction.adb:4:12: high: validity check [CWE 457] (Inspector): check fails here; requires X'Initialized (iteration 1 of 10)

Multi_Induction

In many cases, Inspector can also follow precisely the relations between induction variables in a loop, as in subprogram Multi_Induction:

procedure Multi_Induction (X1, X2 : out Integer; Y : in Integer) is
begin
   X1 := 0;
   X2 := 0;
   while X1 < Y loop
      X1 := X1 + 2;
      X2 := X2 + 6;
   end loop;
end Multi_Induction;

On this subprogram, Inspector generates the following contract:

multi_induction.adb:1: (pre)- multi_induction:Y <= 715_827_882
multi_induction.adb:1: (post)- multi_induction:X1 - Y in 0..2_147_483_648
multi_induction.adb:1: (post)- multi_induction:X1 in (0 | 2 | 4 | 6 | ... | 44..715_827_882)
multi_induction.adb:1: (post)- multi_induction:X2 - Y*3 in -2_147_483_646..6_442_450_944
multi_induction.adb:1: (post)- multi_induction:X2 = X1*3
multi_induction.adb:1: (post)- multi_induction:X2 in (0 | 6 | 12 | 18 | ... | 132..2_147_483_646)

Note how the postcondition on line 5 correctly indicates the relation between X1 and X2 after the loop.

Bad_Multi_Induction

Consider a version of Multi_Induction in which X1 is not assigned in the loop:

procedure Bad_Multi_Induction (X1, X2 : out Integer; Y : in Positive) is
begin
   X1 := 0;
   X2 := 0;
   while X1 < Y loop
      X2 := X2 + 6;
   end loop;
   return;
end Bad_Multi_Induction;

Inspector detects that the loop never terminates, because the exit test on line 5 is always true:

bad_multi_induction.adb:1:1: medium warning: subp never returns (Inspector): bad_multi_induction never returns
bad_multi_induction.adb:5:13: medium warning: test always true [CWE 571] (Inspector): test always true because X1 < Y
bad_multi_induction.adb:5:13: medium warning: loop does not complete normally [CWE 835] (Inspector)
bad_multi_induction.adb:8:4: medium warning: dead code [CWE 561] (Inspector): dead code because X1 < Y

14.2.2.2. Array Scanning

The most frequent use of loops is to iterate over a collection, for example an array. Use of arrays introduces a new difficulty, namely that the static analysis must handle a large or unbounded number of memory locations. This requires performing some abstractions, to compute a safe approximation.

Search

Take a simple function Search scanning an array for a value. We are reusing here the type Assign_Arr.Arr from example Assign_Arr of arrays of ten integers.

with Assign_Arr; use Assign_Arr;
function Search (X : in Arr; Y : in Integer) return Integer is
begin
   for J in X'Range loop
      if X (J) = Y then
         return J;
      end if;
   end loop;
   return 0;
end Search;

On this subprogram, Inspector generates the following contract:

search.adb:2: (pre)- search:(validity check) X(1) = Y or X(2) = Y or X(3) = Y or X(4) = Y or X(5) = Y or X(6) = Y or X(7) = Y or X(8) = Y or X(9) = Y or X(10)'Initialized
search.adb:2: (pre)- search:(validity check) X(1) = Y or X(2) = Y or X(3) = Y or X(4) = Y or X(5) = Y or X(6) = Y or X(7) = Y or X(8) = Y or X(9)'Initialized
search.adb:2: (pre)- search:(validity check) X(1) = Y or X(2) = Y or X(3) = Y or X(4) = Y or X(5) = Y or X(6) = Y or X(7) = Y or X(8)'Initialized
search.adb:2: (pre)- search:(validity check) X(1) = Y or X(2) = Y or X(3) = Y or X(4) = Y or X(5) = Y or X(6) = Y or X(7)'Initialized
search.adb:2: (pre)- search:(validity check) X(1) = Y or X(2) = Y or X(3) = Y or X(4) = Y or X(5) = Y or X(6)'Initialized
search.adb:2: (pre)- search:(validity check) X(1) = Y or X(2) = Y or X(3) = Y or X(4) = Y or X(5)'Initialized
search.adb:2: (pre)- search:(validity check) X(1) = Y or X(2) = Y or X(3) = Y or X(4)'Initialized
search.adb:2: (pre)- search:(validity check) X(1) = Y or X(2) = Y or X(3)'Initialized
search.adb:2: (pre)- search:(validity check) X(1) = Y or X(2)'Initialized
search.adb:2: (pre)- search:(validity check) X(1)'Initialized
search.adb:2: (post)- search:search'Result in 0..10

The preconditions on lines 1-10 exactly capture in which case the function can be called, regarding the initialization of the array X. Indeed, it is safe to call Assign_arr with a partially initialized array, provided the value Y is found before reaching the uninitialized part.

The postcondition on line 11 is a safe approximation on Search. The most precise postcondition would have to state that either the array X does not contain Y, in which case Search returns 0, or the array X contains Y, in which case Search returns the smallest corresponding index.

Bad_Search

Consider a version of Search in which the final return statement is missing:

with Assign_Arr; use Assign_Arr;
function Bad_Search (X : in Arr; Y : in Integer) return Integer is
begin
   for J in X'Range loop
      if X (J) = Y then
         return J;
      end if;
   end loop;
end Bad_Search;

On this subprogram, Inspector generates the following contract:

bad_search.adb:2: (pre)- bad_search:(conditional raise) X(1) = Y or X(2) = Y or X(3) = Y or X(4) = Y or X(5) = Y or X(6) = Y or X(7) = Y or X(8) = Y or X(9) = Y or X(10) = Y
bad_search.adb:2: (pre)- bad_search:(validity check) X(1) = Y or X(2) = Y or X(3) = Y or X(4) = Y or X(5) = Y or X(6) = Y or X(7) = Y or X(8) = Y or X(9) = Y or X(10)'Initialized
bad_search.adb:2: (pre)- bad_search:(validity check) X(1) = Y or X(2) = Y or X(3) = Y or X(4) = Y or X(5) = Y or X(6) = Y or X(7) = Y or X(8) = Y or X(9)'Initialized
bad_search.adb:2: (pre)- bad_search:(validity check) X(1) = Y or X(2) = Y or X(3) = Y or X(4) = Y or X(5) = Y or X(6) = Y or X(7) = Y or X(8)'Initialized
bad_search.adb:2: (pre)- bad_search:(validity check) X(1) = Y or X(2) = Y or X(3) = Y or X(4) = Y or X(5) = Y or X(6) = Y or X(7)'Initialized
bad_search.adb:2: (pre)- bad_search:(validity check) X(1) = Y or X(2) = Y or X(3) = Y or X(4) = Y or X(5) = Y or X(6)'Initialized
bad_search.adb:2: (pre)- bad_search:(validity check) X(1) = Y or X(2) = Y or X(3) = Y or X(4) = Y or X(5)'Initialized
bad_search.adb:2: (pre)- bad_search:(validity check) X(1) = Y or X(2) = Y or X(3) = Y or X(4)'Initialized
bad_search.adb:2: (pre)- bad_search:(validity check) X(1) = Y or X(2) = Y or X(3)'Initialized
bad_search.adb:2: (pre)- bad_search:(validity check) X(1) = Y or X(2)'Initialized
bad_search.adb:2: (pre)- bad_search:(validity check) X(1)'Initialized
bad_search.adb:2: (post)- bad_search:bad_search'Result in 1..10

Inspector will figure out that in order for the subprogram to exit successfully, the loop should never terminate without a return, otherwise the subprogram would raise Program_Error (as mandated by the Ada standard). This is expressed by the precondition at line 1.

Call_Search

Inspector also computes the set of inputs and outputs of Search, whether these are reachable from parameters or global variables. These inputs and outputs form a part of the generated contract not shown here. Now consider a caller of Search, that calls it twice on the same inputs:

with Assign_Arr; use Assign_Arr;
with Search;
procedure Call_Search (X : in Arr; Y : in Integer; U, V : out Integer) is
begin
   U := Search (X, Y);
   V := Search (X, Y);
end Call_Search;

On this subprogram, when run with --mode=deep, Inspector generates the following contract:

call_search.adb:3: (pre)- call_search:(validity check) X(1) = Y or X(2) = Y or X(3) = Y or X(4) = Y or X(5) = Y or X(6) = Y or X(7) = Y or X(8) = Y or X(9) = Y or X(10)'Initialized
call_search.adb:3: (pre)- call_search:(validity check) X(1) = Y or X(2) = Y or X(3) = Y or X(4) = Y or X(5) = Y or X(6) = Y or X(7) = Y or X(8) = Y or X(9)'Initialized
call_search.adb:3: (pre)- call_search:(validity check) X(1) = Y or X(2) = Y or X(3) = Y or X(4) = Y or X(5) = Y or X(6) = Y or X(7) = Y or X(8)'Initialized
call_search.adb:3: (pre)- call_search:(validity check) X(1) = Y or X(2) = Y or X(3) = Y or X(4) = Y or X(5) = Y or X(6) = Y or X(7)'Initialized
call_search.adb:3: (pre)- call_search:(validity check) X(1) = Y or X(2) = Y or X(3) = Y or X(4) = Y or X(5) = Y or X(6)'Initialized
call_search.adb:3: (pre)- call_search:(validity check) X(1) = Y or X(2) = Y or X(3) = Y or X(4) = Y or X(5)'Initialized
call_search.adb:3: (pre)- call_search:(validity check) X(1) = Y or X(2) = Y or X(3) = Y or X(4)'Initialized
call_search.adb:3: (pre)- call_search:(validity check) X(1) = Y or X(2) = Y or X(3)'Initialized
call_search.adb:3: (pre)- call_search:(validity check) X(1) = Y or X(2)'Initialized
call_search.adb:3: (pre)- call_search:(validity check) X(1)'Initialized
call_search.adb:3: (post)- call_search:U in 0..10
call_search.adb:3: (post)- call_search:V = U

Inspector uses the knowledge that the same inputs produce the same outputs to compute the postcondition on line 12.

Bad_Call_Search

Consider a caller of Search which does not initialize the last element of parameter X before the call:

with Assign_Arr; use Assign_Arr;
with Search;
function Bad_Call_Search return Integer is
   X : Arr;
begin
   for J in 1 .. 9 loop
      X (J) := J;
   end loop;
   return Search (X, 10);
end Bad_Call_Search;

When run with --mode=deep, Inspector generates an error, as it understands that X(10) is not initialized, and that 10 is not among the possible values at indices 1..9.

bad_call_search.adb:3:1: high warning: subp always fails (Inspector): bad_call_search fails for all possible inputs
bad_call_search.adb:9:11: high: precondition <validity check> [CWE 457] (Inspector): precondition failure on call to search; requires X(1) = Y or X(2) = Y or X(3) = Y or X(4) = Y or X(5) = Y or X(6) = Y or X(7) = Y or X(8) = Y or X(9) = Y or X(10) to be initialized

Search_Unk

Take now a slightly different function Search_Unk. It also scans an array for a value, but we are reusing here the type Assign_Arr_Unk.Arr from example Assign_Arr_Unk of unconstrained arrays, which may contain an unbounded number of integers.

with Assign_Arr_Unk; use Assign_Arr_Unk;
function Search_Unk (X : in Arr; Y : in Integer) return Integer is
begin
   for J in X'Range loop
      if X (J) = Y then
         return J;
      end if;
   end loop;
   return 0;
end Search_Unk;

On this subprogram, Inspector generates the following contract:

search_unk.adb:2: (pre)- search_unk:X'Length = 0 or X(J)'Initialized
search_unk.adb:2: (pre)- search_unk:(validity check) X'Length = 0 or X(X'First)'Initialized
search_unk.adb:2: (post)- search_unk:search_unk'Result'Initialized

Inspector generates a precondition that array X is completely initialized upon entry to Search_Unk. However, this is too strong for the function to execute safely: it would be sufficient to have X(X'First) initialized, and equal to Y.

Search_While

The same reasoning as above applies to other forms of loops. Suppose we rewrite Search using a while loop instead of a for loop:

with Assign_Arr_Unk; use Assign_Arr_Unk;
function Search_While (X : in Arr; Y : in Integer) return Integer is
   J : Integer := X'First;
begin
   while J <= X'Last loop
      if X (J) = Y then
         return J;
      end if;
      J := J + 1;
   end loop;
   return 0;
end Search_While;

On this subprogram, Inspector generates the following contract:

search_while.adb:2: (pre)- search_while:(overflow check) X'Length = 0 or X(J)'Initialized
search_while.adb:2: (pre)- search_while:(validity check) X'Length = 0 or X(X'First)'Initialized
search_while.adb:2: (pre)- search_while:(overflow check) X(X'First) = Y or X'Length = 0 or X'First /= 2_147_483_647
search_while.adb:2: (post)- search_while:search_while'Result'Initialized

Here we have one additional precondition that worries about the possibility of overflow on adding one to J, which is not an issue for "for" loops, but otherwise, we have the same contract as the one for Search_Unk.

Search_Loop

Now, we rewrite Search using an indefinite loop instead of a for loop:

with Assign_Arr_Unk; use Assign_Arr_Unk;
function Search_Loop (X : in Arr; Y : in Integer) return Integer is
   J : Integer := X'First;
begin
   loop
      if J > X'Last then
         return 0;
      end if;
      if X (J) = Y then
         return J;
      end if;
      J := J + 1;
   end loop;
end Search_Loop;

On this subprogram, Inspector generates the following contract:

search_loop.adb:2: (pre)- search_loop:(overflow check) X'Length = 0 or X(J)'Initialized
search_loop.adb:2: (pre)- search_loop:(validity check) X'Length = 0 or X(X'First)'Initialized
search_loop.adb:2: (pre)- search_loop:(overflow check) X(X'First) = Y or X'Length = 0 or X'First /= 2_147_483_647
search_loop.adb:2: (post)- search_loop:search_loop'Result'Initialized

Again, this is the same contract as the one for Search_While.

14.2.2.3. Array Increments

Assign_All_Arr

Let's consider now subprograms that iterate over arrays to increment their elements. The procedure Assign_All_Arr increments each element of its array parameter X:

with Assign_Arr; use Assign_Arr;
procedure Assign_All_Arr (X : in out Arr) is
begin
   for J in X'Range loop
      X (J) := X (J) + 1;
   end loop;
end Assign_All_Arr;

On this subprogram, Inspector generates the following contract:

assign_all_arr.adb:2: (pre)- assign_all_arr:(overflow check) X(1) /= 2_147_483_647
assign_all_arr.adb:2: (pre)- assign_all_arr:(overflow check) X(10) /= 2_147_483_647
assign_all_arr.adb:2: (pre)- assign_all_arr:(overflow check) X(2) /= 2_147_483_647
assign_all_arr.adb:2: (pre)- assign_all_arr:(overflow check) X(3) /= 2_147_483_647
assign_all_arr.adb:2: (pre)- assign_all_arr:(overflow check) X(4) /= 2_147_483_647
assign_all_arr.adb:2: (pre)- assign_all_arr:(overflow check) X(5) /= 2_147_483_647
assign_all_arr.adb:2: (pre)- assign_all_arr:(overflow check) X(6) /= 2_147_483_647
assign_all_arr.adb:2: (pre)- assign_all_arr:(overflow check) X(7) /= 2_147_483_647
assign_all_arr.adb:2: (pre)- assign_all_arr:(overflow check) X(8) /= 2_147_483_647
assign_all_arr.adb:2: (pre)- assign_all_arr:(overflow check) X(9) /= 2_147_483_647
assign_all_arr.adb:2: (post)- assign_all_arr:X(1) = X(1)'Old + 1
assign_all_arr.adb:2: (post)- assign_all_arr:X(1..10) /= -2_147_483_648
assign_all_arr.adb:2: (post)- assign_all_arr:X(10) = X(10)'Old + 1
assign_all_arr.adb:2: (post)- assign_all_arr:X(2) = X(2)'Old + 1
assign_all_arr.adb:2: (post)- assign_all_arr:X(3) = X(3)'Old + 1
assign_all_arr.adb:2: (post)- assign_all_arr:X(4) = X(4)'Old + 1
assign_all_arr.adb:2: (post)- assign_all_arr:X(5) = X(5)'Old + 1
assign_all_arr.adb:2: (post)- assign_all_arr:X(6) = X(6)'Old + 1
assign_all_arr.adb:2: (post)- assign_all_arr:X(7) = X(7)'Old + 1
assign_all_arr.adb:2: (post)- assign_all_arr:X(8) = X(8)'Old + 1
assign_all_arr.adb:2: (post)- assign_all_arr:X(9) = X(9)'Old + 1

The preconditions on lines 1 to 10 ensure that all additions on line 5 of Assign_All_Arr will not overflow. These preconditions are really the most precise ones for subprogram Assign_All_Arr, guaranteeing that no run-time error can be raised during subprogram execution.

Bad_Assign_All_Arr

Consider a version of Assign_All_Arr in which elements are shifted to the left of the array:

with Assign_Arr; use Assign_Arr;
procedure Bad_Assign_All_Arr (X : in out Arr) is
begin
   for J in X'Range loop
      X (J) := X (J + 1);
   end loop;
end Bad_Assign_All_Arr;

Inspector generates an index error because the last iteration of the loop will access past the upper bound of X:

bad_assign_all_arr.adb:2:1: high warning: subp always fails (Inspector): bad_assign_all_arr fails for all possible inputs
bad_assign_all_arr.adb:5:16: high: array index check [CWE 120] (Inspector): check fails here; requires 10 + 1 <= 10 (iteration 10 of 10)

Assign_All_Arr_Incr

Take now a slight variation over example Assign_All_Arr that increments each element by a different amount:

with Assign_Arr; use Assign_Arr;
procedure Assign_All_Arr_Incr (X : in out Arr) is
begin
   for J in X'Range loop
      X (J) := X (J) + J;
   end loop;
end Assign_All_Arr_Incr;

On this subprogram, Inspector generates the following contract:

assign_all_arr_incr.adb:2: (pre)- assign_all_arr_incr:(overflow check) X(1) /= 2_147_483_647
assign_all_arr_incr.adb:2: (pre)- assign_all_arr_incr:(overflow check) X(10) <= 2_147_483_637
assign_all_arr_incr.adb:2: (pre)- assign_all_arr_incr:(overflow check) X(2) <= 2_147_483_645
assign_all_arr_incr.adb:2: (pre)- assign_all_arr_incr:(overflow check) X(3) <= 2_147_483_644
assign_all_arr_incr.adb:2: (pre)- assign_all_arr_incr:(overflow check) X(4) <= 2_147_483_643
assign_all_arr_incr.adb:2: (pre)- assign_all_arr_incr:(overflow check) X(5) <= 2_147_483_642
assign_all_arr_incr.adb:2: (pre)- assign_all_arr_incr:(overflow check) X(6) <= 2_147_483_641
assign_all_arr_incr.adb:2: (pre)- assign_all_arr_incr:(overflow check) X(7) <= 2_147_483_640
assign_all_arr_incr.adb:2: (pre)- assign_all_arr_incr:(overflow check) X(8) <= 2_147_483_639
assign_all_arr_incr.adb:2: (pre)- assign_all_arr_incr:(overflow check) X(9) <= 2_147_483_638
assign_all_arr_incr.adb:2: (post)- assign_all_arr_incr:X(1) = X(1)'Old + 1
assign_all_arr_incr.adb:2: (post)- assign_all_arr_incr:X(1..10) /= -2_147_483_648
assign_all_arr_incr.adb:2: (post)- assign_all_arr_incr:X(10) = X(10)'Old + 10
assign_all_arr_incr.adb:2: (post)- assign_all_arr_incr:X(2) = X(2)'Old + 2
assign_all_arr_incr.adb:2: (post)- assign_all_arr_incr:X(3) = X(3)'Old + 3
assign_all_arr_incr.adb:2: (post)- assign_all_arr_incr:X(4) = X(4)'Old + 4
assign_all_arr_incr.adb:2: (post)- assign_all_arr_incr:X(5) = X(5)'Old + 5
assign_all_arr_incr.adb:2: (post)- assign_all_arr_incr:X(6) = X(6)'Old + 6
assign_all_arr_incr.adb:2: (post)- assign_all_arr_incr:X(7) = X(7)'Old + 7
assign_all_arr_incr.adb:2: (post)- assign_all_arr_incr:X(8) = X(8)'Old + 8
assign_all_arr_incr.adb:2: (post)- assign_all_arr_incr:X(9) = X(9)'Old + 9

Again, the preconditions on lines 1 to 10 ensure that all additions on line 5 of Assign_All_Arr_Incr will not overflow. These preconditions are really the most precise ones for subprogram Assign_All_Arr_Incr, guaranteeing that no run-time error can be raised during subprogram execution.

Assign_All_Arr_Incr_Unk

Take yet another variation over the previous example that uses arrays of unbounded size:

with Assign_Arr_Unk; use Assign_Arr_Unk;
procedure Assign_All_Arr_Incr_Unk (X : in out Arr) is
begin
   for J in X'Range loop
      X (J) := X (J) + J;
   end loop;
end Assign_All_Arr_Incr_Unk;

On this subprogram, Inspector generates the following contract:

assign_all_arr_incr_unk.adb:2: (pre)- assign_all_arr_incr_unk:(overflow check) X'Length = 0 or X(J)'Initialized
assign_all_arr_incr_unk.adb:2: (pre)- assign_all_arr_incr_unk:(overflow check) X'Length = 0 or X(X'First)'Initialized
assign_all_arr_incr_unk.adb:2: (pre)- assign_all_arr_incr_unk:(overflow check) X'Length = 0 or X(X'Last)'Initialized
assign_all_arr_incr_unk.adb:2: (post)- assign_all_arr_incr_unk:X(..) = One-of{X(J)'Old, (for _I in X'Range => _I + X(_I))}

Here, Inspector generates no precondition to guarantee that the addition on line 5 of Assign_All_Arr_Incr_Unk cannot overflow. However, Inspector does not issue any error on this subprogram. This is because these errors are suppressed by default, because they are likely false alarms.

Bad_Assign_All_Arr_Unk

Now take the subprogram just seen, and use an unbounded array instead:

with Assign_Arr_Unk; use Assign_Arr_Unk;
procedure Bad_Assign_All_Arr_Unk (X : in out Arr) is
begin
   for J in X'Range loop
      X (J) := X (J + 1);
   end loop;
end Bad_Assign_All_Arr_Unk;

Inspector can still detect that the last iteration accesses the array at index X'Last + 1, because it treats array bounds symbolically:

bad_assign_all_arr_unk.adb:5:16: high: array index check [CWE 120] (Inspector): check fails here; requires X'First <= J + 1 and J + 1 <= X'Last

14.2.2.4. Array Treatments

Let's consider now more general array treatments, in which subprograms iterate over arrays to update their content.

Map

Take the subprogram Map which stores in array Z an incremented version of array X:

with Assign_Arr; use Assign_Arr;
procedure Map (X : in Arr; Y : in Integer; Z : out Arr) is
begin
   for J in X'Range loop
      Z (J) := X (J) + Y;
   end loop;
end Map;

On this subprogram, Inspector generates the following contract:

map.adb:2: (pre)- map:(validity check) X(1)'Initialized
map.adb:2: (pre)- map:(validity check) X(10)'Initialized
map.adb:2: (pre)- map:(validity check) X(2)'Initialized
map.adb:2: (pre)- map:(validity check) X(3)'Initialized
map.adb:2: (pre)- map:(validity check) X(4)'Initialized
map.adb:2: (pre)- map:(validity check) X(5)'Initialized
map.adb:2: (pre)- map:(validity check) X(6)'Initialized
map.adb:2: (pre)- map:(validity check) X(7)'Initialized
map.adb:2: (pre)- map:(validity check) X(8)'Initialized
map.adb:2: (pre)- map:(validity check) X(9)'Initialized
map.adb:2: (pre)- map:(overflow check) Y + X(1) in -2_147_483_648..2_147_483_647
map.adb:2: (pre)- map:(overflow check) Y + X(10) in -2_147_483_648..2_147_483_647
map.adb:2: (pre)- map:(overflow check) Y + X(2) in -2_147_483_648..2_147_483_647
map.adb:2: (pre)- map:(overflow check) Y + X(3) in -2_147_483_648..2_147_483_647
map.adb:2: (pre)- map:(overflow check) Y + X(4) in -2_147_483_648..2_147_483_647
map.adb:2: (pre)- map:(overflow check) Y + X(5) in -2_147_483_648..2_147_483_647
map.adb:2: (pre)- map:(overflow check) Y + X(6) in -2_147_483_648..2_147_483_647
map.adb:2: (pre)- map:(overflow check) Y + X(7) in -2_147_483_648..2_147_483_647
map.adb:2: (pre)- map:(overflow check) Y + X(8) in -2_147_483_648..2_147_483_647
map.adb:2: (pre)- map:(overflow check) Y + X(9) in -2_147_483_648..2_147_483_647
map.adb:2: (post)- map:Z(1) = Y + X(1)
map.adb:2: (post)- map:Z(1..10)'Initialized
map.adb:2: (post)- map:Z(10) = Y + X(10)
map.adb:2: (post)- map:Z(2) = Y + X(2)
map.adb:2: (post)- map:Z(3) = Y + X(3)
map.adb:2: (post)- map:Z(4) = Y + X(4)
map.adb:2: (post)- map:Z(5) = Y + X(5)
map.adb:2: (post)- map:Z(6) = Y + X(6)
map.adb:2: (post)- map:Z(7) = Y + X(7)
map.adb:2: (post)- map:Z(8) = Y + X(8)
map.adb:2: (post)- map:Z(9) = Y + X(9)

The overflow check preconditions are sufficient to guarantee that the addition on line 5 of Map cannot overflow, so no messages are generated.

Concat

Consider the program Concat which takes two arrays of unbounded size in input, and returns their concatenation in array parameter Z:

with Assign_Arr_Unk; use Assign_Arr_Unk;
procedure Concat (X, Y : in Arr; Z : out Arr) is
   K : Integer := 1;
begin
   for J in X'Range loop
      Z (K) := X (J);
      K := K + 1;
   end loop;
   for J in Y'Range loop
      Z (K) := Y (J);
      K := K + 1;
   end loop;
end Concat;

On this subprogram, Inspector generates the following contract:

concat.adb:2: (pre)- concat:(overflow check) X'Length <= 2_147_483_646
concat.adb:2: (pre)- concat:(array index check) X'Length = 0 or X'Last - X'First < Z'Last
concat.adb:2: (pre)- concat:X'Length = 0 or X(J)'Initialized
concat.adb:2: (pre)- concat:(array index check) X'Length = 0 or Z'First <= 1
concat.adb:2: (pre)- concat:(array index check) X'Length = 0 or Z'First <= X'Last - X'First + 1
concat.adb:2: (pre)- concat:(array index check) X'Length = 0 or Z'Last >= 1
concat.adb:2: (pre)- concat:(aliasing check) Y'Address /= Z'Address
concat.adb:2: (pre)- concat:(overflow check) Y'Length <= 2_147_483_646
concat.adb:2: (pre)- concat:(overflow check) Y'Length = 0 or Y(J)'Initialized
concat.adb:2: (pre)- concat:(array index check) Z'Last <= X'Last - X'First + 6_442_450_942
concat.adb:2: (post)- concat:Z(..) = One-of{Z(..)'Old, (for _I in Z'Range => X((X'First + _I) - 1)), (for _I in Z'Range => Y(Y'First + (_I - K)))}

The precondition on line 4 guarantees that the assignment to Z(K) on line 6 of Concat is within bounds: either X is empty (then the loop is not executed), or it should fit in Z.

This time, when run in a deep mode, Inspector issues errors for possible index checks and overflow checks failure:

concat.adb:10:7: medium: array index check [CWE 120] (Inspector): requires K <= Z'Last
concat.adb:10:7: medium: array index check [CWE 120] (Inspector): requires Z'First <= K
concat.adb:11:14: low: overflow check [CWE 190] (Inspector): requires K /= Integer_32'Last

Concat_Op

Of course, the behavior of Concat can be obtained by simply using the Ada concatenation operator, as in subprogram Concat_Op:

with Assign_Arr_Unk; use Assign_Arr_Unk;
procedure Concat_Op (X, Y : in Arr; Z : out Arr) is
begin
   Z := X & Y;
end Concat_Op;

On this subprogram, Inspector generates the following contract:

concat_op.adb:2: (pre)- concat_op:X'First /= 2_147_483_647
concat_op.adb:2: (pre)- concat_op:(overflow check) X'Length + Y'Length in 2..4_294_967_296
concat_op.adb:2: (pre)- concat_op:X'Length in 1..4_294_967_295
concat_op.adb:2: (pre)- concat_op:Y'Length in 1..4_294_967_295
concat_op.adb:2: (post)- concat_op:possibly_updated(Z(..))

The preconditions above are not sufficient to guarantee that the bounds of Z allow such an assignment, hence the error message generated by Inspector in a deep mode:

concat_op.adb:4:11: medium: array index check [CWE 120] (Inspector): requires Z'Length = ((if X'Length + Y'Length = 0 then Y'First else if X'Length /= 0 then X'First else Y'First)..(if X'Length + Y'Length = 0 then Y'Last else if X'Length /= 0 then X'First else Y'First + X'Length + Y'Length - 1))'Length

14.2.2.5. Limitations

Rec_Constant

Although recursion and loops are in theory equivalent, Inspector treats them very differently. While the analysis of loops is carefully designed to recognize invariants over induction variables, the analysis of recursive functions may be less precise. Take as a contrived example a simple recursive function returning a constant value:

function Rec_Constant (X : in Integer) return Integer is
begin
   if X < 10 then
      return 3;
   else
      return Rec_Constant (5);
   end if;
end Rec_Constant;

On this subprogram, Inspector generates the following contract:

rec_constant.adb:1: (post)- rec_constant:rec_constant'Result'Initialized

The most precise postcondition would state that Rec_Constant always return the value 3.

Ident_Arr

Inspector can follow quite precisely the value of individual elements in an array, as well as the possible values for all other elements which are not individually tracked. This is not the same as being able to handle arbitrary quantified expressions over arrays, although in the cases of loop with static bounds, Inspector will automatically unroll these loops, leading to precise messages when the loop is not too large. Take for example a subprogram Ident_Arr that initializes an array to the identity function over its indexes:

procedure Ident_Arr (X : out Arr) is
begin
   for J in X'Range loop
      X (J) := J;
   end loop;
end Ident_Arr;

Using the aspect syntax of Ada 2012, the user can even specify a postcondition for this procedure stating the property above:

with Assign_Arr; use Assign_Arr;
procedure Ident_Arr (X : out Arr) with
  Post => (for all J in X'Range => X (J) = J);

which is proven by Inspector.

Sum_All_Arr

Inspector does not treat specially some quite useful abstractions over array content, like the sum/max/min over array elements, but again, as long as the loop has static bounds and is not too large, Inspector is able to unroll such loops and produce the most precise analysis. Consider a subprogram Sum_All_Arr which computes the sum over the elements of an array:

with Assign_Arr; use Assign_Arr;
function Sum_All_Arr (X : in Arr) return Integer is
   Sum : Integer := 0;
begin
   for J in X'Range loop
      Sum := Sum + X (J);
   end loop;
   return Sum;
end Sum_All_Arr;

Inspector will generate preconditions stating that this sum cannot overflow:

sum_all_arr.adb:2: (pre)- sum_all_arr:(overflow check) X(1) + X(2) + X(3) + X(4) + X(5) + X(6) + X(7) + X(8) + X(9) + X(10) in -2_147_483_648..2_147_483_647
sum_all_arr.adb:2: (pre)- sum_all_arr:(overflow check) X(1) + X(2) + X(3) + X(4) + X(5) + X(6) + X(7) + X(8) + X(9) in -2_147_483_648..2_147_483_647
sum_all_arr.adb:2: (pre)- sum_all_arr:(overflow check) X(1) + X(2) + X(3) + X(4) + X(5) + X(6) + X(7) + X(8) in -2_147_483_648..2_147_483_647
sum_all_arr.adb:2: (pre)- sum_all_arr:(overflow check) X(1) + X(2) + X(3) + X(4) + X(5) + X(6) + X(7) in -2_147_483_648..2_147_483_647
sum_all_arr.adb:2: (pre)- sum_all_arr:(overflow check) X(1) + X(2) + X(3) + X(4) + X(5) + X(6) in -2_147_483_648..2_147_483_647
sum_all_arr.adb:2: (pre)- sum_all_arr:(overflow check) X(1) + X(2) + X(3) + X(4) + X(5) in -2_147_483_648..2_147_483_647
sum_all_arr.adb:2: (pre)- sum_all_arr:(overflow check) X(1) + X(2) + X(3) + X(4) in -2_147_483_648..2_147_483_647
sum_all_arr.adb:2: (pre)- sum_all_arr:(overflow check) X(1) + X(2) + X(3) in -2_147_483_648..2_147_483_647
sum_all_arr.adb:2: (pre)- sum_all_arr:(overflow check) X(1) + X(2) in -2_147_483_648..2_147_483_647
sum_all_arr.adb:2: (pre)- sum_all_arr:(validity check) X(1)'Initialized
sum_all_arr.adb:2: (pre)- sum_all_arr:(validity check) X(10)'Initialized
sum_all_arr.adb:2: (pre)- sum_all_arr:(validity check) X(2)'Initialized
sum_all_arr.adb:2: (pre)- sum_all_arr:(validity check) X(3)'Initialized
sum_all_arr.adb:2: (pre)- sum_all_arr:(validity check) X(4)'Initialized
sum_all_arr.adb:2: (pre)- sum_all_arr:(validity check) X(5)'Initialized
sum_all_arr.adb:2: (pre)- sum_all_arr:(validity check) X(6)'Initialized
sum_all_arr.adb:2: (pre)- sum_all_arr:(validity check) X(7)'Initialized
sum_all_arr.adb:2: (pre)- sum_all_arr:(validity check) X(8)'Initialized
sum_all_arr.adb:2: (pre)- sum_all_arr:(validity check) X(9)'Initialized
sum_all_arr.adb:2: (post)- sum_all_arr:sum_all_arr'Result = X(1) + X(2) + X(3) + X(4) + X(5) + X(6) + X(7) + X(8) + X(9) + X(10)
sum_all_arr.adb:2: (post)- sum_all_arr:sum_all_arr'Result'Initialized

14.2.3. Pointer Examples

This section presents the results of running GNAT SAS' Inspector on subprograms containing pointers.

14.2.3.1. Dereference

Inspector assumes that the strong typing guarantees provided by Ada are not circumvented by the improper use of unchecked conversions and unchecked deallocation. In particular, it assumes that there are no dangling pointers. Thus, it is equivalent to state that pointer X can be dereferenced and that X is not null.

Deref

Consider an access type Ptr on integers, and a function Deref.Read which takes a parameter of type Ptr:

package Deref is
   type Ptr is access all Integer;
   function Read (X : in Ptr) return Integer;
end Deref;

It simply returns the value pointed to:

package body Deref is
   function Read (X : in Ptr) return Integer is
   begin
      return X.all;
   end Read;
end Deref;

On this subprogram, Inspector generates the following contract:

deref.adb:2: (pre)- deref.read:(access check) X /= null
deref.adb:2: (pre)- deref.read:(validity check) X.all'Initialized
deref.adb:2: (post)- deref.read:deref.read'Result = X.all
deref.adb:2: (post)- deref.read:deref.read'Result'Initialized

This is indeed the most precise contract for subprogram Deref.Read. The preconditions on lines 1 and 2 guarantee that no run-time error can be raised and that no uninitialized value can be read. The postcondition on line 3 completely summarizes the effect of calling Deref.Read.

Bad_Deref

Consider a version of Deref in which parameter X is an in out parameter that is always reset to null:

with Deref; use Deref;
function Bad_Deref (X : in out Ptr) return Integer is
begin
   if X /= null then
      X := null;
   end if;
   return X.all;
end Bad_Deref;

Inspector detects that X is null at the point of dereference, and it generates an error:

bad_deref.adb:2:1: high warning: subp always fails (Inspector): bad_deref fails for all possible inputs
bad_deref.adb:7:13: high: access check [CWE 476] (Inspector): check fails here; requires X /= null

Deref_Assign

Consider now subprogram Deref_Assign which updates the value pointed to by X:

with Deref; use Deref;
procedure Deref_Assign (X : in Ptr; Y : in Integer) is
begin
   X.all := Y;
end Deref_Assign;

On this subprogram, Inspector generates the following contract:

deref_assign.adb:2: (pre)- deref_assign:(access check) X /= null
deref_assign.adb:2: (post)- deref_assign:X.all = Y
deref_assign.adb:2: (post)- deref_assign:X.all'Initialized

Again, this is the most precise contract for subprogram Deref_Assign. The precondition on line 1 guarantees that no run-time error can be raised. The postcondition on line 2 completely summarizes the effect of calling Deref_Assign.

Bad_Deref_Assign

Consider a version of Deref_Assign in which some defensive code wrongly returns when parameter X is not null:

with Deref; use Deref;
procedure Bad_Deref_Assign (X : in Ptr; Y : in Integer) is
begin
   if X /= null then
      return;
   end if;
   X.all := Y;
end Bad_Deref_Assign;

Inspector detects that X is null at the point of dereference, and it generates an error:

bad_deref_assign.adb:7:6: high: access check [CWE 476] (Inspector): check fails here; requires X /= null

Self_Deref_Assign

Finally, consider the version of Self_Assign seen previously, where X is now a pointer:

with Deref; use Deref;
procedure Self_Deref_Assign (X : in out Ptr) is
begin
   X.all := X.all + 1;
end Self_Deref_Assign;

On this subprogram, Inspector generates the following contract:

self_deref_assign.adb:2: (pre)- self_deref_assign:(access check) X /= null
self_deref_assign.adb:2: (pre)- self_deref_assign:(overflow check) X.all /= 2_147_483_647
self_deref_assign.adb:2: (post)- self_deref_assign:X.all /= -2_147_483_648
self_deref_assign.adb:2: (post)- self_deref_assign:X.all = X.all'Old + 1

The preconditions on lines 1 and 2 guarantee that that no run-time error can be raised and that no uninitialized value can be read. Note that the precondition on line 2 implicitly states that X.all is initialized, since it expresses a relation involving X.all. The lines 2-4 are exactly the same as the contract previously seen for Self_Assign, where X has been replaced by X.all.

Bad_Self_Deref_Assign

Consider a version of Self_Deref_Assign in which the increment is missing:

with Deref; use Deref;
procedure Bad_Self_Deref_Assign (X : in out Ptr) is
begin
   X.all := X.all;
end Bad_Self_Deref_Assign;

Inspector detects that the assignment is useless, and in a deep mode, it generates a warning:

bad_self_deref_assign.adb:4:10: medium warning: useless reassignment [CWE 563] (Inspector): useless reassignment of X.all

14.2.3.2. Aliasing

Pointer_Assign

What makes pointers so tricky to handle in static analysis is the possibility of aliasing, where two pointers point to the same memory location. Consider the subprogram Pointer_Assign:

with Deref; use Deref;
procedure Pointer_Assign (X, Y : in Ptr) is
begin
   X.all := Y.all + 1;
end Pointer_Assign;

On this subprogram, Inspector generates the following contract:

pointer_assign.adb:2: (pre)- pointer_assign:(access check) X /= null
pointer_assign.adb:2: (pre)- pointer_assign:(access check) Y /= null
pointer_assign.adb:2: (pre)- pointer_assign:(overflow check) Y.all /= 2_147_483_647
pointer_assign.adb:2: (post)- pointer_assign:X.all /= -2_147_483_648
pointer_assign.adb:2: (post)- pointer_assign:X.all = Y.all + 1

Preconditions are the expected ones. The interesting postcondition is the one on line 5, which states the relationship between the input value of Y.all and the output value of X.all. Indeed, this is true whether X and Y are equal or not. (Note that on this example, Inspector displays Y.all for the input value pointed to by Y.)

Bad_Pointer_Assign

Consider a version of Pointer_Assign in which the user added an assertion that, after the assignment, X.all and Y.all should indeed be different:

with Deref; use Deref;
procedure Bad_Pointer_Assign (X, Y : in Ptr) is
begin
   X.all := Y.all + 1;
   pragma Assert (X.all = Y.all + 1);
end Bad_Pointer_Assign;

This is not true in the case where X and Y are equal. In a deep mode, Inspector detects this possibility, and it generates an error:

bad_pointer_assign.adb:5:19: low: assertion (Inspector): requires Y.all = Y.all
bad_pointer_assign.adb:5:33: low: overflow check [CWE 190] (Inspector): requires Y.all /= Integer_32'Last

The message indicates that the value of Y.all at subprogram entry, and the value of Y.all after the assignment, may differ. This is the case precisely when X and Y are equal.

Call_Pointer_Assign

Let's see how Inspector handles a caller of Pointer_Assign which aliases its parameters X and Y:

with Deref; use Deref;
with Pointer_Assign;
procedure Call_Pointer_Assign (X : in Ptr) is
begin
   Pointer_Assign (X, X);
end Call_Pointer_Assign;

On this subprogram, when run in a deep mode, Inspector generates the following contract:

call_pointer_assign.adb:3: (pre)- call_pointer_assign:(access check) X /= null
call_pointer_assign.adb:3: (pre)- call_pointer_assign:(overflow check) X.all /= 2_147_483_647
call_pointer_assign.adb:3: (post)- call_pointer_assign:X.all /= -2_147_483_648
call_pointer_assign.adb:3: (post)- call_pointer_assign:X.all = X.all'Old + 1

The postcondition of Pointer_Assign has lead to a similar postcondition for Call_Pointer_Assign, where Y.all has correctly been replaced with X.all'Old (and not X.all).

Double_Pointer_Assign

Consider now the subprogram Double_Pointer_Assign which assigns to both X and Y pointers:

with Deref; use Deref;
procedure Double_Pointer_Assign (X, Y : in Ptr) is
begin
   X.all := 1;
   Y.all := 2;
end Double_Pointer_Assign;

On this subprogram, Inspector generates the following contract:

double_pointer_assign.adb:2: (pre)- double_pointer_assign:(access check) X /= null
double_pointer_assign.adb:2: (pre)- double_pointer_assign:(access check) Y /= null
double_pointer_assign.adb:2: (post)- double_pointer_assign:X.all in 1..2
double_pointer_assign.adb:2: (post)- double_pointer_assign:Y.all = 2

Note the asymmetry between postconditions 3 and 4 which deal respectively with the output values of X.all and Y.all. Since Y.all is assigned last, its output value 2 comes from this last assignment. On the contrary, the output value of X.all can come either from the explicit assignment to X.all, or from the assignment to Y.all if X and Y are equal. Therefore, the postcondition on line 3 correctly considers the two output values for X.all.

The postcondition on line 3 is not the most precise postcondition, which would state in which case the value of X.all is 1 or 2:

(X /= Y and X.all = 1) or (X = Y and X.all = 2)

As already seen in section Basic Examples in the context of branchings, Inspector generates internally this more precise postcondition, from which it outputs on line 3 a more user-friendly postcondition. The internal more precise postcondition is used for analyzing callers of Double_Pointer_Assign.

Call_Double_Pointer_Assign

Take now such a caller Call_Double_Pointer_Assign, which calls Double_Pointer_Assign on non-aliased parameters:

package Call_Double_Pointer_Assign is
   X, Y : aliased Integer;   
   procedure Call;
end Call_Double_Pointer_Assign;

with Deref; use Deref;
with Double_Pointer_Assign;
package body Call_Double_Pointer_Assign is
   procedure Call is
   begin
      Double_Pointer_Assign (X'Access, Y'Access);
   end Call;
end Call_Double_Pointer_Assign;

On this subprogram, Inspector generates the following contract:

call_double_pointer_assign.adb:4: (post)- call_double_pointer_assign.call:X = 1
call_double_pointer_assign.adb:4: (post)- call_double_pointer_assign.call:Y = 2

As mentioned before, Inspector could use the more precise contract for Double_Pointer_Assign, which leads here to the precise postcondition that X has value 1 after the call.

14.2.4. Unknown Subprograms

This section presents the results of running GNAT SAS' Inspector on partial applications. It is very common to analyze a partial application, where some units are not yet implemented. This may happen either when analyzing a library, or when not having access to parts of an application (third-party development) or when analyzing an application early on, before all the code has been developed. Inspector handles these cases gracefully, by assuming that calling an unknown subprogram has some effects on its calling environment. These assumptions are precisely tuned to avoid false alarms, while keeping the analysis as precise as possible.

Call_Unknown

Take the unknown subprogram Unknown:

procedure Unknown (X : out Integer; Y : in Integer);

It is called by subprogram Call_Unknown:

with Unknown;
procedure Call_Unknown (X : out Integer) is
begin
   Unknown (X, 1);
end Call_Unknown;

On this subprogram, Inspector generates the following contract:

call_unknown.adb:2: (post)- call_unknown:X'Initialized

Because the parameter X of Unknown is marked as out, Inspector assumes that it is initialized by the call to Unknown, hence the corresponding postcondition of Call_Unknown.

Call_Unknown_Pos

Now consider a slight variation of Call_Unknown in which X is a positive integer:

with Unknown;
procedure Call_Unknown_Pos (X : out Positive) is
begin
   Unknown (X, 1);
end Call_Unknown_Pos;

On this subprogram, Inspector generates the following contract:

call_unknown_pos.adb:2: (presumption)- call_unknown_pos:unknown.X@4 >= 1
call_unknown_pos.adb:2: (post)- call_unknown_pos:X'Initialized

The postcondition on line 2 is similar to the one seen previously. What is new here is the presumption on line 1, which states that Inspector assumes that Unknown returns a positive value for X, as needed to avoid a possible run-time error in calling Unknown. Note the name X@4 is used instead of X to denote the value of X on line 4, after the call to Unknown. Since this presumption is relative to the call in Call_Unknown_Pos, it is part of the contract of Call_Unknown_Pos.

Call_Unknown_Rel

Presumptions can be more complex, for example in the subprogram Call_Unknown_Rel, an assertion requires that the value of X returned by Unknown respects a linear relation with Y:

with Unknown;
procedure Call_Unknown_Rel (X : out Integer; Y : in Integer) is
begin
   Unknown (X, Y);
   pragma Assert (X < 2 * Y + 1);
end Call_Unknown_Rel;

On this subprogram, Inspector generates the following contract:

call_unknown_rel.adb:2: (pre)- call_unknown_rel:(overflow check) Y in -1_073_741_824..1_073_741_823
call_unknown_rel.adb:2: (presumption)- call_unknown_rel:unknown.X@4 - Y*2 in -4_294_967_294..0
call_unknown_rel.adb:2: (presumption)- call_unknown_rel:unknown.X@4 /= 2_147_483_647
call_unknown_rel.adb:2: (post)- call_unknown_rel:X - Y*2 in -4_294_967_294..0
call_unknown_rel.adb:2: (post)- call_unknown_rel:X /= 2_147_483_647

The presumption on line 2 indeed propagates the desired assertion on the expected behavior of Unknown.

Call_Unknown_Arr

Inspector tries as much as possible to keep precise information through calls to unknown subprograms. Take the unknown subprogram Unknown_Arr which takes an array as in out parameter:

with Assign_Arr; use Assign_Arr;
procedure Unknown_Arr (X : in out Arr);

It is called in a context where the value of some array elements is known:

with Assign_Arr; use Assign_Arr;
with Unknown_Arr;
procedure Call_Unknown_Arr (X : in out Arr) is
begin
   X (1) := 1;
   X (4) := 2;
   Unknown_Arr (X);
end Call_Unknown_Arr;

On this subprogram, Inspector generates the following contract:

call_unknown_arr.adb:3: (post)- call_unknown_arr:X(1 | 4) = X(1 | 4)@7

Since the array is passed as in out, Inspector assumes that the value of X may change, but it keeps the information that elements at indexes 1 and 4 are initialized.

Call_Unknown_Ptr

This is even more visible in the way Inspector analyzes calls to unknown subprograms which take pointers in parameter, like Unknown_Ptr:

with Deref; use Deref;
procedure Unknown_Ptr (X : in out Ptr);

It is called twice, first in a context where the value of parameter X.all is not known, then in a context where it is known:

with Deref; use Deref;
with Unknown_Ptr;
procedure Call_Unknown_Ptr (X, Y : in out Ptr) is
begin
   Unknown_Ptr (X);
   Y.all := 1;
   Unknown_Ptr (Y);
   pragma Assert (X.all < Y.all);
end Call_Unknown_Ptr;

On this subprogram, Inspector generates the following contract:

call_unknown_ptr.adb:3: (pre)- call_unknown_ptr:(access check) Y /= null
call_unknown_ptr.adb:3: (presumption)- call_unknown_ptr:unknown_ptr.X@5 /= null
call_unknown_ptr.adb:3: (presumption)- call_unknown_ptr:unknown_ptr.X@5.all /= 2_147_483_647
call_unknown_ptr.adb:3: (presumption)- call_unknown_ptr:unknown_ptr.X@5.all < unknown_ptr.X@7.all
call_unknown_ptr.adb:3: (presumption)- call_unknown_ptr:unknown_ptr.X@7 /= null
call_unknown_ptr.adb:3: (presumption)- call_unknown_ptr:unknown_ptr.X@7.all /= -2_147_483_648
call_unknown_ptr.adb:3: (post)- call_unknown_ptr:X /= null
call_unknown_ptr.adb:3: (post)- call_unknown_ptr:Y /= null
call_unknown_ptr.adb:3: (post)- call_unknown_ptr:Y.all = 1

The presumption on line 4 shows that Inspector assumes that the first call to Unknown_Ptr (on line 5 of Call_Unknown_Ptr) returns a value for X.all that is less than the value of Y.all returned by the second call to Unknown_Ptr (on line 7 of Call_Unknown_Ptr) as specified by the following assertion.

Note that the postconditions on line 7 and 8 are derived from presumptions.

Above_Call_Unknown

In general, the exact constraint expected from a call to an unknown subprogram may not be given by its direct caller, but possibly by a caller higher in the call chain. Inspector handles these cases by generating presumptions on unknown subprograms in the contract of these indirect callers. Consider a caller of the subprogram Call_Unknown, which expects X to be different from 10 after the call:

with Call_Unknown;
procedure Above_Call_Unknown (X : out Integer) is
begin
   Call_Unknown (X);
   pragma Assert (X /= 10);
end Above_Call_Unknown;

On this subprogram, Inspector generates the following contract:

above_call_unknown.adb:2: (presumption)- above_call_unknown:unknown.X@4 /= 10
above_call_unknown.adb:2: (post)- above_call_unknown:X /= 10

The presumption on line 1 indeed requires that the call to Unknown inside Call_Unknown returns a value different from 10. Since this presumption is relative to the call in Call_Unknown inside a call in Above_Call_Unknown, it is part of the contract of Above_Call_Unknown.

14.3. Infer's Limitations and Heuristics

Since Infer is a static analysis framework, it can use different analyses to emit different messages, and each analysis can have distinct limitations. The following table summarizes these limitations:

Message kinds	Limitations and heuristics
access check, memory leak, use after free, function with side effects, function with side effects in conditional	The checker typically doesn't follow all paths through the subprogram and can thus miss errors.
unitialized value passed to	The checker is intraprocedural and field-insensitive. It only checks whether any field of a composite type object is written before the object is passed as an IN or IN-OUT parameter to a call. Consequently, it misses issues when the written field is not the one that is later read. The checker doesn't emit messages on tagged types primitives and null records.
write without open, read without open, double open, close without open	The checker is intraprocedural, meaning messages are emitted only for problems in a single subprogram.