PrincetonUniversity/VST issues and pull requests

#626 - Software Foundations vol 5 - Verifiable C expects VST 2.10 but Coq platform has VST 2.9

Issue - State: closed - Opened by ghulette about 2 years ago - 1 comment

#596 - Remove old OPAM dev entry

Issue - State: closed - Opened by QinshiWang over 2 years ago - 1 comment

#361 - Makefile bug for progs/pile data abstraction example

Issue - State: closed - Opened by dnaumann over 5 years ago - 1 comment

#295 - Pretty-printing of Clight uses wrong subscopes

Issue - State: open - Opened by andrew-appel about 6 years ago - 2 comments

#100 - Extend the max number of variables allowed in 'WITH' clause.

Pull Request - State: closed - Opened by lastland about 7 years ago

#99 - A few of the progs/ now have nontrivial _main postconditions

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

#98 - Fix bug tc environ

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

#97 - Fix bug in tc_environ

Pull Request - State: closed - Opened by QinxiangCao about 7 years ago

#96 - fix markdown formatting for "Build" in readme

Pull Request - State: closed - Opened by andres-erbsen about 7 years ago

#95 - Added string library examples.

Pull Request - State: closed - Opened by mansky1 about 7 years ago

#94 - Rmaps are no longer required to be cancelative or cross-splittable.

Pull Request - State: closed - Opened by mansky1 about 7 years ago

#93 - Qualified path names now start with VST.floyd, VST.veric, etc.,

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

#92 - Small change

Pull Request - State: closed - Opened by QinxiangCao about 7 years ago

#91 - Canon semax return

Pull Request - State: closed - Opened by QinxiangCao about 7 years ago - 1 comment

#90 - Redundent type-checking in sem_shift

Issue - State: closed - Opened by QinxiangCao over 7 years ago - 2 comments

#89 - Small change for go_lower

Pull Request - State: closed - Opened by QinxiangCao over 7 years ago - 1 comment

#88 - Adding new files containing only definitions and result.

Pull Request - State: closed - Opened by adampetcher over 7 years ago

#87 - Made with_library much faster, especially the version in floyd/library.v

Pull Request - State: closed - Opened by andrew-appel over 7 years ago - 1 comment

#86 - Improved an error message in with_library, to fix issue #63

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

#85 - More integrated load

Pull Request - State: closed - Opened by QinxiangCao over 7 years ago

#84 - Andrew

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

#83 - More integrated load rule

Pull Request - State: closed - Opened by QinxiangCao over 7 years ago

#82 - Improve dep

Pull Request - State: closed - Opened by QinxiangCao over 7 years ago - 1 comment

#81 - Makefile requires CONFIGURE for personnal configuration.

Pull Request - State: closed - Opened by ildyria over 7 years ago

#80 - Andrew

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

#79 - Request for a -ignore-coq-version option

Issue - State: closed - Opened by Zimmi48 over 7 years ago - 3 comments

#78 - Fixed up verif_object.v, with improvements and documentation

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

#77 - Atomics

Pull Request - State: closed - Opened by mansky1 over 7 years ago

#76 - improve 'make clean' to also remove .xxx.vo.aux

Pull Request - State: closed - Opened by ildyria over 7 years ago - 3 comments

#75 - Improvements to ghost state and release-acquire atomics.

Pull Request - State: closed - Opened by mansky1 over 7 years ago

#74 - add _Coqproject into gitignore: generated by the Makefile

Pull Request - State: closed - Opened by ildyria over 7 years ago

#73 - Breaking things to test Travis.

Pull Request - State: closed - Opened by mansky1 over 7 years ago - 1 comment

#72 - Build broken

Issue - State: closed - Opened by ghost over 7 years ago - 9 comments

#71 - Build broken

Issue - State: closed - Opened by maximedenes over 7 years ago - 1 comment

#70 - start_function should check parameter-type mismatch

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

#69 - Shifts of long-long integers

Issue - State: closed - Opened by andrew-appel over 7 years ago - 1 comment

#68 - Fix real literals

Pull Request - State: closed - Opened by ppedrot over 7 years ago

#67 - Explicitly name parameter in destruct.

Pull Request - State: closed - Opened by ejgallego over 7 years ago - 1 comment

#66 - Coq.8.6.admitted

Pull Request - State: closed - Opened by ildyria over 7 years ago

#65 - add proof of factorial intro progs

Pull Request - State: closed - Opened by ildyria almost 8 years ago - 1 comment

#64 - Misleading error message in forward-call

Issue - State: closed - Opened by lennartberinger almost 8 years ago - 2 comments

#63 - error message of with_library - tactic

Issue - State: closed - Opened by lennartberinger almost 8 years ago - 1 comment

#62 - no_loads_expr needs to support Esizeof

Issue - State: closed - Opened by roconnor-blockstream almost 8 years ago - 2 comments

#61 - add the possibility to compile a html doc in doc/html

Pull Request - State: closed - Opened by ildyria almost 8 years ago - 1 comment

#60 - Check return type

Issue - State: closed - Opened by lennartberinger almost 8 years ago - 1 comment

#59 - Coq.8.6

Pull Request - State: closed - Opened by ildyria almost 8 years ago

#58 - Allow overriding of the COMPCERT variable

Pull Request - State: closed - Opened by tbrk over 8 years ago - 4 comments

#57 - forward_while should give error message when expression fails to symbolically evaluate

