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 /riscV | |
| 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 'riscV')
0 files changed, 0 insertions, 0 deletions