PrincetonUniversity/VST

Issues

• Trying to prove properties about eBPF programs (Clightgen issue)

  #792 opened 3 months ago by swarnpriya
  7

• repr_inj_signed64 has incorrect bounds.

  #789 opened 3 months ago by roconnor-blockstream
  0

• mailbox broken: typedef with/without *

  #782 opened 4 months ago by andrew-appel
  2

• CompCert planned change: adding a `Mbool` memory chunk

  #779 opened 4 months ago by xavierleroy
  6

• In VST 3.0beta2, normalize1 tactic

  #773 opened 7 months ago by andrew-appel
  6

• check_parameter_vals should have lazymatch

  #772 opened 7 months ago by andrew-appel
  0

• IPM proof fails in lib/proof body_release, succeeds in atomics body_release

  #770 opened 7 months ago by andrew-appel
  1

• verif_incr should prove that it restores an uninitialized counter

  #769 opened 7 months ago by andrew-appel
  1

• cstring should not need a compspecs argument

  #764 opened 8 months ago by andrew-appel
  2

• mkVSU external function check does not give useful error message

  #763 opened 8 months ago by andrew-appel
  3

• Please create a tag for Coq 8.19 in Coq Platform 2024.01

  #760 opened 8 months ago by rtetley
  4

• inhabited_value doesn't really work well

  #762 opened 8 months ago by andrew-appel
  0

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

  #626 opened 8 months ago by ghulette
  1

• future-coercion-class-field warning

  #674 opened 8 months ago by andrew-appel
  3

• localize / entailer_for_load_tac / unlocalize / Coq 8.17

  #756 opened 9 months ago by andrew-appel
  11

• overbroad match in try_conjuncts

  #745 opened 9 months ago by andrew-appel
  0

• data_at_int_or_ptr_int share

  #749 opened 9 months ago by andrew-appel
  0

• solve_load_rule_evaluation @proj_reptype

  #748 opened 9 months ago by andrew-appel
  3

• Improvements in deadvars

  #751 opened 9 months ago by andrew-appel
  0

• Unnecessary premise in `Lemma field_at_app`

  #743 opened 9 months ago by MSoegtropIMC
  0

• fail levels in forward_if'_new

  #744 opened 9 months ago by andrew-appel
  0

• Useful lemma for users: nonempty_writable_glb

  #734 opened 9 months ago by andrew-appel
  0

• solve_store_rule_evaluation

  #752 opened 9 months ago by andrew-appel
  1

• forward_call takes a long time

  #750 opened 9 months ago by rigille
  2

• Function pointer comparison apparently not supported

  #746 opened a year ago by lennartberinger
  0

• Please create a tag for Coq 8.18 in Coq Platform 2023.10

  #727 opened a year ago by rtetley
  5

• do {S} while (0)

  #738 opened a year ago by andrew-appel
  0

• Some observations on `forward_call` performance

  #729 opened a year ago by MSoegtropIMC
  21

• quick_typecheck3 should not clear

  #722 opened a year ago by andrew-appel
  2

• field_compatible0_Tarray_offset

  #700 opened a year ago by andrew-appel
  0

• `builtin` and `type` don't exist in `dash` (`util/make_version` is invoked inconsistently)

  #702 opened a year ago by JasonGross
  0

• list_solve no longer solves a goal

  #653 opened a year ago by joscoh
  4

• list_solve problems with sorted lists

  #664 opened a year ago by andrew-appel
  3

• `make install` silently installs nothing when `IGNORECOMPCERTVERSION=true` is passed and the versions mismatch

  #706 opened a year ago by JasonGross
  0

• `make install` fails with "install: cannot stat 'msl/LICENSE': No such file or directory"

  #704 opened a year ago by JasonGross
  0

• field_compatible0_Tarray_offset does not need naturally_aligned

  #710 opened a year ago by andrew-appel
  1

• Please create a tag for Coq 8.17 in Coq Platform 2023.03

  #666 opened a year ago by MSoegtropIMC
  6

• Transparent Vptrofs

  #699 opened a year ago by andrew-appel
  0

• More concise defined evaluations (Definition arch : nat := Eval ... )

  #690 opened a year ago by andrew-appel
  0

• Portable build of progs/ and progs64/ directories

  #686 opened a year ago by andrew-appel
  6

• strcmp code and spec

  #667 opened a year ago by dnaumann
  0

• Opaque Int64.repr blocking tactics

  #669 opened 2 years ago by roconnor-blockstream
  1

• Typo in GitHub release notes for 2.9

  #672 opened 2 years ago by Zimmi48
  1

• Broken with Coq master

  #673 opened 2 years ago by SkySkimmer
  3

• subsumespec_app1, subsumespec_app2

  #660 opened 2 years ago by andrew-appel
  1

• Suggestion: Val.of_bool and partial evaluation

  #625 opened 2 years ago by roconnor-blockstream
  10

• check_parameter_vals

  #641 opened 2 years ago by andrew-appel
  1

• rep_lia tactic is missing in the catalog

  #628 opened 2 years ago by olympichek
  0

• Global array of doubles is not properly packaged by start_function

  #655 opened 2 years ago by andrew-appel
  1

• check_mpreds2 fails at too high a level

  #638 opened 2 years ago by andrew-appel
  0