From 6a05fbf4b55dfdf2884c3e0b2cb57d707ad1598d Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 24 Mar 2020 23:53:42 +0100 Subject: Asmgenproof1 --- aarch64/Asmgenproof1.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'aarch64/Asmgenproof1.v') diff --git a/aarch64/Asmgenproof1.v b/aarch64/Asmgenproof1.v index 4da1b52b..bd1474b6 100644 --- a/aarch64/Asmgenproof1.v +++ b/aarch64/Asmgenproof1.v @@ -1932,7 +1932,9 @@ Proof. { destruct (rs base); try discriminate. simpl in *. rewrite Ptrofs.of_int64_to_int64 by auto. auto. } destruct offset_representable. - econstructor; econstructor; split. apply exec_straight_opt_refl. auto. -- exploit (exec_loadimm64 X16); eauto. intros (rs' & A & B & C). +- exploit (exec_loadimm64 X16); eauto. + simpl. congruence. + intros (rs' & A & B & C). econstructor; econstructor; split. apply exec_straight_opt_intro; eexact A. split. simpl. rewrite B, C by eauto with asmgen. auto. auto. Qed. -- cgit