Skip to content

Pull requests: PrincetonUniversity/VST

New pull request New
Clear current search query, filters, and sorts
6 Open 483 Closed
6 Open 483 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

can frame affine props in lithium
#791 by rinshankaihou was merged Aug 29, 2024 Loading…
More typing example
#790 by rinshankaihou was merged Aug 21, 2024 Loading…
R vst
#788 by rinshankaihou was merged Aug 12, 2024 Loading…
Adapt w.r.t. coq/coq#19228.
#787 by ppedrot was merged Aug 9, 2024 Loading…
2
merge VST into OpenMP
#786 by ducthann was closed Aug 6, 2024 Loading…
1
port everything for lithium
#785 by rinshankaihou was merged Jul 31, 2024 Loading…
port some automation related files and a bit of program.v
#784 by rinshankaihou was merged Jul 30, 2024 Loading…
updated mailbox to use new lock_t
#783 by mansky1 was closed Jul 26, 2024 Loading…
1
2
Port VST 2.x to CompCert master
#781 by andrew-appel was merged Jul 28, 2024 Loading…
3
Vstoniris
#780 by sgacs was closed Jul 18, 2024 Loading…
simpl_classes.v
#778 by sgacs was closed Jul 11, 2024 Loading…
2
build: support PROFILING and TIMED like coq_makefile
#777 by SkySkimmer was merged Jun 12, 2024 Loading…
Vst on iris
#776 by sgacs was closed Jun 6, 2024 Loading…
Create simpl_classes.v
#775 by sgacs was closed Jul 11, 2024 Loading…
Wrap functor facts in abstract lemmas.
#774 by ppedrot was merged May 31, 2024 Loading…
Changed definition of valid_pointer' wrt locations with PURE resource…
#771 by lennartberinger was merged May 30, 2024 Loading…
Ported progs64/VSUpile from compcert 3.8 to 3.13, ported proofs, and …
#768 by lennartberinger was merged Apr 16, 2024 Loading…
Initial version of proof connecting VSU system to VST+Compcert soundn…
#767 by lennartberinger was merged Apr 16, 2024 Loading…
change_compspecs adjusts cstring
#766 by andrew-appel was merged Apr 9, 2024 Loading…
1
improved VSU diagnostics; better support for initialized cstring
#765 by andrew-appel was merged Apr 8, 2024 Loading…
Adapt to Coq 8.19 and CompCert 3.13.1
#761 by andrew-appel was merged Mar 20, 2024 Loading…
Added a slightly stronger lemma HORec_sub, plus some earlier changes wrt sc_tac
#759 by lennartberinger was merged Mar 17, 2024 Loading…
Improved, more precise fix for issue #756
#758 by andrew-appel was merged Mar 13, 2024 Loading…
Patch to partially address issue #756 (localize/unlocalize/quick_typecheck3)
#757 by andrew-appel was merged Mar 8, 2024 Loading…
Fix issue #745
#754 by andrew-appel was merged Mar 4, 2024 Loading…
ProTip! Filter pull requests by the default branch with base:master.