Commits

Branch selector

 master

User selector

All users

Datepicker

All time

Commit History

Commits on Aug 28, 2024

• advanced xdp example

  swarnpriya

  committed
  1cf24e9

  Copy full SHA for 1cf24e9

• proof for packet count example with counter of type uint

  swarnpriya

  committed
  f43f64e

  Copy full SHA for f43f64e

• .

  swarnpriya

  committed
  2816e5d

  Copy full SHA for 2816e5d

• wip for packet_count example

  swarnpriya

  committed
  992f2a9

  Copy full SHA for 992f2a9

• wip for packet count xdp

  swarnpriya

  committed
  1ca0780

  Copy full SHA for 1ca0780

Commits on Aug 9, 2024

• Merge pull request PrincetonUniversity#787 from ppedrot/template-no-sup-constraint

  Show description for 1ba625a
  andrew-appel

  authored
  1ba625a

  Copy full SHA for 1ba625a

Commits on Aug 8, 2024

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

  ppedrot

  committed
  108091c

  Copy full SHA for 108091c

Commits on Jul 28, 2024

• Merge pull request PrincetonUniversity#781 from PrincetonUniversity/compcert3.15

  Show description for 6c978e6
  andrew-appel

  authored
  6c978e6

  Copy full SHA for 6c978e6

Commits on Jul 27, 2024

• Bump VST version number to 2.15

  andrew-appel

  committed
  8c76515

  Copy full SHA for 8c76515

Commits on Jul 26, 2024

• Merge PrincetonUniversity#783

  andrew-appel

  committed
  fa12c99

  Copy full SHA for fa12c99

• Brought sha proofs up to date

  andrew-appel

  committed
  bc802ff

  Copy full SHA for bc802ff

• Tweak test targets for VSUpile in 64 and 32 bit modes

  andrew-appel

  committed
  3a21957

  Copy full SHA for 3a21957

• updated mailbox to use new lock_t

  mansky1

  committed
  4a0f569

  Copy full SHA for 4a0f569

• Got test2 working in 32-bit mode

  andrew-appel

  committed
  60bb838

  Copy full SHA for 60bb838

• clightgen all the 32-bit progs .c files

  andrew-appel

  committed
  13b0cdf

  Copy full SHA for 13b0cdf

• Hack progs64/printf.v

  andrew-appel

  committed
  9bd9296

  Copy full SHA for 9bd9296

• tweak CI

  andrew-appel

  committed
  3c188b6

  Copy full SHA for 3c188b6

• tweak CI

  andrew-appel

  committed
  b3e922f

  Copy full SHA for b3e922f

Commits on Jul 25, 2024

• tweak CI

  andrew-appel

  committed
  2f2bcee

  Copy full SHA for 2f2bcee

• tweak CI

  andrew-appel

  committed
  a2c02ce

  Copy full SHA for a2c02ce

• Tweaks to CI and some work on verif_printf test case

  andrew-appel

  committed
  f865914

  Copy full SHA for f865914

• More tweaks, got most of CI working

  andrew-appel

  committed
  31fcf79

  Copy full SHA for 31fcf79

Commits on Jul 24, 2024

• Port VST 2.x to CompCert master AbsInt/CompCert@f92facf

  andrew-appel

  committed
  e4539a3

  Copy full SHA for e4539a3

Commits on Jun 12, 2024

• Merge pull request PrincetonUniversity#777 from SkySkimmer/make-profiling

  Show description for 0eed04f
  andrew-appel

  authored
  0eed04f

  Copy full SHA for 0eed04f

Commits on Jun 11, 2024

• build: support TIMED like coq_makefile

  SkySkimmer

  committed
  4ec5322

  Copy full SHA for 4ec5322

• build: support PROFILING like coq_makefile

  Show description for f8859cb
  SkySkimmer

  committed
  f8859cb

  Copy full SHA for f8859cb

Commits on May 31, 2024

• Merge pull request PrincetonUniversity#774 from ppedrot/abstract-functor-lemmas

  Show description for 350e508
  andrew-appel

  authored
  350e508

  Copy full SHA for 350e508

Commits on May 30, 2024

• Merge pull request PrincetonUniversity#771 from PrincetonUniversity/funcptr_validpointer

  Show description for 411744b
  andrew-appel

  authored
  411744b

  Copy full SHA for 411744b

Commits on May 26, 2024

• Wrap functor facts in abstract lemmas.

  ppedrot

  committed
  1442260

  Copy full SHA for 1442260

Commits on Apr 26, 2024

• Added func_ptr'_valid_pointer and SeparationLogic.func_ptr_valid_pointer to the valid_pointer hint database, removeing the latter from saturate_locals

  lennartberinger

  committed
  1fb9af5

  Copy full SHA for 1fb9af5

• Added another test case that compares two function pointers; spec assumes the (somewhat adhoc) assumption 'globals_injective'

  lennartberinger

  committed
  1b2a5c8

  Copy full SHA for 1b2a5c8

Commits on Apr 25, 2024

• Changed definition of valid_pointer' wrt locations with PURE resources, to facilitate proof of lemma func_at_valid_pointer and ensuing lemmas about func_ptr and func_ptr'

  lennartberinger

  committed
  81801b7

  Copy full SHA for 81801b7

Commits on Apr 18, 2024

• Improved rule WholeComponent_DrySafe; the rule still depends on an axiom concerning the relationship between the definitions of semaxfunc in the VST interface and the model

  lennartberinger

  committed
  56e6886

  Copy full SHA for 56e6886

Commits on Apr 16, 2024

• Merge pull request PrincetonUniversity#768 from PrincetonUniversity/VSUpile64

  Show description for f72a1fd
  lennartberinger

  authored
  f72a1fd

  Copy full SHA for f72a1fd

• Ported progs64/VSUpile from compcert 3.8 to 3.13, ported proofs, and added the directory as target (test6) to Makefile

  lennartberinger

  committed
  af11545

  Copy full SHA for af11545

Pagination

Previous

Next