Symbolic Heap Syntax

Attestor supports a limited fragment of symbolic heap separation logic with inductive predicate definitions to provide initial states. The syntax of these symbolic heaps is as follows:

PREDICATE( VAR{TYPE}, ..., VAR{TYPE} ) <= VAR{TYPE}, ..., VAR{TYPE} | FORMULA

Here, PREDICATE is a predicate symbol consisting of a non-empty string of letters and digits. Moreover, VAR{TYPE} declares a variable named VAR of type TYPE, i.e. TYPE corresponds to the class or primitive data type of objects or values that may be assigned to variable VAR. Variables left of <= correspond to free variables of PREDICATE and will be interpreted as program variables. Variables declared right of <= and left of | are interpreted as existentially quantified variables. The delimiter | is omitted if no variables are existentially quantified.

The symbolic heap itself is given by the FORMULA afterwards, which is defined according to the following context-free grammar:

FORMULA ::= VAR.FIELD -> VAR | VAR.FIELD -> null | FORMULA * FORMULA | VAR = VAR | VAR = CONST | PRED(VAR (, VAR)*)

Here, VAR corresponds to the name of a previously declared variable, FIELD is an identifier of a selector, null is a constant referring to the null reference, and CONST refers to constants null, or numerical constants such as 0, -1, or 1. Finally, PRED(VAR (,VAR)*) denotes a call of predicate PRED with the provided comma-separated list of parameters. Please notice that dangling pointers are not supported.