Search results

[Fulminate] Missing instrumentation under non-loop labels

Status: Open.

#479 In rems-project/cn;

· rbanerjee20 opened on Dec 11, 2025

[Seq-Test] Make Fulminate usage consistent with new API

CN sequence testing

Status: Open.

#470 In rems-project/cn;

· ZippeyKeys12 opened on Dec 3, 2025

[Testing] Gradual Rustification of runtime libraries

BennetRelated to input generation via random backtracking search. Available via `cn test`Related to input generation via random backtracking search. Available via `cn test`

CN spec testingRelated to Bennet, Darcy, or the shared infrastructure for running spec-based random testing.Related to Bennet, Darcy, or the shared infrastructure for running spec-based random testing.

DarcyRelated to input generation via constraint solving. Available via `cn test --symbolic`Related to input generation via constraint solving. Available via `cn test --symbolic`

Status: Open.

Task

#462 In rems-project/cn;

· ZippeyKeys12 opened on Nov 21, 2025

[Fulminate] Clarify Fulminate API

Status: Open.

#461 In rems-project/cn;

· ZippeyKeys12 opened on Nov 21, 2025

[Testing] Separate test runner

CN spec testingRelated to Bennet, Darcy, or the shared infrastructure for running spec-based random testing.Related to Bennet, Darcy, or the shared infrastructure for running spec-based random testing.

Status: Open.

#459 In rems-project/cn;

· ZippeyKeys12 opened on Nov 21, 2025

[Bennet] Support CN value generation

BennetRelated to input generation via random backtracking search. Available via `cn test`Related to input generation via random backtracking search. Available via `cn test`

CN spec testingRelated to Bennet, Darcy, or the shared infrastructure for running spec-based random testing.Related to Bennet, Darcy, or the shared infrastructure for running spec-based random testing.

Status: Open.

Feature

#457 In rems-project/cn;

· ZippeyKeys12 opened on Nov 21, 2025

[Fulminate] Generate functions for spec-checking

FulminateRelated to CN executable spec generation, called using `cn instrument`Related to CN executable spec generation, called using `cn instrument`

Status: Open.

Task

#454 In rems-project/cn;

· rbanerjee20 opened on Nov 19, 2025

[CN-exec] Provenance issue: function prologues have to be inserted before CN_LOAD

bugSomething isn't workingSomething isn't working

FulminateRelated to CN executable spec generation, called using `cn instrument`Related to CN executable spec generation, called using `cn instrument`

Status: Open.

Bug

#453 In rems-project/cn;

· moratorium08 opened on Nov 19, 2025

[CN-exec] Missing instrumentation for ghost arguments at call sites when goto/tag is used

bugSomething isn't workingSomething isn't working

FulminateRelated to CN executable spec generation, called using `cn instrument`Related to CN executable spec generation, called using `cn instrument`

Status: Open.

Bug

#452 In rems-project/cn;

· moratorium08 opened on Nov 19, 2025

Fix div, mod, pointer-diff in bitvector mode

Status: Open.

#438 In rems-project/cn;

· cp526 opened on Nov 9, 2025

[Testing] Better handling of globals

CN spec testingRelated to Bennet, Darcy, or the shared infrastructure for running spec-based random testing.Related to Bennet, Darcy, or the shared infrastructure for running spec-based random testing.

Status: Open.

#420 In rems-project/cn;

· ZippeyKeys12 opened on Nov 4, 2025

[CN-Exec] Incorrect instrumentation for the use of return values

Status: Open.

#392 In rems-project/cn;

· moratorium08 opened on Oct 28, 2025