Issue - State: closed - Opened by andrew-appel over 8 years ago - 1 comment

#56 - More progress in porting to Coq 8.5.

Pull Request - State: closed - Opened by maximedenes over 8 years ago

#55 - make forward_while also work if the while loop is at the end of a block

Pull Request - State: closed - Opened by samuelgruetter over 8 years ago - 1 comment

#54 - Fix a couple of minor errors in VC.tex.

Pull Request - State: closed - Opened by agl over 8 years ago

#53 - concurrency machine compilation

Pull Request - State: closed - Opened by nickgian over 8 years ago

#52 - checking for loads in `forward` is too eager

Issue - State: closed - Opened by jmadiot about 9 years ago - 1 comment

#51 - Converted 'make_version' script to python

Pull Request - State: closed - Opened by ahmadsalim over 9 years ago - 1 comment

#50 - Compilation error when running `make_version` during build process on OS X

Issue - State: closed - Opened by ahmadsalim over 9 years ago - 2 comments

#49 - Reroot, fold_data_at

Issue - State: closed - Opened by QinxiangCao over 9 years ago - 2 comments

#48 - A set rule with field_address

Issue - State: closed - Opened by QinxiangCao over 9 years ago - 1 comment

#47 - A proof theory for stronger

Issue - State: closed - Opened by QinxiangCao over 9 years ago - 1 comment

#46 - local variables in function-spec postcondition

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

#45 - globalenv vs Genv.globalenv

Issue - State: open - Opened by QinxiangCao over 9 years ago

#44 - Remove elements_remove

Issue - State: closed - Opened by QinxiangCao over 9 years ago - 1 comment

#43 - Improve go_lower0

Issue - State: closed - Opened by jldodds over 9 years ago - 1 comment

#42 - Abstracting the type of messages in the HMAC spec.

Pull Request - State: closed - Opened by adampetcher over 9 years ago

#41 - Added FCF and HMAC crypto proof

Pull Request - State: closed - Opened by adampetcher almost 10 years ago

#40 - Exponential blow up in Rtac load store rules

Issue - State: closed - Opened by QinxiangCao almost 10 years ago

#39 - Clean up forward.v

Issue - State: closed - Opened by jldodds almost 10 years ago - 1 comment

#38 - Don't export proof irrelevance and existential extentionality as hints to auto

Issue - State: closed - Opened by jldodds almost 10 years ago - 1 comment

#37 - forward_if tactic is not documented in the Verifiable C manual

Issue - State: closed - Opened by andrew-appel almost 10 years ago - 1 comment

#36 - Prove the soundness of applying load rule in rtac

Issue - State: closed - Opened by QinxiangCao almost 10 years ago

#35 - Write a Rtac version of hoist_later_in_pre

Issue - State: closed - Opened by QinxiangCao almost 10 years ago

#34 - Rtac version of nth solver

Issue - State: closed - Opened by QinxiangCao almost 10 years ago

#33 - Prove rmsubst sound

Issue - State: closed - Opened by jldodds almost 10 years ago
Labels: mc_reify

#32 - Prove REFLEXIVITY_DENOTE sound

Issue - State: closed - Opened by jldodds almost 10 years ago

#31 - Prove REFLEXIVITYTAC_msubst_sound

Issue - State: closed - Opened by jldodds almost 10 years ago
Labels: mc_reify

#30 - Prove REFLEXIVITY_sound

Issue - State: closed - Opened by jldodds almost 10 years ago

#29 - Tactic for solving msubst

Issue - State: closed - Opened by jldodds almost 10 years ago

#28 - data_at, field_address

Issue - State: closed - Opened by QinxiangCao almost 10 years ago
Labels: enhancement

#27 - Make reified load also work with top level, dynamically sized arrays

Issue - State: closed - Opened by jldodds almost 10 years ago - 1 comment
Labels: enhancement

#26 - Clarify what structured-data predicates to use in ref manual

Issue - State: closed - Opened by jldodds almost 10 years ago - 4 comments
Labels: documentation/refcard

#25 - Optimize set_reif_eq2 proof

Issue - State: closed - Opened by jldodds almost 10 years ago
Labels: mc_reify

#24 - examples/cont makefile

Issue - State: open - Opened by andrew-appel almost 10 years ago - 1 comment

#23 - forward_call gives bad error message when return type mismatches

Issue - State: closed - Opened by andrew-appel almost 10 years ago - 1 comment

#22 - list_cell, list_cell_eq

Issue - State: closed - Opened by andrew-appel almost 10 years ago - 1 comment

#21 - Fold id names

Issue - State: closed - Opened by jldodds almost 10 years ago - 1 comment
Labels: enhancement

#20 - Write tactic to apply load rule in Rtac

Issue - State: closed - Opened by QinxiangCao almost 10 years ago
Labels: enhancement

#19 - field_address reasoning lemmas

Issue - State: closed - Opened by andrew-appel almost 10 years ago - 1 comment

#18 - field_at_compatible

Issue - State: closed - Opened by andrew-appel almost 10 years ago

#17 - Prove soundness of Applying set

Issue - State: closed - Opened by jldodds almost 10 years ago
Labels: proof, mc_reify

#16 - Prove reified set function correct

Issue - State: closed - Opened by jldodds almost 10 years ago
Labels: proof

#15 - array_seg_reroot_lemma too strict

Issue - State: closed - Opened by andrew-appel almost 10 years ago - 1 comment