Interface SetType

All Superinterfaces:
All Known Subinterfaces:

public interface SetType extends Type

A set type is the type for expressions that represent sets of objects. A set type has an element type which is an instance of an ObjectType (see also elementType()).

The construction of a set type expression is defined in ACSL v1.16 "Sec. 2.3.4 Memory locations and sets of terms". see also SetTypeAnalyzer.

Expressions of set-of NON POINTER type cannot be used in other places than the argument lists of ACSL assigns, loop assigns or CIVL-C POR contract reads clauses.

Expressions of set-of POINTER type can only be used in places where a $mem type object is needed.

There is an implicit type conversion from SetType with element of pointer type to MemType. see MemConversion.

  • Method Details

    • elementType

      ObjectType elementType()
      the element type of this set type; will not be null , MemType or SetType.