diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-03-02 11:39:06 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-03-02 11:39:06 +0100 |
| commit | 94558ecb3e48261f12c644045d40c7d0784415e0 (patch) | |
| tree | 4ea87a06512b930f1c8d7c9f02f1a350ed99cc2d /common | |
| parent | f8d3d265f6ef967acf6eea017cb472809096a135 (diff) | |
| download | compcert-94558ecb3e48261f12c644045d40c7d0784415e0.tar.gz compcert-94558ecb3e48261f12c644045d40c7d0784415e0.zip | |
Define the semantics of `free(NULL)`, continued
The proof script for Events.excall_free_ok was incomplete
if Archi.ptr64 is unknown (as in the RISC-V case).
Diffstat (limited to 'common')
| -rw-r--r-- | common/Events.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/common/Events.v b/common/Events.v index 022adaef..28bb992a 100644 --- a/common/Events.v +++ b/common/Events.v @@ -1150,7 +1150,7 @@ Proof. - assert (t1 = t2) by (inv H; inv H0; auto). subst t2. exists vres1; exists m1; auto. (* determ *) -- inv H; inv H0; try (unfold Vnullptr in *; discriminate). +- inv H; inv H0; try (unfold Vnullptr in *; destruct Archi.ptr64; discriminate). + assert (EQ1: Vptrofs sz0 = Vptrofs sz) by congruence. assert (EQ2: sz0 = sz). { unfold Vptrofs in EQ1; destruct Archi.ptr64 eqn:SF. |