| commit | ab7a70089011bf3c834f9a16ae6a594956cbe45a | |
| author | Sven Verdoolaege <skimo@kotnet.org> | |
| Thu, 8 Aug 2013 12:50:08 +0000 (8 14:50 +0200) | ||
| committer | Sven Verdoolaege <skimo@kotnet.org> | |
| Wed, 16 Oct 2013 13:22:18 +0000 (16 15:22 +0200) | ||
| tree | a06223c4913f95edcbaaa24b6688c3787a5a7735 | treesnapshot (tar.gz zip) |
| parent | e1a954c2e22b17c952aacc9b40f6093ae783c265 | commitdiff |
add support for structs
A member access is represented by an index expression and access
relation with a wrapped range. The domain of the wrapped range
represents the structure, while the range of the wrapped range
represents the member. The domain may in turn be a wrapped relation
in case of nested member accesses.
For example, an access of the form
s.f[i].a[j]
is represented as
{ S_0[i, j] -> s_f_a[s_f[s[] -> f[i]] -> a[j]] }
We also keep track of all the structure definitions involved
as some users may need to print these definitions.
Signed-off-by: Sven Verdoolaege <skimo@kotnet.org>
A member access is represented by an index expression and access
relation with a wrapped range. The domain of the wrapped range
represents the structure, while the range of the wrapped range
represents the member. The domain may in turn be a wrapped relation
in case of nested member accesses.
For example, an access of the form
s.f[i].a[j]
is represented as
{ S_0[i, j] -> s_f_a[s_f[s[] -> f[i]] -> a[j]] }
We also keep track of all the structure definitions involved
as some users may need to print these definitions.
Signed-off-by: Sven Verdoolaege <skimo@kotnet.org>
30 files changed: