Issues

• Build fails on master, blocking Coq bench

  mit-plv/bedrock2#499 · Filter by author JasonGross opened on Nov 3, 2025
  1

• FR: Sign-extending load1/load2/load4

  mit-plv/bedrock2#496 · Filter by author andres-erbsen opened on Oct 7, 2025

• Improve program_logic_goal_for error messages

  mit-plv/bedrock2#492 · Filter by author miriampolzer opened on Sep 16, 2025
  

• Preserve variable names in ProgramLogic proofs

  mit-plv/bedrock2#478 · Filter by author andres-erbsen opened on Jul 24, 2025
  1

• supporting $@ (map.of_list_word_at) for stackalloc/stackdealloc

  mit-plv/bedrock2#477 · Filter by author andres-erbsen opened on Jul 16, 2025
  3

• bytedump test seems to no longer work on Windows

  mit-plv/bedrock2#454 · Filter by author JasonGross opened on Apr 24, 2025

• README should link relevant papers written on / on top of bedrock2

  mit-plv/bedrock2#448 · Filter by author JasonGross opened on Feb 18, 2025

• build fails on 32-bit

  mit-plv/bedrock2#434 · Filter by author JasonGross opened on Oct 26, 2024
  1

• design: core functionality of RecordPredicates?

  mit-plv/bedrock2#370 · Filter by author andres-erbsen opened on Aug 25, 2023
  4

• design: outputting bitwidth-generic code?

  mit-plv/bedrock2#368 · Filter by author andres-erbsen opened on Aug 23, 2023
  7

• make should not run coq and cc when there's nothing to be done

  mit-plv/bedrock2#298 · Filter by author JasonGross opened on Nov 21, 2022

• Test suite for ToCString

  mit-plv/bedrock2#204 · Filter by author andres-erbsen opened on Nov 28, 2021
  1

• Hint Mode + again

  mit-plv/bedrock2#193 · Filter by author samuelgruetter opened on Jul 20, 2021
  9

• Makefile doesn't work with EXTERNAL_DEPENDENCIES=1

  mit-plv/bedrock2#192 · Filter by author Alizter opened on Jul 19, 2021
  4

• Missing operators

  mit-plv/bedrock2#189 · Filter by author samuelgruetter opened on Jun 18, 2021
  1

• predicates describing bytes in memory

  mit-plv/bedrock2#185 · Filter by author andres-erbsen opened on Apr 30, 2021
  5

• opam package for bench

  mit-plv/bedrock2#170 · Filter by author SkySkimmer opened on Dec 11, 2020
  1

• [request] c_call like c_func / fmt_c_decl

  mit-plv/bedrock2#168 · Filter by author JasonGross opened on Nov 10, 2020
  2

• load8 vs load_word?

  mit-plv/bedrock2#159 · Filter by author andres-erbsen opened on Jun 29, 2020
  5

• incorporate bytes<->words conversion from fiat-crypto

  mit-plv/bedrock2#156 · Filter by author andres-erbsen opened on Apr 30, 2020
  6

• Does bedrock2 want warning/error annotations on PRs?

  mit-plv/bedrock2#149 · Filter by author JasonGross opened on Mar 28, 2020
  4

• bedrock2 fails to build when switching from EXTERNAL_DEPENDENCIES=1 to EXTERNAL_DEPENDENCIES= because _CoqProject is not remade

  mit-plv/bedrock2#119 · Filter by author JasonGross opened on Dec 9, 2019
  2

• make -k does not build compiler if bedrock2 fails

  mit-plv/bedrock2#114 · Filter by author andres-erbsen opened on Nov 14, 2019
  1

• make is very noisy, even when there's nothing to be done

  mit-plv/bedrock2#105 · Filter by author JasonGross opened on Oct 4, 2019
  4

• the build output contains a lot of noise

  mit-plv/bedrock2#97 · Filter by author andres-erbsen opened on Sep 19, 2019
  1