Update ora submodule; carefully suppress warnings; fix a couple of br…

…oken proofs.
PrincetonUniversity · May 13, 2024 · 4e34ca8 · 4e34ca8
1 parent 0acc02a
commit 4e34ca8
Showing 13 changed files with 22 additions and 6 deletions.
diff --git a/floyd/Component.v b/floyd/Component.v
@@ -1,4 +1,6 @@
+Set Warnings "-custom-entry-overridden".
 Require Import VST.floyd.proofauto.
+Set Warnings "custom-entry-overridden".
 Require Import VST.veric.Clight_initial_world.
 Require Import VST.floyd.assoclists.
 Require Import VST.floyd.PTops.

diff --git a/floyd/QPcomposite.v b/floyd/QPcomposite.v
@@ -1,4 +1,6 @@
+Set Warnings "-hiding-delimiting-key,-custom-entry-overridden,-notation-overridden".
 Require Import VST.floyd.base.
+Set Warnings "hiding-delimiting-key,custom-entry-overridden,notation-overridden".
 Require Import VST.floyd.PTops.
 
 Local Unset SsrRewrite.

diff --git a/floyd/quickprogram.v b/floyd/quickprogram.v
@@ -1,4 +1,6 @@
+Set Warnings "-hiding-delimiting-key,-custom-entry-overridden,-notation-overridden".
 Require Import VST.floyd.base.
+Set Warnings "hiding-delimiting-key,custom-entry-overridden,notation-overridden".
 Require Import VST.floyd.PTops.
 Require Import VST.floyd.QPcomposite.
 Import -(notations) compcert.lib.Maps.

diff --git a/ora b/ora
diff --git a/progs/os_combine.v b/progs/os_combine.v
@@ -142,7 +142,7 @@ Section ext_trace.
   Proof.
     intros.
     eapply whole_program_sequential_safety_ext in EXIT as (b & q & ? & ? & Hsafe); eauto.
-    2: { intros; apply CSHL_Sound.semax_prog_sound, H. }
+    2: { intros; eexists; apply CSHL_Sound.semax_prog_sound, H. }
     do 3 eexists; eauto; split; eauto; intros n.
     eapply dry_safe_ext_trace_safe; eauto.
   Qed.

diff --git a/progs/verif_io_mem.v b/progs/verif_io_mem.v
@@ -593,7 +593,7 @@ Proof.
   - apply io_spec_sound.
     intros ?? [<- | [<- | ?]]; last done;
       rewrite /ext_link /ext_link_prog /prog /=; repeat (if_tac; first done); done.
-  - intros; apply CSHL_Sound.semax_prog_sound, prog_correct.
+  - intros; eexists; apply CSHL_Sound.semax_prog_sound, prog_correct.
   - apply (proj2_sig init_mem_exists).
   - exists q.
     rewrite (proj2_sig main_block_exists) in Hb; inv Hb.

diff --git a/progs64/VSUpile/Makefile b/progs64/VSUpile/Makefile
@@ -38,7 +38,7 @@ OFILES = $(patsubst %.c,%.o,$(CFILES))
 VOFILES = $(patsubst %.v,%.vo,$(CVFILES) $(VFILES))
 
 
-VST_DIRS= msl sepcomp veric zlist floyd
+VST_DIRS= msl shared sepcomp veric zlist floyd
 VSTFLAGS= -R $(VST_LOC)/compcert compcert $(foreach d, $(VST_DIRS), -Q $(VST_LOC)/$(d) VST.$(d)) -R . pile
 
 

diff --git a/progs64/os_combine.v b/progs64/os_combine.v
@@ -142,7 +142,7 @@ Section ext_trace.
   Proof.
     intros.
     eapply whole_program_sequential_safety_ext in EXIT as (b & q & ? & ? & Hsafe); eauto.
