From 94558ecb3e48261f12c644045d40c7d0784415e0 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 2 Mar 2020 11:39:06 +0100 Subject: 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). --- common/Events.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'common') 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. -- cgit