Extend AST for Regular Commands with instructions that work on heap memory

[Yurand2000]

A new set of atomic commands needs to be included in the analisys tool:

• Memory Allocation alloc(x) or x := alloc() where x is a variable
• Memory Deallocation free(x) where x is a variable
• Memory Reading x = [y] where x and y are variables
• Memory Writing [x] = a where x is a variable and a is an arithmetic expression

Note that the memory must be accessed only through variables and not through arithmetic expressions which compute the memory location, this is to simplify the analisys rules. Pointer arithmetic and similar can be simulated using more commands. Example: x = [y + 1] becomes z = y + 1; x = [z]

[Yurand2000]

We are still missing the non-deterministic assignment operator, which we have discussed to be a separate atomic command rather than an expression: x = nondet() or nondet(x)