Ecosyste.ms: Issues

An open API service for providing issue and pull request metadata for open source projects.

GitHub / PrincetonUniversity/VST issues and pull requests

#797 - Prototype of RefinedVST frontend.

Pull Request - State: closed - Opened by rinshankaihou about 1 month ago

#796 - Sassign example mostly working

Pull Request - State: closed - Opened by rinshankaihou about 2 months ago

#795 - Update github actions artifact to version 4.1.7

Pull Request - State: closed - Opened by andrew-appel about 2 months ago

#794 - Adapt to https://github.com/coq/coq/pull/19530

Pull Request - State: closed - Opened by proux01 about 2 months ago - 5 comments

#793 - Bump actions/download-artifact from 2 to 4.1.7 in /.github/workflows

Pull Request - State: closed - Opened by dependabot[bot] 2 months ago - 2 comments
Labels: dependencies

#792 - Trying to prove properties about eBPF programs (Clightgen issue)

Issue - State: open - Opened by swarnpriya 3 months ago - 7 comments

#791 - can frame affine props in lithium

Pull Request - State: closed - Opened by rinshankaihou 3 months ago

#790 - More typing example

Pull Request - State: closed - Opened by rinshankaihou 3 months ago

#789 - repr_inj_signed64 has incorrect bounds.

Issue - State: open - Opened by roconnor-blockstream 3 months ago

#788 - R vst

Pull Request - State: closed - Opened by rinshankaihou 3 months ago

#787 - Adapt w.r.t. coq/coq#19228.

Pull Request - State: closed - Opened by ppedrot 3 months ago - 2 comments

#786 - merge VST into OpenMP

Pull Request - State: closed - Opened by ducthann 3 months ago - 1 comment

#785 - port everything for lithium

Pull Request - State: closed - Opened by rinshankaihou 4 months ago

#784 - port some automation related files and a bit of program.v

Pull Request - State: closed - Opened by rinshankaihou 4 months ago

#783 - updated mailbox to use new lock_t

Pull Request - State: closed - Opened by mansky1 4 months ago - 2 comments

#782 - mailbox broken: typedef with/without *

Issue - State: closed - Opened by andrew-appel 4 months ago - 2 comments

#781 - Port VST 2.x to CompCert master

Pull Request - State: closed - Opened by andrew-appel 4 months ago - 3 comments

#780 - Vstoniris

Pull Request - State: closed - Opened by sgacs 4 months ago

#779 - CompCert planned change: adding a `Mbool` memory chunk

Issue - State: closed - Opened by xavierleroy 5 months ago - 6 comments

#778 - simpl_classes.v

Pull Request - State: closed - Opened by sgacs 5 months ago - 2 comments

#777 - build: support PROFILING and TIMED like coq_makefile

Pull Request - State: closed - Opened by SkySkimmer 5 months ago

#776 - Vst on iris

Pull Request - State: closed - Opened by sgacs 5 months ago

#775 - Create simpl_classes.v

Pull Request - State: closed - Opened by sgacs 5 months ago

#774 - Wrap functor facts in abstract lemmas.

Pull Request - State: closed - Opened by ppedrot 6 months ago

#773 - In VST 3.0beta2, normalize1 tactic

Issue - State: open - Opened by andrew-appel 6 months ago - 6 comments

#772 - check_parameter_vals should have lazymatch

Issue - State: open - Opened by andrew-appel 6 months ago

#769 - verif_incr should prove that it restores an uninitialized counter

Issue - State: open - Opened by andrew-appel 7 months ago - 1 comment

#766 - change_compspecs adjusts cstring

Pull Request - State: closed - Opened by andrew-appel 7 months ago

#764 - cstring should not need a compspecs argument

Issue - State: closed - Opened by andrew-appel 7 months ago - 2 comments

#763 - mkVSU external function check does not give useful error message

Issue - State: closed - Opened by andrew-appel 8 months ago - 3 comments

#762 - inhabited_value doesn't really work well

Issue - State: open - Opened by andrew-appel 8 months ago

#761 - Adapt to Coq 8.19 and CompCert 3.13.1

Pull Request - State: closed - Opened by andrew-appel 8 months ago

#760 - Please create a tag for Coq 8.19 in Coq Platform 2024.01

Issue - State: closed - Opened by rtetley 8 months ago - 4 comments

#758 - Improved, more precise fix for issue #756

Pull Request - State: closed - Opened by andrew-appel 8 months ago

#756 - localize / entailer_for_load_tac / unlocalize / Coq 8.17

Issue - State: closed - Opened by andrew-appel 8 months ago - 11 comments

#755 - VST on Iris

Pull Request - State: open - Opened by mansky1 8 months ago - 9 comments

#754 - Fix issue #745

Pull Request - State: closed - Opened by andrew-appel 8 months ago

#752 - solve_store_rule_evaluation

Issue - State: closed - Opened by andrew-appel 9 months ago - 1 comment

#751 - Improvements in deadvars

Issue - State: closed - Opened by andrew-appel 9 months ago

#750 - forward_call takes a long time

Issue - State: closed - Opened by rigille 9 months ago - 2 comments

#749 - data_at_int_or_ptr_int share

Issue - State: closed - Opened by andrew-appel 9 months ago

#748 - solve_load_rule_evaluation @proj_reptype

Issue - State: closed - Opened by andrew-appel 11 months ago - 3 comments

