Search results

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

veric/superprecise.v

Status: Open.

#603 In PrincetonUniversity/VST;

· andrew-appel opened on Jul 15, 2022

Define address_mapsto by encode_val instead of decode_val?

Status: Open.

#602 In PrincetonUniversity/VST;

· andrew-appel opened on Jul 15, 2022

Mission of <code>.opam</code> files in this repo

Status: Open.

#597 In PrincetonUniversity/VST;

· QinshiWang opened on Jul 12, 2022

Add a description of how to use withspacer in manual

Status: Open.

#581 In PrincetonUniversity/VST;

· lennartberinger opened on May 21, 2022