aboutsummaryrefslogtreecommitdiffstats
path: root/coq
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-09-07 19:35:02 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2015-09-07 19:35:02 +0200
commit73e20bd6e0586e38fbc7d87d8c306fad7b578418 (patch)
tree3b4ffcfd6ab4df231a2fa66716fa58b4d5ab1b76 /coq
parent76d82e41797ef79531e6bf3d530f380dddd3310e (diff)
downloadcompcert-73e20bd6e0586e38fbc7d87d8c306fad7b578418.tar.gz
compcert-73e20bd6e0586e38fbc7d87d8c306fad7b578418.zip
Added builtins for call frame and return address.
This builtins can be used to get the call frame address and the return address. To correctly compute the load address of the return address the allocframe is extended to contain the offset of the return address.
Diffstat (limited to 'coq')
0 files changed, 0 insertions, 0 deletions