Skip to content
Snippets Groups Projects
Select Git revision
  • alloc_align
  • bits-deep-backup
  • case-pgtable
  • ci/VerifyThis2021
  • ci/VerifyThis2022
  • ci/allocstack
  • ci/bff-artifact
  • ci/bits-record-param
  • ci/bitvec_typed
  • ci/bool-simpl
  • ci/case-mt7601u
  • ci/case_router
  • ci/free_no_layout
  • ci/frontent_fix
  • ci/lithium-dissertation-sammler
  • ci/more-bit-cases
  • ci/more_prov
  • ci/pkvm-hof
  • ci/pldi21-submission-artifact
  • ci/ptrfrag
  • vip-popl22-submission-artifact
  • pldi21-submission-artifact
22 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.09Jul865330Jun292825242221181614109754231May272521201929Apr282723191615148231Mar302927262524231698542126Feb25242322191817161512111085432129Jan282726232219181514121117Dec11987643230Nov2726252420181716131211109543229Oct222172130Sep29261715147432131Aug2827201829Jul28272321Update the Cerberus dependency.Fix frontend bug on [refinedc clean].Update the Cerberus dependency.Add mem castfix admittedhack printing of filenamesmore proofsmake copy alloc id a functionadd introduce_typed_stmtmake statement postcondition more genericadd list of types to callmake calls extensiblefind buddyForce code generation.Original code of Hafnium for [sl_lock_both].Tweak implementation of [copy_alloc_id].remove sketches from ocaml runtime codeadd subsumption for alloc alive for arraysadd forgotten filecopy alloc id for one past the end pointerremove array ptr learnchange diff rule for arraysallow int-to-ptr casts in lexprsadd typing rule for ptrdiff on arrayadd ocaml_runtime examplelearn alignment on pointer to integer castsanother tweaktweak copy alloc id ruleUpdated early alloc exampleupdate type cast ptr intptr ruleUse the Cerberus intrinsic for copy_alloc_id.Rename rc_copy_alloc_id into copy_alloc_id.Update Cerberus + update script.fix wrapping rulescheck in missing filesAllow alloc_alive_loc to open invariantsadd roundtrip example for one past the end pointerschange tagged_ptr example to use bitwise operationsadd pointer to integer casts for function pointersmore equality in opsem