Search results

make_func_ptr, or evaluating a global name, without GLOBALS(gv)

Status: Open.

#848 In PrincetonUniversity/VST;

· andrew-appel opened on Dec 30, 2025

improve forward.destruct_it

Status: Open.

#847 In PrincetonUniversity/VST;

· andrew-appel opened on Dec 30, 2025

Dependently typed WITH components

Status: Open.

#838 In PrincetonUniversity/VST;

· andrew-appel opened on Sep 25, 2025

compcert version in progs64/

Status: Open.

#831 In PrincetonUniversity/VST;

· lengyijun opened on Jul 9, 2025

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

Status: Open.

#822 In PrincetonUniversity/VST;

· laforetbarroso opened on Jun 4, 2025

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

Status: Open.

#820 In PrincetonUniversity/VST;

· laforetbarroso opened on May 31, 2025

do {S} while (0)

Status: Open.

#738 In PrincetonUniversity/VST;

· andrew-appel opened on Oct 26, 2023

Transparent Vptrofs

Status: Open.

#699 In PrincetonUniversity/VST;

· andrew-appel opened on Jul 12, 2023

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

Status: Open.

#690 In PrincetonUniversity/VST;

· andrew-appel opened on Jun 20, 2023

Portable build of progs/ and progs64/ directories

Status: Open.

#686 In PrincetonUniversity/VST;

· andrew-appel opened on May 31, 2023

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

Status: Open.

#615 In PrincetonUniversity/VST;

· QinshiWang opened on Aug 1, 2022

store_tac_with_hint insufficiently general for array of struct

Status: Open.

#613 In PrincetonUniversity/VST;

· andrew-appel opened on Jul 29, 2022