diff options
author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2020-03-02 10:41:11 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-02 10:41:11 +0100 |
commit | f8d3d265f6ef967acf6eea017cb472809096a135 (patch) | |
tree | 7db8cc57526c0d679962e03f4a0d9654d113e1db /lib/Parmov.v | |
parent | 8587b8310a91702e2635a689e1622a87b7bf8985 (diff) | |
download | compcert-f8d3d265f6ef967acf6eea017cb472809096a135.tar.gz compcert-f8d3d265f6ef967acf6eea017cb472809096a135.zip |
Define the semantics of `free(NULL)` (#226)
According to ISO C, `free(NULL)` is correct and does nothing.
This commit updates accordingly the formal semantics of the `free`
external function and the reference interpreter.
Closes: #334
Diffstat (limited to 'lib/Parmov.v')
0 files changed, 0 insertions, 0 deletions