Commits

Branch selector

 master

User selector

All users

Datepicker

All time

Commit History

Commits on Jun 22, 2022

• Add data_at lemmas for arrays and numbers

  joscoh

  committed
  38f9e67

  Copy full SHA for 38f9e67

Commits on Jun 21, 2022

• tweak zlist (#589)

  Show description for 8d976f0
  

  QinshiWang

  and

  andrew-appel

  authored
  8d976f0

  Copy full SHA for 8d976f0

Commits on Jun 20, 2022

• Fix CI to avoid redoing "build" in "test" stage; update submodules (#588)

  Show description for e870f28
  andrew-appel

  authored
  e870f28

  Copy full SHA for e870f28

Commits on Jun 14, 2022

• Fix soundness-checking; organize TCB and soundness check in CI

  Show description for a6df99a
  andrew-appel

  authored
  a6df99a

  Copy full SHA for a6df99a

Commits on Jun 13, 2022

• `finish` & `fastforward` (#575)

  Show description for 1374469
  ZippeyKeys12

  authored
  1374469

  Copy full SHA for 1374469

Commits on May 16, 2022

• Improve VSUpile makefile (#579)

  Show description for 3fc0204
  andrew-appel

  authored
  3fc0204

  Copy full SHA for 3fc0204

Commits on May 10, 2022

• Merge pull request #576 from Alizter/adapt-to-16004

  Show description for 1caea02
  andrew-appel

  authored
  1caea02

  Copy full SHA for 1caea02

• Adapt w.r.t coq/coq#16004

  Alizter

  committed
  240c0e6

  Copy full SHA for 240c0e6

Commits on May 4, 2022

• Tactics: `Intros *`, `Intros ?` and `Exists ?` (#572)

  Show description for 7090fd1
  ZippeyKeys12

  authored
  7090fd1

  Copy full SHA for 7090fd1

Commits on Apr 28, 2022

• Merge pull request #573 from PrincetonUniversity/entailer-tweaks

  Show description for c3e68fb
  andrew-appel

  authored
  c3e68fb

  Copy full SHA for c3e68fb

• Change Flocq3 back to Flocq in compcert/*.v

  Show description for 6558e4b
  andrew-appel

  committed
  6558e4b

  Copy full SHA for 6558e4b

• Disable an Admitted lemma in core soundness proof

  andrew-appel

  committed
  824350f

  Copy full SHA for 824350f

• Merge pull request #571 from PrincetonUniversity/entailer-tweaks

  Show description for ea277ad
  andrew-appel

  authored
  ea277ad

  Copy full SHA for ea277ad

Commits on Apr 27, 2022

• Fix permissions

  andrew-appel

  committed
  7d593b3

  Copy full SHA for 7d593b3

• faster binop_lemmas?.v proofs, delete lots of junk

  Show description for b927830
  andrew-appel

  committed
  b927830

  Copy full SHA for b927830

• Merge pull request #569 from PrincetonUniversity/entailer-tweaks

  Show description for c22234a
  andrew-appel

  authored
  c22234a

  Copy full SHA for c22234a

Commits on Apr 26, 2022

• Fix progs64 build; also, adapt bundled compcert for Coq Platform 2022.04 (Flocq->Flocq3)

  andrew-appel

  committed
  f3ad896

  Copy full SHA for f3ad896

• Improve entailer; faster proofs in veric.extend_tc; Makefile fix

  Show description for bd74ffa
  andrew-appel

  committed
  bd74ffa

  Copy full SHA for bd74ffa

• Merge pull request #568 from PrincetonUniversity/abandon-coq-8.13

  Show description for d1687ef
  andrew-appel

  authored
  d1687ef

  Copy full SHA for d1687ef

Commits on Apr 25, 2022

• Tweak for Coq 8.14 compatibility

  andrew-appel

  committed
  8d73ba4

  Copy full SHA for 8d73ba4

• Abandon Coq 8.13 compatibility; abandon travis-ci; other minor cleanups

  andrew-appel

  committed
  3f2d7bd

  Copy full SHA for 3f2d7bd

Commits on Apr 21, 2022

• Remove Coq 8.13 from CI scripts; now just test in Coq 8.14 and 8.15

  andrew-appel

  committed
  30a4654

  Copy full SHA for 30a4654

• Unfolding in forward (#563)

  Show description for 94764a4
  ZippeyKeys12

  authored
  94764a4

  Copy full SHA for 94764a4

• Merge pull request #567 from PrincetonUniversity/bugfixes

  Show description for d80fecd
  andrew-appel

  authored
  d80fecd

  Copy full SHA for d80fecd

• Fix issue #561 (missing check for long-long signed overflow)

  Show description for 9a91f41
  andrew-appel

  committed
  9a91f41

  Copy full SHA for 9a91f41

Commits on Apr 20, 2022

• Merge pull request #564 from PrincetonUniversity/bugfixes

  Show description for 0327c1e
  andrew-appel

  authored
  0327c1e

  Copy full SHA for 0327c1e

• Bring 'make all' up to date with latest VST

  andrew-appel

  committed
  d3afd1e

  Copy full SHA for d3afd1e

Commits on Apr 19, 2022

• Fix issues #562 #560 #558

  andrew-appel

  committed
  f1e7b9b

  Copy full SHA for f1e7b9b

Commits on Apr 4, 2022

• Merge pull request #555 from PrincetonUniversity/atomic_locks

  Show description for ba3dc4a
  andrew-appel

  authored
  ba3dc4a

  Copy full SHA for ba3dc4a

Commits on Apr 2, 2022

• Permit Coq 8.15.1 in Makefile

  txyyss

  committed
  e84fadb

  Copy full SHA for e84fadb

• Merge branch 'master' into atomic_locks

  txyyss

  committed
  435b4f8

  Copy full SHA for 435b4f8

• Fix #[export] for Coq 8.13.

  txyyss

  committed
  26d2767

  Copy full SHA for 26d2767

• Fix locality warnings.

  txyyss

  committed
  bded79c

  Copy full SHA for bded79c

Commits on Apr 1, 2022

• Merge pull request #559 from MSoegtropIMC/fix-makefile

  Show description for 2f72f26
  andrew-appel

  authored
  2f72f26

  Copy full SHA for 2f72f26

Commits on Mar 31, 2022

• Fix the proof of add_item in hashtable_atomic.c

  txyyss

  committed
  f2003c5

  Copy full SHA for f2003c5

Pagination

Previous

Next