Value Analysis Alarms

When the value analysis results are available, the generated alarms can be found in the Properties array, or in the Tis-info About Properties results. In both cases, a column gives the alarm kind, and the following sections give information about each kind of alarm that can be generated by the value analysis. The alarm kind also appear in the name of the generated assertions as illustrated in the examples below.

To learn how to deal with these alarms, refer to the Study the Alarms section of the TrustInSoft Analyzer Manual.

Division_by_zero

When dividing by an expression that the analysis is not able to guarantee non-null, a proof obligation is emitted. This obligation expresses that the divisor is different from zero at this point of the code.

In the particular case where zero is the only possible value for the divisor, the analysis stops the propagation of this execution path. If the divisor seems to be able to take non-null values, the analyzer is allowed to take into account the property that the divisor is different from zero when it continues the analysis after this point. The property expressed by an alarm may also not be taken into account when it is not easy to do so.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
unsigned int A;
unsigned int B;
void main(unsigned int x, unsigned int y)
{
  /*@ assert Value: division_by_zero: (unsigned int)(x*y) ≢ 0; */
  A = 100u / (x * y);
  /*@ assert Value: division_by_zero: x ≢ 0; */
  B = 333u % x;
  return;
}

In the above example, there is no way for the analyzer to guarantee that x*y is not null, so it emits an alarm at line 5. In theory, it could avoid emitting the alarm x != 0 at line 7 because this property is a consequence of the property emitted as an alarm at line 7. Redundant alarms happen – even in cases simpler than this one. Do not be surprised by them.

Division_overflow

According to the ISO/IEC 9899:2011 standard, paragraph 6.5.5:6:

When integers are divided, the result of the / operator is the algebraic quotient with any fractional part discarded. If the quotient a/b is representable, the expression (a/b)*b + a%b shall equal a; otherwise, the behavior of both a/b and a%b is undefined.

So an alarm is emitted when b is -1 and a is the smallest negative value of its type, as shown in this example:

1
2
3
4
5
6
7
8
int G;
void main(int x, int y)
{
  if (y < 0) 
    /*@ assert Value: division_overflow: x ≢ -2147483648 ∨ y ≢ -1; */
    G = x % y;
  return;
}

Memory Accesses

Whenever the value analysis is not able to establish that a dereferenced pointer is valid, it emits an alarm that expresses that the pointer needs to be valid at that point. This alarm can be Memory_access or Index_out_of_bound as shown below.

The choice between these two kinds of alarms is influenced by option -unsafe-arrays.

Memory_access

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
int t[10];
void main(int c)
{
  int *p;
  p = & t[5];
  if (c) 
    /*@ assert Value: mem_access: \valid(p+7); */
    *(p + 7) = c;
  *(p + -3) = c;
  return;
}

In the above example, the analysis is not able to guarantee that the memory accesses *(p + 7) at line 8 is valid, so it emits a proof obligation. Notice that no alarm is emitted for *(p + -3) validity at line 9, as the analysis is able to guarantee that this always holds.

Index_out_of_bound

Memory problem

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
int t[10];
void main(int c)
{
  int i;
  i = 0;
  while (i <= 10) {
    if (i < c) 
      /*@ assert Value: index_bound: i < 10; */
      t[i] = i;
    i ++;
  }
  return;
}

In the above example, the analysis is not able to guarantee that the memory accesses t[i] at line 9 is valid, so it emits a proof obligation. Notice that no alarm is emitted for 0 <= i at line 9 as the analysis is able to guarantee that this always holds.

Overflow in array accesses

The value analysis assumes that when an array access occurs in the analyzed program, the intention is that the accessed address should be inside the array. If it can not determine that this is the case, it emits an out of bounds index alarm. This leads to an alarm on the following example:

int t[10][10];
int main(void)
{
  int __retres;
  /*@ assert Value: index_bound: 12 < 10; */
  __retres = t[0][12];
  return __retres;
}

The value analysis assumes that writing t[0][...], the programmer intended the memory access to be inside t[0]. Consequently, it emits an alarm.

The option -unsafe-arrays tells the value analysis to warn only if the address as computed using its modelization of pointer arithmetics is invalid. With the option, the value analysis does not warn about line 6 and assumes that the programmer was referring to the cell t[1][2].