#747 - Adapt to https://github.com/coq/coq/pull/18164

Pull Request - State: closed - Opened by proux01 12 months ago - 2 comments

#745 - overbroad match in try_conjuncts

Issue - State: closed - Opened by andrew-appel about 1 year ago

#744 - fail levels in forward_if'_new

Issue - State: closed - Opened by andrew-appel about 1 year ago

#743 - Unnecessary premise in `Lemma field_at_app`

Issue - State: closed - Opened by MSoegtropIMC about 1 year ago

#742 - Tactic & example fixes

Pull Request - State: closed - Opened by rinshankaihou about 1 year ago

#741 - repr_inj handles int64 compares better; updated submodules

Pull Request - State: closed - Opened by andrew-appel about 1 year ago

#740 - VSTlib: adapt to gentype branch of vcfloat

Pull Request - State: closed - Opened by andrew-appel about 1 year ago

#739 - Adjusted SC_tac, adjusted change_compspecs warning message, store_tac

Pull Request - State: closed - Opened by andrew-appel about 1 year ago - 2 comments

#738 - do {S} while (0)

Issue - State: open - Opened by andrew-appel about 1 year ago

#737 - Vst on iris

Pull Request - State: closed - Opened by rinshankaihou about 1 year ago

#736 - Vst on iris

Pull Request - State: closed - Opened by rinshankaihou about 1 year ago

#735 - Vst on iris

Pull Request - State: closed - Opened by rinshankaihou about 1 year ago

#734 - Useful lemma for users: nonempty_writable_glb

Issue - State: closed - Opened by andrew-appel about 1 year ago

#733 - vst_on_iris floyd fixes

Pull Request - State: closed - Opened by rinshankaihou about 1 year ago

#732 - New lemma data_at_conflict_glb

Pull Request - State: closed - Opened by andrew-appel about 1 year ago - 1 comment

#731 - removed a call to try simple apply eq_refl in SC_tac

Pull Request - State: closed - Opened by lennartberinger about 1 year ago - 1 comment

#730 - Vst on iris

Pull Request - State: closed - Opened by rinshankaihou about 1 year ago

#729 - Some observations on `forward_call` performance

Issue - State: closed - Opened by MSoegtropIMC about 1 year ago - 21 comments

#727 - Please create a tag for Coq 8.18 in Coq Platform 2023.10

Issue - State: closed - Opened by rtetley about 1 year ago - 5 comments

#726 - Have coqdep use DEPFLAGS not COQFLAGS

Pull Request - State: closed - Opened by proux01 about 1 year ago - 3 comments

#725 - Honor COQEXTRAFLAGS env var

Pull Request - State: closed - Opened by proux01 about 1 year ago - 1 comment

#724 - Added Lemma init_data_tarray_tint

Pull Request - State: closed - Opened by lennartberinger about 1 year ago

#723 - don't clear in quick_typecheck3; closes #722

Pull Request - State: closed - Opened by andrew-appel about 1 year ago

#722 - quick_typecheck3 should not clear

Issue - State: closed - Opened by andrew-appel about 1 year ago - 2 comments

#721 - sumarray fixes

Pull Request - State: closed - Opened by rinshankaihou about 1 year ago

#720 - Vst on iris

Pull Request - State: closed - Opened by rinshankaihou about 1 year ago

#719 - verif_append2.v done

Pull Request - State: closed - Opened by rinshankaihou about 1 year ago

#718 - fix lemma statement

Pull Request - State: closed - Opened by rinshankaihou about 1 year ago

#717 - bug fixes in floyd

Pull Request - State: closed - Opened by rinshankaihou about 1 year ago

#714 - Pass `COQEXTRAFLAGS` through to `coqc`

Pull Request - State: closed - Opened by JasonGross about 1 year ago - 1 comment

#712 - Ltac2 local2ptree

Pull Request - State: open - Opened by MSoegtropIMC about 1 year ago - 14 comments

#711 - fix issues #700 and #702

Pull Request - State: closed - Opened by andrew-appel about 1 year ago

#709 - Pass stderr through calc_install_files when commands fail

Pull Request - State: open - Opened by JasonGross about 1 year ago - 2 comments

#708 - Pass along `IGNORECOMPCERTVERSION` to `calc_install_files`

Pull Request - State: closed - Opened by JasonGross about 1 year ago

#707 - Add some generated zlist files to .gitignore

Pull Request - State: closed - Opened by JasonGross about 1 year ago

#705 - Don't try to install `msl/LICENSE`

Pull Request - State: closed - Opened by JasonGross about 1 year ago

#703 - Make `util/make_version` more POSIX-compliant

Pull Request - State: closed - Opened by JasonGross about 1 year ago

#701 - Fix issues in list solver

Pull Request - State: closed - Opened by bcip about 1 year ago

#700 - field_compatible0_Tarray_offset

Issue - State: closed - Opened by andrew-appel over 1 year ago

#687 - Update fcf to master branch

Pull Request - State: closed - Opened by andrew-appel over 1 year ago

#674 - future-coercion-class-field warning

Issue - State: closed - Opened by andrew-appel over 1 year ago - 3 comments

#664 - list_solve problems with sorted lists

Issue - State: closed - Opened by andrew-appel almost 2 years ago - 3 comments

#653 - list_solve no longer solves a goal

Issue - State: closed - Opened by joscoh almost 2 years ago - 4 comments