History log of /seL4-l4v-master/l4v/tools/autocorres/tests/proof-tests/nested_struct.c
Revision Date Author Comments
# 092b1207 18-Apr-2020 Gerwin Klein <gerwin.klein@data61.csiro.au>

run astyle on all C files in the repository

Leaves parse tests and generated files unchanged, and provides a style
filter for these.

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>


# a424d55e 09-Mar-2020 Gerwin Klein <gerwin.klein@data61.csiro.au>

licenses: convert license tags to SPDX


# e83be48e 10-Apr-2015 Japheth Lim <Japheth.Lim@nicta.com.au>

autocorres: activate regression test for nested struct access (VER-321).


# 7cc357e0 01-Sep-2014 Japheth Lim <Japheth.Lim@nicta.com.au>

autocorres: translate accesses to nested structs correctly. See tests/proof-tests/nested_struct.thy.

This should (finally) close issue JIRA VER-321. Unfortunately it also breaks some other things,
such as heap_abs_syntax, which we'll need to examine later.