The default behavior is stricter than necessary but often produces more readable and useful alarms. To reiterate, in this default behavior the value analysis gets hints from the syntactic shape of the program. Even in the default mode, it does not warn for the following code:

int *p=&t[0][12];
return *p;

Logic_memory_access

This alarm is very similar to the Memory_access one except that it is used for library internal built-ins such as memset as shown in the example below.

void main(unsigned int i)
{
  char t[10];
  if (i < (unsigned int)10) 
    /*@ assert
        Value: logic_mem_access: \valid(&t[i]+(0 .. (unsigned int)10-1));
    */
    memset((void *)(& t[i]),5,(size_t)10);
  __tis_globfini();
  return;
}

Valid_string

Like Logic_memory_access, this alarm is emitted when using library internal built-ins such as strlen as shown in the example below.

int main(char *str)
{
  int __retres;
  size_t tmp;
  /*@ assert Value: valid_string: \points_to_valid_string((void *)str); */
  tmp = strlen((char const *)str);
  __retres = (int)tmp;
  __tis_globfini();
  return __retres;
}

Valid_wstring

Similar to Valid_string, but for strings of wchar.

Comparable_char_blocks

This \comparable_char_blocks(ptr1, ptr2, size) alarm is emitted when there might be some invalid contents in a call to memcmp() (uninitialized memory, dangling pointers, or addresses: called incomparable content below).

The expected behavior is like this:

  • If a buffer contains incomparable bytes but a difference is certain to occur before this happens, no alarm is emitted. Note that some incomparable bytes are allowed to occur after a difference because that seemed the most useful in practice and the standard is not so explicit.
  • If there appears to be a risk that memcmp() consumes a byte of incomparable bytes then the alarm \comparable_char_blocks is emitted. This alarm says that these bytes should not be incomparable or should not be consumed by memcmp().
  • Beside this alarm, a \valid_read(ptr1+(0 .. size-1)) alarm can also be emitted if the values of ptr1 and size seem like they can be such that memcmp() makes an invalid memory access. Note that memcmp() requires the entire range to be valid even if a difference occurs before the end of the buffers (see technical article: memcmp requires pointers to fully valid buffers).
  • Furthermore, a line in the log is emitted if size is zero and ptr1 can be an invalid pointer, because this is a constraint imposed by the standard that is not captured by \valid_read(ptr1+(0 ..  size-1)).

Comparable_wchar_blocks

Similar to Comparable_char_blocks, but for wchar blocks.

Invalid_shift

Another arithmetic alarm is the alarm emitted for logical shift operations on integers where the second operand may be larger than the size in bits of the first operand’s type. Such an operation is left undefined by the ISO/IEC 9899:1999 standard, and indeed, processors are often built in a way that such an operation does not produce the -0 or -1 result that could have been expected. Here is an example of program with such an issue, and the resulting alarm:

void main(int c)
{
  int x;
  unsigned int tmp;
  {
    if (c) tmp = (unsigned int)1; else tmp = (unsigned int)8 * sizeof(int);
    c = (int)tmp;
  }
  /*@ assert Value: shift: 0 ≤ c < 32; */
  x = 1 << c;
  return;
}

Pointer_comparison

Proof obligations can also be emitted for pointer comparisons whose results may vary from one compilation to another, such as &a < &b or &x+2 != NULL. These alarms do not necessarily correspond to run-time errors, but relying on an undefined behavior of the compiler is in general undesirable (although this one is rather benign for current compilation platforms).

Although these alarms may seem unimportant, they should still be checked, because the value analysis may reduce the propagated states accordingly to the emitted alarm. For instance, for the &x+2 != NULL comparison, after emitting the alarm that the quantity &x+2 must be reliably comparable to 0, the analysis assumes that the result of the comparison is 1. The consequences are visible when analyzing the following example:

int x;
int y;
int *p;
void main(void)
{
  p = & x;
  while (1) {
    /*@ assert
        Value: ptr_comparison: \pointer_comparable((void *)p, (void *)(&y));
    */
    if (! (p != & y)) break;
    p ++;
  }
  return;
}

