PrincetonUniversity/VST

Las issues en las que quizá ya trabaja alguien aparecen al final. Ordenar todo por fecha

• [VST2.16] Inconsistent bitfield rejection leads to incorrect verification results

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

  PrincetonUniversity/VST#868 · 1 comentario · Abierto el 2/9/2026

• aes/verif_setkey_enc_LL.v: Vundef_is_Vint is admitted with a comment saying it does not hold, then used twice

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 5/5 Más de una semana Aptitud para principiantes 35/100

  PrincetonUniversity/VST#867 · Abierto el 29/8/2026

• Dependently typed WITH components

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 5/5 Más de una semana Aptitud para principiantes 25/100

  PrincetonUniversity/VST#838 · 1 comentario · Abierto el 25/9/2025

• How to Specify and Prove a Function Reading Header from a Payload Pointer

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 5/5 Más de una semana Aptitud para principiantes 25/100

  PrincetonUniversity/VST#822 · 1 comentario · Abierto el 4/6/2025

• Issues with VST Installation via OPAM (coq-vst.3.0beta2)

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 4/5 3-5 días Aptitud para principiantes 25/100

  PrincetonUniversity/VST#820 · 6 comentarios · Abierto el 31/5/2025

• do {S} while (0)

  Quizá libre de nuevo @QinxiangCao la tomó hace 1067 días y no hay ningún pull request abierto. Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  PrincetonUniversity/VST#738 · 1 asignado · Abierto el 26/10/2023

• Transparent Vptrofs

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 5/5 Más de una semana Aptitud para principiantes 25/100

  PrincetonUniversity/VST#699 · Abierto el 12/7/2023

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

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 2/5 1-3 horas Aptitud para principiantes 35/100

  PrincetonUniversity/VST#690 · Abierto el 20/6/2023

• Portable build of progs/ and progs64/ directories

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 5/5 Más de una semana Aptitud para principiantes 35/100

  PrincetonUniversity/VST#686 · 6 comentarios · Abierto el 31/5/2023

• Provide a convenient way to run examples with OPAM-install VST

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 5/5 Más de una semana Aptitud para principiantes 25/100

  PrincetonUniversity/VST#615 · 10 comentarios · Abierto el 1/8/2022

• store_tac_with_hint insufficiently general for array of struct

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 5/5 Más de una semana Aptitud para principiantes 35/100

  PrincetonUniversity/VST#613 · Abierto el 29/7/2022

• veric/superprecise.v

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 5/5 Más de una semana Aptitud para principiantes 20/100

  PrincetonUniversity/VST#603 · Abierto el 15/7/2022

• Define address_mapsto by encode_val instead of decode_val?

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 5/5 Más de una semana Aptitud para principiantes 35/100

  PrincetonUniversity/VST#602 · 2 comentarios · 1 reacción · Abierto el 15/7/2022

• Mission of `.opam` files in this repo

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 4/5 3-5 días Aptitud para principiantes 35/100

  PrincetonUniversity/VST#597 · Abierto el 12/7/2022

• Add a description of how to use withspacer in manual

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 2/5 1-3 horas Aptitud para principiantes 35/100

  PrincetonUniversity/VST#581 · 2 comentarios · Abierto el 21/5/2022

• sep_apply unable to handle some expressions with propositions.

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 3/5 1-2 días Aptitud para principiantes 35/100

  PrincetonUniversity/VST#580 · 1 comentario · Abierto el 16/5/2022

• Soundness of VST for gcc and clang

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 5/5 Más de una semana Aptitud para principiantes 25/100

  PrincetonUniversity/VST#566 · 3 comentarios · 1 reacción · Abierto el 21/4/2022

• VST upgrade 2.6 -> 2.8: 80% slowdown in compilation time

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 5/5 Más de una semana Aptitud para principiantes 25/100

  PrincetonUniversity/VST#514 · 2 comentarios · Abierto el 3/9/2021

• forward_for_simple_bound and EWD heuristic

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 5/5 Más de una semana Aptitud para principiantes 25/100

  PrincetonUniversity/VST#507 · Abierto el 26/7/2021

• Create new opam packages for VST

  Quizá libre de nuevo @MSoegtropIMC la tomó hace 2268 días y no hay ningún pull request abierto. Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  infrastructure

  PrincetonUniversity/VST#441 · 17 comentarios · 1 asignado · Abierto el 13/7/2020

• Pretty-printing of Clight uses wrong subscopes

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 3/5 1-2 días Aptitud para principiantes 35/100

  PrincetonUniversity/VST#295 · 2 comentarios · Abierto el 23/10/2018

• Forward_for and forward_for_simple_bound cannot handle multiple EX in Inv

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 4/5 3-5 días Aptitud para principiantes 25/100

  PrincetonUniversity/VST#193 · 1 comentario · Abierto el 24/4/2018

• globalenv vs Genv.globalenv

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 5/5 Más de una semana Aptitud para principiantes 20/100

  PrincetonUniversity/VST#45 · Abierto el 18/3/2015

• examples/cont makefile

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 2/5 1-3 horas Aptitud para principiantes 45/100

  PrincetonUniversity/VST#24 · 1 comentario · Abierto el 16/12/2014