rems-project/cerberus

Issues

• [cn] Pretty print terms for humans

  #465 opened 2 months ago by yav
  7

• [CN] Print resource "output arguments" is a more helpful way

  #519 opened 2 months ago by dc-mak
  0

• [CN] Rename the `extract` statement to `focus`

  #499 opened 2 months ago by cp526
  2

• [CN] Retire the ability to break up specifications across magic comments

  #503 opened 2 months ago by dc-mak
  1

• [CN] Lexer lookup inefficiency

  #511 opened 2 months ago by dc-mak
  1

• [CN] Adjust output/printing for multiple errors

  #513 opened 2 months ago by dc-mak
  3

• [CN] Misleading warning on necessary use of `extract`

  #498 opened 2 months ago by septract
  11

• [CN] Make `extract` and `instantiate` more idiomatic

  #471 opened 2 months ago by septract
  6

• [CN] Double array access

  #484 opened 2 months ago by lwli11
  7

• [CN] Remove `list`, and remove / deprecate other unused keywords

  #490 opened 2 months ago by septract
  2

• [CN] Split out CN CI from CHERI

  #510 opened 2 months ago by dc-mak
  0

• [CN] Unknown constant response from SMT solver

  #505 opened 2 months ago by peterohanley
  2

• [CN] Streamline `spec` syntax

  #500 opened 2 months ago by dc-mak
  2

• [CN] Make `rems-project/cn-tutorial` a submodule of `rems-project/cerberus`?

  #475 opened 2 months ago by septract
  13

• [CN] Make type names consistent in spec language (eg `char` vs. `u8`)

  #442 opened 3 months ago by septract
  10

• [CN] Run Docker build nightly

  #489 opened 2 months ago by septract
  2

• Potentially bad elaboration in presence of bitvectors

  #493 opened 2 months ago by dc-mak
  0

• [CN] Caputre all output (not just return codes) for CI in a convenient to update way

  #412 opened 3 months ago by dc-mak
  1

• Initialiization with unaligned pointer

  #488 opened 2 months ago by vzaliva
  0

• [CN] Automatically generate a grammar reference

  #486 opened 2 months ago by dc-mak
  0

• [CN] Use a auto-unfolding scheme for `function`s

  #483 opened 2 months ago by dc-mak
  0

• [CN] Confusing error message for shift right

  #464 opened 2 months ago by lwli11
  4

• [CN] Block should allow omitting C-type like owned

  #413 opened 2 months ago by dc-mak
  3

• [CN] Clean up error reporting in `backend/cn/lib/check.ml`

  #462 opened 2 months ago by septract
  0

• [CN] Allow wildcard name / no name for `take`

  #466 opened 2 months ago by septract
  1

• [CN] Consolidate `trusted` and `spec` keywords

  #467 opened 2 months ago by septract
  2

• [CN] Align `unchanged` syntax with other CN syntax

  #468 opened 2 months ago by septract
  1

• [CN] Meta-issue: proposals for small-scale CN improvements

  #469 opened 2 months ago by septract
  0

• [CN] Add CI for executable spec

  #417 opened 2 months ago by dc-mak
  3

• [CN] Add subcommand for executable spec

  #480 opened 2 months ago by dc-mak
  0

• [CN] Divergence in CN verification

  #451 opened 3 months ago by elaustell
  14

• CN-exec: double space before `=` causes bad source injection

  #445 opened 3 months ago by dc-mak
  1

• CN-exec: Struct equality bug/regression

  #444 opened 2 months ago by dc-mak
  1

• [CN-Exec] Postconditions not checked due to use of `return`

  #419 opened 3 months ago by ZippeyKeys12
  7

• [CN] Semantics of `unchanged` is confusing (eg. local vars, changed vars)

  #443 opened 3 months ago by septract
  5

• CN: Better syntax for referring to mutable variables (unchanged, {...}@start, {...}@end)

  #472 opened 2 months ago by cp526
  0

• [CN] clarify implementation-defined behaviors

  #406 opened 3 months ago by peterohanley
  8

• [CN] feature: allow mention of function pointers with empty parameter lists

  #438 opened 2 months ago by peterohanley
  2

• CN: Enable lemma CI

  #455 opened 3 months ago by dc-mak
  1

• [CN] missing dependencyh on ocamlgraph?

  #457 opened 3 months ago by bcpierce00
  3

• [CN] crash on unknown sort with external SMT solver

  #435 opened 3 months ago by peterohanley
  3

• CN: Cache cn opam depenedencies in CI

  #456 opened 3 months ago by dc-mak
  0

• [CN] Consider promoting some CN CLI code to `lib`

  #450 opened 3 months ago by samcowger
  0

• CN: Remove Z3 dependency

  #411 opened 3 months ago by cp526
  1

• [CN] feature: Allow undefined structs that are only referenced indirectly

  #437 opened 3 months ago by peterohanley
  0

• [CN] Solver crashes at debug level 5 on any function with an argument.

  #427 opened 3 months ago by ZippeyKeys12
  3

• [CN] Support modulus `%`

  #424 opened 3 months ago by dc-mak
  1

• Build multiplatform CN docker image

  #431 opened 3 months ago by podhrmic
  0

• [CN] Delete solver2.ml

  #423 opened 3 months ago by yav
  1

• [CN] Block should allow omitting C-type like owned

  #414 opened 3 months ago by dc-mak
  1