-    2: { intros; apply CSHL_Sound.semax_prog_sound, H. }
+    2: { intros. eexists.  apply CSHL_Sound.semax_prog_sound, H. }
     do 3 eexists; eauto; split; eauto; intros n.
     eapply dry_safe_ext_trace_safe; eauto.
   Qed.

diff --git a/progs64/verif_io_mem.v b/progs64/verif_io_mem.v
@@ -593,7 +593,7 @@ Proof.
   - apply io_spec_sound.
     intros ?? [<- | [<- | ?]]; last done;
       rewrite /ext_link /ext_link_prog /prog /=; repeat (if_tac; first done); done.
-  - intros; apply CSHL_Sound.semax_prog_sound, prog_correct.
+  - intros; eexists; apply CSHL_Sound.semax_prog_sound, prog_correct.
   - apply (proj2_sig init_mem_exists).
   - exists q.
     rewrite (proj2_sig main_block_exists) in Hb; inv Hb.

diff --git a/veric/Clight_Cop2.v b/veric/Clight_Cop2.v
@@ -19,7 +19,9 @@
 
 Require Export VST.veric.Cop2.
 Require Import VST.veric.Clight_base.
+Set Warnings "-custom-entry-overridden".
 Require Import VST.veric.tycontext.
+Set Warnings "custom-entry-overridden".
 
 (** * Type classification and semantics of operators. *)
 

diff --git a/veric/NullExtension.v b/veric/NullExtension.v
@@ -1,10 +1,14 @@
 Require Import VST.sepcomp.extspec.
 Require Import VST.sepcomp.step_lemmas.
 Require Import VST.veric.base.
+Set Warnings "-custom-entry-overridden".
 Require Import VST.veric.juicy_extspec.
+Set Warnings "custom-entry-overridden".
 Require Import VST.veric.juicy_mem.
 Require Import VST.veric.mpred.
+Set Warnings "-hiding-delimiting-key,-notation-overridden".
 Require Import VST.veric.external_state.
+Set Warnings "hiding-delimiting-key,notation-overridden".
 Require Import VST.veric.compspecs.
 Require Import VST.veric.semax_prog.
 Require Import VST.veric.SequentialClight.

diff --git a/veric/SequentialClight.v b/veric/SequentialClight.v
@@ -4,13 +4,15 @@ Require Import VST.veric.Clight_core.
 Require Import VST.veric.Clight_lemmas.
 Require Import VST.sepcomp.step_lemmas.
 Require Import VST.sepcomp.event_semantics.
+Set Warnings "-hiding-delimiting-key,-custom-entry-overridden,-notation-overridden".
 Require Import VST.veric.Clight_evsem.
 Require Import VST.veric.SeparationLogic.
 Require Import VST.veric.juicy_extspec.
 Require Import VST.veric.juicy_mem.
 Require Import VST.veric.SeparationLogicSoundness.
 Require Import iris_ora.logic.wsat.
 Require Import iris_ora.logic.fancy_updates.
+Set Warnings "hiding-delimiting-key,custom-entry-overridden,notation-overridden".
 Require Import VST.sepcomp.extspec.
 
 Import VericSound.

diff --git a/veric/mpred.v b/veric/mpred.v
@@ -413,7 +413,9 @@ Proof. intros.  exists (assert_of P). reflexivity. Qed.
 
 Fail Example bi_of_assert'_test : forall (P Q : assert'), P ∗ Q ⊢ Q ∗ P.
 Program Definition bi_assert (P : assert) : bi_car assert := {| monPred_at := P |}.
+Set Warnings "-uniform-inheritance".
 Global Coercion bi_assert : assert >-> bi_car.
+Set Warnings "uniform-inheritance".
 (* "Print Coercion Paths assert' bi_car" prints "[assert_of; bi_assert]" *)
 Example test : forall (P Q : assert'), P ∗ Q ⊢ Q ∗ P. 
 Proof. intros. rewrite bi.sep_comm. done. Qed.