The value analysis finds that this program does not terminate. This seems incorrect because an actual execution will terminate on most architectures. However, the value analysis’ conclusion is conditioned by an alarm emitted for the pointer comparison.

The value analysis only allows pointer comparisons that give reproducible results — that is, the possibility of obtaining an unspecified result for a pointer comparison is considered as an unwanted error, and is excluded by the emission of an alarm.

The analyzer can be instructed to propagate past these undefined pointer comparisons with option -undefined-pointer-comparison-propagate-all. With this option, in the example program above, the values 0 and 1 are considered as results for the condition as soon as p becomes an invalid address. Therefore, the value analysis does not predict that the program does not terminate.

Differing_blocks

This alarm is emitted on subtractions between two pointers that may not point to the same allocated block. The example below shows the generated assertion:

int main(int *p1, int *p2)
{
  int __retres;
  /*@ assert Value: differing_blocks: \base_addr(p2) ≡ \base_addr(p1); */
  __retres = p2 - p1;
  return __retres;
}

Notice that this alarm is only emitted when the -val-warn-pointer-subtraction option is set (set by default, but can be cleared with -no-val-warn-pointer-subtraction).

Overflow

By default, the value analysis emits alarms for - and reduces the sets of possible results of - signed arithmetic computations where the possibility of an overflow exists. Indeed, such overflows have an undefined behavior according to paragraph 6.5.5 of the ISO/IEC 9899:1999 standard. The example below shows the generated assertions:

int G;
void main(int x, int y)
{
  /*@ assert Value: signed_overflow: -2147483648 ≤ x+y; */
  /*@ assert Value: signed_overflow: x+y ≤ 2147483647; */
  G = x + y;
  return;
}

If useful, it is also possible to assume that signed integers overflow according to a 2’s complement representation. The option -no-warn-signed-overflow can be used to this end. A reminder message is nevertheless emitted operations that are detected as potentially overflowing.

Regardless of the value of option -warn-signed-overflow, a warning is emitted on signed arithmetic operations applied to the cast to signed int of an address, since the compiler may place variables in memory at will.

By default, no alarm is emitted for arithmetic operations on unsigned integers for which an overflow may happen, since such operations have defined semantics according to the ISO/IEC 9899:1999 standard. If one wishes to signal and prevent such unsigned overflows, option -warn-unsigned-overflow can be used.

Finally, no alarm is emitted for downcasts to signed or unsigned integers. In the signed case, the least significant bits of the original value are used, and are interpreted according to 2’s complement representation. TrustInSoft Analyzer’s options -warn-signed-downcast and -warn-unsigned-downcast are not honored by the value analysis. The RTE plug-in can be used to generate the relevant assertions before starting an analysis.

Float_to_int

An alarm is emitted when a floating-point value appears to exceed the range of the integer type it is converted to.

int main(void)
{
  int __retres;
  float f;
  f = tis_float_interval((float)2e9,(float)3e9);
  /*@ assert
      Value: float_to_int: \is_finite(f) ∧ -2147483649 < f < 2147483648;
  */
  __retres = (int)f;
  __tis_globfini();
  return __retres;
}

The results also show the final possible values:

f ∈ [2000000000. .. 3000000000.]
__retres ∈ [2000000000..2147483647]

Not_separated

The C language allows compact notations for modifying a variable that is being accessed (for instance, y = x++;). The effect of these pre- or post-increment (or decrement) operators is undefined when the variable is accessed elsewhere in the same statement. For instance, y = x + x++; is undefined: the code generated by the compiler may have any effect, and especially not the effect expected by the programmer.

Sometimes, it is not obvious whether the increment operation is defined. In the example y = *p + x++;, the post-increment is defined as long as *p does not have any bits in common with x.

When the -unspecified-access option is used, the Not_separated alarm is emitted when the read/write accesses occurring between sequence points are not proved to be separated. There is for instance a problem in the following example:

int main(int x, int y)
{
    int * p = (x < y) ? &x : &y;
    return x + (*p)++;
}

An assertion is emitted to show that the code execution is only specified if p does not point on x because otherwise, x would be both read and write in the statement.

