# 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¶

Calls to library functions exhibit undefined behavior if any of their arguments have invalid values (unless invalid values are explicitly allowed). Invalid values are those of unexpected types, values outside a given function’s domain, pointers outside the program’s address space, null pointers, non-const pointers to non-modifiable storage, and others (see C17 §7.1.4p1 for details).

The logic_mem_access alarm occurs when value analysis is unable to conclude that a dereferenced pointer is valid when used as arguments to library-internal builtins, such as memset, memcpy, memcmp, and similar (see Standard library functions). The alarm is analogous to Memory_access except that it involves a call to a library-internal built-in.

Representative examples follow.

#### Invalid memory access \valid_read(src + …)¶

This example shows an invalid use of the library-internal builtin memset. The memset builtin populates an area of memory of a given length and starting at a specified location with some constant. In the example, memset is called to populate an area of memory within the array t, starting at offset i (where i < 10), up to the length 10, with the constant 5.

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


The emitted alarm shows a violation with respect to memset, which requires the entire extent of memory to be valid. This means that the addresses between &t[i] and &t[i] + (10 - 1) are required to be valid. However, an inspection of the example reveals that since t is a ten-element array, the call to memset is not valid for any i greater than 0.

#### Apparently benign behavior \valid_read(src)¶

This example shows a use of the builtin memcpy. This builtin copies a specified number of bytes from one memory area to another, non-overlapping memory area. In this example memcpy is called to populate an area of memory within the ten-element character array t from the pointer s which is currently set to NULL, but the number of elements copied from s to t is zero.

void main(void)
{
char t;
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;
}


Since the number of bytes to copy from s to t is zero, it is commonly believed that no problem should occur, since an implementation of memset would not attempt to access t in such a case.

However, the analyzer emits an alarm indicating that passing a pointer to memory which cannot be read to memset is undefined behavior regardless. The standard specifies that arguments to standard library functions must have valid values (C17 §7.1.4p1). It is also specific that when a pointer and length pair describing an array are passed as arguments to standard library functions from <string.h>, the pointer must have a valid value, even if the length is zero (C17 §7.24.1p2).

Compilers can rely on this definition to introduce optimizations. As an example, the following function populate copies len bytes from the array src to the area of memory pointed to by the variable tgt. The function guards against a situation where tgt is null and len non-zero, but if len is zero, the function can call memcpy irrespective of tgt being NULL. The function then returns 42 if tgt is NULL.

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

char const *src;

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

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


Since memcpy receives NULL as an argument, the analyzer finds an undefined behavior here:

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


This undefined behavior manifests a practical consequence for the programmer. Since the standard allows the compiler to assume that any pointer passed to memcpy is valid, it can use this fact as a basis for optimization. Specifically, gcc (v. 12.2 running with -O3 on x84-64) produces output that omits the check for tgt being NULL after the call to memcpy and the associated instructions returning the value 42 (see here for details). If tgt cannot be invalid when calling memcpy, it follows that tgt cannot be NULL in the following condition as well. Thus, the compiler treats the condition as dead code and omits it, causing likely undesirable behavior. This means that if tgt is NULL and len is zero, the behavior of the function may change and either return 0 or 42 depending on compilers and applied optimizations.

### 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.

## 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.

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.

### 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.