aboutsummaryrefslogtreecommitdiffstats
path: root/common/Sections.mli
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2014-12-17 10:36:41 +0100
committerXavier Leroy <xavier.leroy@inria.fr>2014-12-17 10:36:41 +0100
commit9a0cc571c98ca2ce41891c09c24aabfea4bfe639 (patch)
tree6f58b49a3bd0deca774bcfca553dfe6551462ba9 /common/Sections.mli
parent2d3330d132b22db7dd44399e0aac6e9e60470f59 (diff)
downloadcompcert-kvx-9a0cc571c98ca2ce41891c09c24aabfea4bfe639.tar.gz
compcert-kvx-9a0cc571c98ca2ce41891c09c24aabfea4bfe639.zip
Prototype the pointer so that the program has well defined semantics and passes the reference interpreter.
Diffstat (limited to 'common/Sections.mli')
0 files changed, 0 insertions, 0 deletions