int main(int x, int y)
{
  int __retres;
  int *p;
  int *tmp;
  int tmp_0;
  int tmp_1;
  if (x < y) tmp = & x; else tmp = & y;
  p = tmp;
  /*@ assert Value: separation: \separated(p, &x); */
  {
    {
      {
        tmp_0 = *p;
        /*@ assert Value: signed_overflow: *p+1 ≤ 2147483647; */
        tmp_1 = *p + 1;
      }
      *p = tmp_1;
    }
    ;
  }
  /*@ assert Value: signed_overflow: -2147483648 ≤ x+tmp_0; */
  /*@ assert Value: signed_overflow: x+tmp_0 ≤ 2147483647; */
  __retres = x + tmp_0;
  __tis_globfini();
  return __retres;
}

Overlap

Vaguely related to, but different from, undefined side-effects in expressions, the value analysis warns about the following program:

struct S {
   int a ;
   int b ;
   int c ;
};
struct T {
   int p ;
   struct S s ;
};
union U {
   struct S s ;
   struct T t ;
};
union U u;
void copy(struct S *p, struct S *q)
{
  /*@ assert Value: overlap: p ≡ q ∨ \separated(p, q); */
  *p = *q;
  return;
}

int main(int c, char **v)
{
  int __retres;
  u.s.b = 1;
  copy(& u.t.s,& u.s);
  __retres = (u.t.s.a + u.t.s.b) + u.t.s.c;
  return __retres;
}

The programmer thought ey was invoking implementation-defined behavior in the above program, using an union to type-pun between structs S and T. Unfortunately, this program returns 1 when compiled with clang -m32; it returns 2 when compiled with clang -m32 -O2, and it returns 0 when compiled with gcc -m32.

For a program as simple as the above, all these compilers are supposed to implement the same implementation-defined choices. Which compiler, if we may ask such a rhetorical question, is right? They all are, because the program is undefined. When function copy() is called from main(), the assignment *p = *q; breaks C99’s 6.5.16.1:3 rule. This rule states that in an assignment from lvalue to lvalue, the left and right lvalues must overlap either exactly or not at all.

The program breaking this rule means compilers neither have to emit warnings (none of the above did) nor produce code that does what the programmer intended, whatever that was. On the above program, the value analysis has generated an overlap alarm , and moreover it reported:

partially overlapping lvalue assignment (u with offsets {32}, size <96> bits; u with offsets {0}, size <96> bits).

By choice, the value analysis does not emit alarms for overlapping assignments of size less than int, for which reading and writing are deemed atomic operations. Finding the exact cut-off point for these warnings would require choosing a specific compiler and looking at the assembly it generates for a large number of C constructs. This kind of fine-tuning of the analyzer for a specific target platform and compiler can be provided as a paying service.

Dangling and Uninitialized pointers

An alarm may be emitted if the application appears to read the value of a local variable that has not been initialized, or if it appears to manipulate the address of a local variable outside of the scope of said variable as shown on examples below.

By default, the value analysis does not emit an alarm for a copy from memory to memory when the copied values include dangling addresses or uninitialized contents. This behavior is safe because the value analysis warns later, as soon as an unsafe value is used in a computation –either directly or after having been copied from another location. The copy operations for which alarms are not emitted are assignments from lvalues to lvalues (lv1 = lv2;), passing lvalues as arguments to functions (f(lv1);), and returning lvalues (return lv1;). An exception is made for lvalues passed as arguments to library functions: in this case, because the function’s code is missing, there is no chance to catch the undefined access later; the analyzer emits an alarm at the point of the call.

The behavior documented above was implemented to avoid spurious warnings where the copied lvalues are structs or unions. In some cases, it may be normal for some fields in a struct or union to contain such dangerous contents. Option -val-warn-copy-indeterminate can be used to obtain a more aggressive behavior. Specifying -val-warn-copy-indeterminate f on the command-line will cause the analyzer to also emit an alarm on all dangerous copy operations occurring in function f, as long as the copied lvalues are not structs or unions. The syntax @all can also be used to activate this behavior for all functions.

Initialization

1
2
3
4
5
6
7
8
9
int main(int c)
{
  int r;
  int t;
  if (c) r = 2;
  /*@ assert Value: initialisation: \initialized(&r); */
  t = r + 3;
  return t;
}

The value analysis emits alarms for line 7 since the variable r may be uninitialized.

