Merge pull request #767 from PrincetonUniversity/VSU_Drysafe

Initial version of proof connecting VSU system to VST+Compcert soundn…
PrincetonUniversity · Apr 16, 2024 · 8d35137 · 8d35137
2 parents 13c4289 + 6c8bcfd
commit 8d35137
Show file tree

Hide file tree

Showing 3 changed files with 1,081 additions and 1 deletion.
diff --git a/Makefile b/Makefile
@@ -504,7 +504,7 @@ FLOYD_FILES= \
    for_lemmas.v semax_tactics.v diagnosis.v simple_reify.v simpl_reptype.v \
    freezer.v deadvars.v Clightnotations.v unfold_data_at.v hints.v reassoc_seq.v \
    SeparationLogicAsLogicSoundness.v SeparationLogicAsLogic.v SeparationLogicFacts.v \
-   subsume_funspec.v linking.v data_at_lemmas.v Funspec_old_Notation.v assoclists.v VSU.v quickprogram.v PTops.v Component.v QPcomposite.v \
+   subsume_funspec.v linking.v data_at_lemmas.v Funspec_old_Notation.v assoclists.v VSU.v VSU_DrySafe.v quickprogram.v PTops.v Component.v QPcomposite.v \
    data_at_list_solver.v step.v fastforward.v finish.v
 #real_forward.v