All pull requests

Pull requests

• Raise the harness timeout of the cargo_autoharness_fmt_impls test

  #4923·tautschnig opened Sep 30, 2026Member·

  ·
  1

• Report SIMD intrinsics on non-SIMD operands as unsupported

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #4922·srivatsansamraj opened Sep 30, 2026Contributor·

  ·
  1

  1

• Add a weekly Charon update job, and run the LLBC regression in the toolchain job

  #4920·tautschnig opened Sep 30, 2026Member·

  ·
  3

• Automatic toolchain upgrade to nightly-2026-09-25

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #4917·github-actions[bot] opened Sep 30, 2026Bot·

  ·
  1

• Resolve fn-pointer type arguments in contract target paths

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #4916·kasimte opened Sep 30, 2026Contributor·

  ·
  1

  1

• Fill omitted defaulted generic parameters during type resolution

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #4915·kasimte opened Sep 30, 2026Contributor·

  ·
  1

  2

• Add an unstable --target option and a riscv64 machine model

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #4913·calef opened Sep 30, 2026·

  ·

• Say why kani_contract_mode is #[inline] while the other contract markers are not

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #4912·feliperodri opened Sep 30, 2026Member·

  ·
  

• Fail verification when CBMC exits abnormally after reporting results

  Z-EndToEndBenchCI
  #4910·Talha-Dmr opened Sep 29, 2026·

  ·
  1

  2

  

• Treat pointer and Box locals of function items as ordinary variables

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #4892·srivatsansamraj opened Sep 28, 2026Contributor·

  ·
  3

  2

  

• Autoharness: try () when instantiating generic functions

  Z-AutoharnessZ-CompilerBenchCIZ-EndToEndBenchCI
  #4880·wodex1nhaoIeng opened Sep 27, 2026Contributor·

  ·

  · Autoharness
  3

  

• Keep a rustc wrapper out of Kani's build

  [F] Crash
  #4872·feliperodri opened Sep 25, 2026Member·

  ·
  1

  2

  

• Let alloc define the Kani models for its own types

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #4871·feliperodri opened Sep 25, 2026Member·

  ·
  1

• Autoharness: do not derive Arbitrary through a NonNull field

  Z-AutoharnessZ-CompilerBenchCIZ-EndToEndBenchCI
  #4864·srivatsansamraj opened Sep 24, 2026Contributor·

  ·
  5

  

• Autoharness: generate &Wtf8 values with unpaired surrogates

  Z-AutoharnessZ-CompilerBenchCIZ-EndToEndBenchCI
  #4862·srivatsansamraj opened Sep 24, 2026Contributor·

  ·
  1

  7

  

• Remove the unreachable deref_box

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #4861·srivatsansamraj opened Sep 24, 2026Contributor·

  ·
  1

  7

  

• benchcomp: scale the solver-time threshold to whether the SAT instance changed

  [E] Performance[I] CI / Infrastructure
  #4846·feliperodri opened Sep 24, 2026Member·

  ·
  1

  6

  

• Report variadic functions with a non-C ABI as unsupported

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #4836·feliperodri opened Sep 23, 2026Member·

  ·
  1

  5

  

• Handle failed constant evaluation gracefully in reachability

  Z-AutoharnessZ-CompilerBenchCIZ-EndToEndBenchCI
  #4818·feliperodri opened Sep 20, 2026Member·Queued· Autoharness
  1

  3

  

• Add 'kani verify-artifacts' subcommand

  [C] Feature / EnhancementZ-UnstableFeature
  #4600·lovesegfault opened May 20, 2026Contributor·

  ·
  4

  

• Add panics_if precondition to express panic-freedom

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #4230·tautschnig opened Jul 16, 2025Member·

  ·
  1

  

• Re-enable debug_assert in our standard library build

  #4207·tautschnig opened Jul 5, 2025Member·

  ·
  1

  

• Document demonic non-determinism

  #3895·tautschnig opened Feb 18, 2025Member·

  ·
  13

  

• RFC: Attribute to distinguish safety preconditions from panic freedom

  T-RFC
  #3893·tautschnig opened Feb 17, 2025Member·

  ·
  37

  

• Reduce CBMC verbosity to CBMC's default

  #3398·tautschnig opened Jul 31, 2024Member·

  ·
  2