Value Analysis Alarms¶

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.

 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;
}

 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;
}

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

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

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;
}

void main(void)
{
  char t[10];
  char *s;
  s = (char *)0;
  /*@ assert Value: logic_mem_access: \valid_read(s); */
  memcpy((void *)(t), (void const *)s, (size_t)0);
  __tis_globfini();
  return;
}

#include <stdlib.h>
#include <string.h>

char const *src[10];

int populate(void *tgt, size_t len) {    
    if (!tgt && (len > 0)) { return 1; }

    memcpy(tgt, src, len); 
    if (!tgt) { return 42; }    
    return 0;
}

/*@ assert Value: logic_mem_access: \valid((char *)tgt); */

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;
}

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: unclassified:
          \warning("Conditional branch depends on garbled mix value that depends on the memory layout .");
    */
    /*@ assert
        Value: unclassified:
          \warning("pointer comparison requires valid pointers: \\inside_object_or_null((int *)p).");
    */
    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.

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.

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 they were 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.

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;
}

 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;
}

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.