# 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; void main(int c) { int *p; p = & t; 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; 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;
int main(void)
{
int __retres;
/*@ assert Value: index_bound: 12 < 10; */
__retres = t;
return __retres;
}
```

The value analysis assumes that writing `t[...]`, the programmer intended the memory access to be inside `t`. 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`.

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;
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;
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: 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.

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;
__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.

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)` 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;
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.

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.