PrincetonUniversity/VST

Le issue su cui forse qualcuno sta già lavorando sono in fondo alla lista. Ordina tutto per data

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

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 4/5 3-5 giorni Idoneità per principianti 48/100

  PrincetonUniversity/VST#868 · 1 commento · Aperta il 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

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 5/5 Più di una settimana Idoneità per principianti 35/100

  PrincetonUniversity/VST#867 · Aperta il 29/8/2026

• Dependently typed WITH components

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 5/5 Più di una settimana Idoneità per principianti 25/100

  PrincetonUniversity/VST#838 · 1 commento · Aperta il 25/9/2025

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

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 5/5 Più di una settimana Idoneità per principianti 25/100

  PrincetonUniversity/VST#822 · 1 commento · Aperta il 4/6/2025

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

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 4/5 3-5 giorni Idoneità per principianti 25/100

  PrincetonUniversity/VST#820 · 6 commenti · Aperta il 31/5/2025

• do {S} while (0)

  Forse di nuovo libera @QinxiangCao l’ha presa 1067 giorni fa e non c’è nessuna pull request aperta. Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  PrincetonUniversity/VST#738 · 1 assegnatario · Aperta il 26/10/2023

• Transparent Vptrofs

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 5/5 Più di una settimana Idoneità per principianti 25/100

  PrincetonUniversity/VST#699 · Aperta il 12/7/2023

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

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 2/5 1-3 ore Idoneità per principianti 35/100

  PrincetonUniversity/VST#690 · Aperta il 20/6/2023

• Portable build of progs/ and progs64/ directories

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 5/5 Più di una settimana Idoneità per principianti 35/100

  PrincetonUniversity/VST#686 · 6 commenti · Aperta il 31/5/2023

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

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 5/5 Più di una settimana Idoneità per principianti 25/100

  PrincetonUniversity/VST#615 · 10 commenti · Aperta il 1/8/2022

• store_tac_with_hint insufficiently general for array of struct

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 5/5 Più di una settimana Idoneità per principianti 35/100

  PrincetonUniversity/VST#613 · Aperta il 29/7/2022

• veric/superprecise.v

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 5/5 Più di una settimana Idoneità per principianti 20/100

  PrincetonUniversity/VST#603 · Aperta il 15/7/2022

• Define address_mapsto by encode_val instead of decode_val?

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 5/5 Più di una settimana Idoneità per principianti 35/100

  PrincetonUniversity/VST#602 · 2 commenti · 1 reazione · Aperta il 15/7/2022

• Mission of `.opam` files in this repo

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100

  PrincetonUniversity/VST#597 · Aperta il 12/7/2022

• Add a description of how to use withspacer in manual

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 2/5 1-3 ore Idoneità per principianti 35/100

  PrincetonUniversity/VST#581 · 2 commenti · Aperta il 21/5/2022

• sep_apply unable to handle some expressions with propositions.

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 3/5 1-2 giorni Idoneità per principianti 35/100

  PrincetonUniversity/VST#580 · 1 commento · Aperta il 16/5/2022

• Soundness of VST for gcc and clang

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 5/5 Più di una settimana Idoneità per principianti 25/100

  PrincetonUniversity/VST#566 · 3 commenti · 1 reazione · Aperta il 21/4/2022

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

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 5/5 Più di una settimana Idoneità per principianti 25/100

  PrincetonUniversity/VST#514 · 2 commenti · Aperta il 3/9/2021

• forward_for_simple_bound and EWD heuristic

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 5/5 Più di una settimana Idoneità per principianti 25/100

  PrincetonUniversity/VST#507 · Aperta il 26/7/2021

• Create new opam packages for VST

  Forse di nuovo libera @MSoegtropIMC l’ha presa 2268 giorni fa e non c’è nessuna pull request aperta. Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla
  infrastructure

  PrincetonUniversity/VST#441 · 17 commenti · 1 assegnatario · Aperta il 13/7/2020

• Pretty-printing of Clight uses wrong subscopes

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 3/5 1-2 giorni Idoneità per principianti 35/100

  PrincetonUniversity/VST#295 · 2 commenti · Aperta il 23/10/2018

• Forward_for and forward_for_simple_bound cannot handle multiple EX in Inv

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 4/5 3-5 giorni Idoneità per principianti 25/100

  PrincetonUniversity/VST#193 · 1 commento · Aperta il 24/4/2018

• globalenv vs Genv.globalenv

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 5/5 Più di una settimana Idoneità per principianti 20/100

  PrincetonUniversity/VST#45 · Aperta il 18/3/2015

• examples/cont makefile

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 2/5 1-3 ore Idoneità per principianti 45/100

  PrincetonUniversity/VST#24 · 1 commento · Aperta il 16/12/2014