Module BufferOverrunDomain.AliasTarget

The value of alias target is exactly the same to the alias key.

The value of alias target is less than or equal to the alias key. For example, if there is an alias between %r and size(x)+i with the Le type, it means size(x)+i <= %r.

Since Sil distinguishes logical and program variables, we need a relation for pruning values of program variables. For example, a C statement if(x){...} is translated to %r=load(x); if(%r){...} in Sil. At the load statement, we record the alias between the values of %r and x, then we can prune not only the value of %r, but also that of x inside the if branch. The java_tmp field is an additional slot for keeping one more alias of temporary variable in Java. The i field is to express %r=load(x)+i.

For pruning vector.length with vector::empty() results, we adopt a specific relation between %r and v->elements, where %r=v.empty(). So, if %r!=0, v's array length (v->elements->length) is pruned by =0. On the other hand, if %r==0, v's array length is pruned by >=1.

This is for pruning vector's length. When there is a function call, %r=x.size(), the alias target for %r becomes AliasTarget.size {l=x.elements}. The java_tmp field is an additional slot for keeping one more alias of temporary variable in Java. The i field is to express %r=x.size()+i, which is required to follow the semantics of Array.add inside loops precisely.

This is for pruning return values of fgets. If the result of fgets is not null, the length of return value will be pruned to greater than or equal to 1.

This is for tracking a relation between an iterator offset and an integer value. If %r has an alias to IteratorSimple {l; i}, which means that %r's iterator offset is same to l.

This is for tracking a relation between an iterator offset and the length of the underlying collection. If %r has an alias to IteratorOffset {l; i}, which means that %r's iterator offset is same to length(l)+i.

This is for tracking return values of the hasNext function. If %r has an alias to HasNext {l}, which means that %r is same to l.hasNext().

This is for tracking the return values of nextObject function. If %r has an alias to nextObject {l}, which means that %r is the same to l.nextObject().