Lattice cluster_control Control cluster_integer Integer cluster_pointer Pointer = nullability × struct type cluster_struct Struct named collection of named scalar types cluster_memory Memory precise alias slices cluster_tuple Tuple collection of types TOP ⊤ XCTRL ⊤:ctrl TOP->XCTRL INT_TOP ⊤:int TOP->INT_TOP PTR_TOP ⊤:ptr [*⊤:struct] TOP->PTR_TOP STRUCT_TOP ⊤:struct [struct top] TOP->STRUCT_TOP MEM_TOP ⊤:mem TOP->MEM_TOP TUPLE_TOP ⊤:tuple TOP->TUPLE_TOP BOT ⊥ CTRL ⊥:ctrl XCTRL->CTRL CTRL->BOT INT_NEG … −2, −1 INT_TOP->INT_NEG INT_ZERO 0 INT_TOP->INT_ZERO INT_POS 1, 2, … INT_TOP->INT_POS INT_BOT ⊥:int INT_BOT->BOT INT_NEG->INT_BOT INT_ZERO->INT_BOT INT_POS->INT_BOT PTR_NULL null PTR_TOP->PTR_NULL PTR_PERSON *Person PTR_TOP->PTR_PERSON PTR_S1 *s1 PTR_TOP->PTR_S1 PTR_MORE *s2, … PTR_TOP->PTR_MORE PTR_BOT ⊥:ptr [*⊥:struct?] PTR_BOT->BOT PTR_PERSON_NIL *Person? PTR_NULL->PTR_PERSON_NIL PTR_S1_NIL *s1? PTR_NULL->PTR_S1_NIL PTR_MORE_NIL *s2?, … PTR_NULL->PTR_MORE_NIL PTR_ANY *⊥:struct [ptr any struct] PTR_ANY->PTR_BOT PTR_PERSON->PTR_ANY PTR_PERSON->PTR_PERSON_NIL PTR_S1->PTR_ANY PTR_S1->PTR_S1_NIL PTR_MORE->PTR_ANY PTR_MORE->PTR_MORE_NIL PTR_PERSON_NIL->PTR_BOT PTR_S1_NIL->PTR_BOT PTR_MORE_NIL->PTR_BOT STRUCT_PERSON Person age: int STRUCT_TOP->STRUCT_PERSON STRUCT_S1 s1 x: int STRUCT_TOP->STRUCT_S1 STRUCT_S2 s2 x: int, y: int STRUCT_TOP->STRUCT_S2 STRUCT_MORE … STRUCT_TOP->STRUCT_MORE STRUCT_BOT ⊥:struct [struct bottom] STRUCT_BOT->BOT STRUCT_PERSON->STRUCT_BOT STRUCT_S1->STRUCT_BOT STRUCT_S2->STRUCT_BOT STRUCT_MORE->STRUCT_BOT MEM_ALIAS2 MEM#2 MEM_TOP->MEM_ALIAS2 MEM_ALIAS3 MEM#3 MEM_TOP->MEM_ALIAS3 MEM_MORE … MEM_TOP->MEM_MORE MEM_BOT ⊥:mem MEM_BOT->BOT MEM_ALIAS2->MEM_BOT MEM_ALIAS3->MEM_BOT MEM_MORE->MEM_BOT TUPLE1 tuple type TUPLE_TOP->TUPLE1 TUPLE2 tuple type type TUPLE_TOP->TUPLE2 TUPLEN tuple type … type TUPLE_TOP->TUPLEN TUPLE_BOT ⊥:tuple TUPLE_BOT->BOT TUPLE1->TUPLE_BOT TUPLE2->TUPLE_BOT TUPLEN->TUPLE_BOT