Dangling

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
int *f(int c)
{
  int *__retres;
  int t;
  t = c;
  __retres = & t;
  return __retres;
}

int main(int c)
{
  int __retres;
  int *p;
  p = f(c);
  /*@ assert Value: dangling_pointer: ¬\dangling(&p); */
  __retres = *p;
  return __retres;
}

The value analysis emits alarms for line 16 since a dangling pointer to local variable t is used.

Is_nan_or_infinite

When it appears that a floating-point operation can result in an infinite value or NaN, the analyzer emits an alarm that excludes these possibilities, and continues the analysis with an interval representing the result obtained if excluding these possibilities. This interval, like any other result, may be over-approximated. An example of this first kind of alarm can be seen in the following example.

double main(double a, double b)
{
  double __retres;
  /*@ assert Value: is_nan_or_infinite: \is_finite((double)(a+b)); */
  __retres = a + b;
  return __retres;
}

An alarm is also emitted when the program uses as argument to a floating-point operation a value from memory that does not ostensibly represent a floating-point number. This can happen with a union type with both int and float fields, or in the case of a conversion from int* to float*. The emitted alarm excludes the possibility of the bit sequence used as a the argument representing NaN, an infinite, or an address. See the example below.

union __anonunion_bits_1 {
   int i ;
   float f ;
};
union __anonunion_bits_1 bits;
/*@ assigns generated: \result;
    assigns \result \from \nothing; */
int unknown_fun(void);

float r;
int main(void)
{
  int __retres;
  bits.i = unknown_fun();
  /*@ assert Value: is_nan_or_infinite: \is_finite(bits.f); */
  r = (float)(1.0 + (double)bits.f);
  __retres = (double)r > 0.;
  return __retres;
}

Function_pointer

When a function pointer is dereferenced, the pointed function must have a type that matches the type of the pointer. The example below may seem OK on a platform where int and float have the same width, but the ABI can still indicate that float and int arguments should be passed through different registers, leading the function f to read from a floating-point register that has not been set up by the call site.

int f(int i)
{
  int __retres;
  __retres = i + 1;
  return __retres;
}

float (*p)(float);
float r;
int main(void)
{
  int __retres;
  p = (float (*)(float))(& f);
  /*@ assert Value: function_pointer: \valid_function(p); */
  r = (*p)(1.0f);
  __retres = 0;
  return __retres;
}

An alarm is emitted, indicating that since *p is being applied with type float(float), the function of which p contains the address should have that type.

Index_in_address

An index expression under the & (address-of) operator must be in the valid range for the array being accessed (even though the & means the access does not take place). It is legal to refer to &(t[10]) when t is an array of size 10 (“pointer one past the last element”). This nuance makes this alarm different from the Index_out_of_bound one, for which the memory access takes place immediately and no such exception is allowed.

Pointer_arithmetic

Pointer arithmetic should only be applied to a pointer to an object, and the pointer should stay within the object (with a single exception for pointing one past the last element). Specifying the option -val-warn-pointer-arithmetic-out-of-bounds on the command-line will cause the analyzer to emit an alarm on all operations that compute pointers out of bounds. An example of this first kind of alarm can be seen in the following example.

char t[10];
void main(int c)
{
  char *buf;
  int parsed;
  buf = t;
  parsed = 10;
  buf += parsed;
  /*@ assert Value: pointer_arithmetic: \inside_object((void *)(buf+1)); */
  buf ++;
  return;
}

The alarm \inside_object((void *)(buf+1)) is emitted, indicating that buf+1 leads to a pointer that does not stay within the object. Note that, when the option -allow-null-plus-zero is set, the alarm \inside_object_or_null((void *)(buf+1)) is emitted, indicating that buf+1 leads to a pointer that neither stays within the object nor is null.

Bad_libc_call

This alarm is automatically emitted on library function calls that have a definition in the standard library when their definition caused at least one alarm. Alarms within the standard library are the consequences of imprecise or incorrect calls to one of the library functions.

UB_annotation

This alarm is emitted when an annotation has the UB label and cannot be verified.

Unclassified

Potential undefined behaviors are reported in this category whenever, they do not belong to any other category. They are emitted as the uninterpreted ACSL \\warning(s) predicate where s is a string describing the undefined behavior.