Closed Yurand2000 closed 5 months ago
A note on the previously mentioned logic operators (some to remove, some to add):
x -> _
is actually equal to ∃v. x -> v
, so the second case is useless.x -/>
which represents that the memory pointed by x
has been deallocated.
A new set of logic operators needs to be included in the analysis tool:
empH
No memory is allocated.x -> a
wherex
is a variable anda
an arithmetic expression. The memory pointed byx
has the valuea
x -> _
wherex
is a variable. The memory pointed byx
is allocated.P * Q
whereP
andQ
are logic formulas. There exists a disjoint partition of heap memoryh1
,h2
which verifies the formulaP
on heapleth1
and formulaQ
on heapleth2
.