Skip to content
Merged

Rustup #5252

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
55 commits
Select commit Hold shift + click to select a range
3a46d4a
MaybeDangling: ensure references fit inside the address space
RalfJung Aug 8, 2026
7d9e141
[Priroda] Add bootstrap test and check steps
moabo3li Aug 6, 2026
0a3157f
[Priroda] Add rust_2018_idioms lint, bootstrap check, and clippy step
moabo3li Aug 8, 2026
d57f033
Auto merge of #160674 - scottmcm:wait-what-happened, r=folkertdev
bors Aug 9, 2026
e9a7eb3
Rollup merge of #158404 - Dnreikronos:trait_solver/canonicalize_next_…
JonathanBrouwer Aug 10, 2026
b78b71c
Rollup merge of #160631 - Kobzol:bootstrap-rustfmt, r=jieyouxu
JonathanBrouwer Aug 10, 2026
36c9087
Rollup merge of #160642 - davidtwco:sve-field-projection, r=folkertdev
JonathanBrouwer Aug 10, 2026
61f2b2c
Rollup merge of #160749 - RalfJung:maybe-dangling-address-space, r=Wa…
JonathanBrouwer Aug 10, 2026
dea4025
Rollup merge of #160791 - Walnut356:enum_recog, r=Kobzol
JonathanBrouwer Aug 10, 2026
d9ce1e1
Rollup merge of #160500 - bb1yd:same-message-for-crate-and-pathroot, …
JonathanBrouwer Aug 10, 2026
ac5b7ae
Rollup merge of #160590 - nia-e:libs-refactor-adjustments, r=clarfonthey
JonathanBrouwer Aug 10, 2026
2f90d23
Rollup merge of #160825 - vita-rust:fix-references-unsupported-vita, …
JonathanBrouwer Aug 10, 2026
1f8a018
Rollup merge of #160852 - ChrisDenton:rmdirall, r=jieyouxu
JonathanBrouwer Aug 10, 2026
74063f7
Auto merge of #160867 - JonathanBrouwer:rollup-bas1App, r=JonathanBro…
bors Aug 10, 2026
49c0ce4
Rollup merge of #160629 - moabo3li:priroda-bootstrap-ci, r=oli-obk
JonathanBrouwer Aug 10, 2026
394d331
Rollup merge of #160811 - zalanlevai:160464-perf-regression, r=Jonath…
JonathanBrouwer Aug 10, 2026
16fe267
Rollup merge of #154329 - VicenteGusmao:fix-bug-151304, r=lcnr
JonathanBrouwer Aug 10, 2026
e185a12
Rollup merge of #157841 - Kivooeo:fix-let-pat-inferred-wf, r=lcnr
JonathanBrouwer Aug 10, 2026
14fa208
Rollup merge of #159300 - DanielEScherzer:bytestr-to-string, r=clarfo…
JonathanBrouwer Aug 10, 2026
1454e72
Rollup merge of #160858 - zakrad:regr-test-91514, r=JohnTitor
JonathanBrouwer Aug 10, 2026
2fda644
Rollup merge of #160864 - ada4a:rename-HostEffectPredicate, r=oli-obk
JonathanBrouwer Aug 10, 2026
b1f69e1
Auto merge of #160801 - nnethercote:new-solver-probes, r=jdonszelmann
bors Aug 10, 2026
c88caf3
Auto merge of #160879 - JonathanBrouwer:rollup-4zAylRT, r=JonathanBro…
bors Aug 11, 2026
8e8db21
Rollup merge of #160872 - steffahn:put_back_homu-ignore, r=jieyouxu
jhpratt Aug 11, 2026
fc27421
Rollup merge of #160432 - joboet:ensure_init_generic, r=clarfonthey
jhpratt Aug 11, 2026
7c88c4a
Rollup merge of #160865 - makai410:debug-static, r=nnethercote
jhpratt Aug 11, 2026
a29d80c
Rollup merge of #160866 - rustbot:docs-update, r=traviscross
jhpratt Aug 11, 2026
de8f1d9
Rollup merge of #160881 - malezjaa:implement_new_init, r=clarfonthey
jhpratt Aug 11, 2026
f6860e2
Auto merge of #160888 - jhpratt:rollup-OY2pQdT, r=jhpratt
bors Aug 11, 2026
48dbff8
Auto merge of #160818 - Mark-Simulacrum:smaller-try, r=Kobzol
bors Aug 11, 2026
b44c7f0
Miri: give the incremental session a chance to finish
RalfJung Aug 8, 2026
5ae6928
fix unused features in Miri tests
RalfJung Aug 8, 2026
c076c24
Rollup merge of #158510 - Amanieu:static-pie-gnu, r=saethlin
JonathanBrouwer Aug 14, 2026
7d04f56
Rollup merge of #160441 - beetrees:inline-asm-fix-powerpc64le, r=Amanieu
JonathanBrouwer Aug 14, 2026
cdb9d0b
Rollup merge of #160760 - RalfJung:miri-incremental, r=bjorn3
JonathanBrouwer Aug 14, 2026
a69537d
Rollup merge of #160892 - nnethercote:new-solver-inlining, r=jdonszel…
JonathanBrouwer Aug 14, 2026
55fb69a
Rollup merge of #160821 - jaroslawroszyk:main, r=clarfonthey
JonathanBrouwer Aug 14, 2026
a87af17
Rollup merge of #160997 - jyn514:agents-md, r=jieyouxu
JonathanBrouwer Aug 14, 2026
dbdf109
Rollup merge of #161057 - estebank:issue-92685-part-deux, r=jieyouxu
JonathanBrouwer Aug 14, 2026
05d12a1
Rollup merge of #161079 - Zalathar:config-macros, r=jieyouxu
JonathanBrouwer Aug 14, 2026
0e4b22c
Rollup merge of #161080 - zedddie:projection_may_match-rerun-no-eased…
JonathanBrouwer Aug 14, 2026
be6dd83
Rollup merge of #161085 - Zalathar:normalize-selectors, r=Kobzol
JonathanBrouwer Aug 14, 2026
bcf1f75
Rollup merge of #161086 - cyrgani:test-3, r=Kivooeo
JonathanBrouwer Aug 14, 2026
b497aaf
Auto merge of #161093 - JonathanBrouwer:rollup-ZAPw9dB, r=JonathanBro…
bors Aug 14, 2026
42aa790
Auto merge of #161077 - nnethercote:CanonicalizerState, r=jdonszelmann
bors Aug 14, 2026
72a650f
Auto merge of #161047 - lcnr:implied-bounds-opaque-only-next, r=adwin…
bors Aug 15, 2026
a83e6d8
Auto merge of #161106 - cuviper:version-100, r=Mark-Simulacrum
bors Aug 15, 2026
60f3fb7
fix buggy MaybeDangling<&T> validation logic
RalfJung Aug 15, 2026
7c98956
Rollup merge of #161125 - RalfJung:MaybeDangling-validity, r=saethlin
JonathanBrouwer Aug 15, 2026
4771c54
Rollup merge of #159971 - amirHdev:fix-missing-placeholder-assumption…
JonathanBrouwer Aug 15, 2026
c0147d9
Auto merge of #161143 - JonathanBrouwer:rollup-hgQTzZ3, r=JonathanBro…
bors Aug 15, 2026
93ba2f6
Prepare for merging from rust-lang/rust
RalfJung Aug 16, 2026
1397f3a
Merge ref '67854e511de2' from rust-lang/rust
RalfJung Aug 16, 2026
a221a2d
fmt, clippy
saethlin Aug 14, 2026
91fb03e
bless and fix tests
RalfJung Aug 16, 2026
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -156,7 +156,8 @@ jobs:
- name: check build
run: |
cd ../rust # ./x does not seem to like being invoked from elsewhere
./x check miri
# checks every tool in that folder (including priroda)
./x check src/tools/miri

# This job is intentionally separate from `test` so that Priroda can be
# developed as a separate crate inside the Miri repository for now.
Expand Down
9 changes: 9 additions & 0 deletions priroda/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ repository = "https://github.com/rust-lang/miri"
version = "0.1.0"
edition = "2024"

[workspace]

[[bin]]
name = "priroda"
Expand All @@ -24,6 +25,14 @@ miri = { path = ".." }
[package.metadata.rust-analyzer]
rustc_private = true

# Same lint policy as miri/src/lib.rs.
[lints.rust]
rust_2018_idioms = "warn"

[lints.clippy]
as_conversions = "warn"
manual_let_else = "warn"

[dev-dependencies]
ui_test = "0.30.2"
regex = "1.5.5"
51 changes: 23 additions & 28 deletions priroda/src/debugger.rs
Original file line number Diff line number Diff line change
Expand Up @@ -377,14 +377,11 @@ impl<'tcx> PrirodaContext<'tcx> {
/// Initialized bytes are shown in hexadecimal, uninitialized bytes as `??`,
/// and complete pointer-sized provenance as pointer markers.
fn render_mplace_bytes(&self, mplace: &MPlaceTy<'tcx>) -> InterpResult<'tcx, String> {
let size = match self.ecx.size_and_align_of_val(mplace)? {
Some((size, _)) => size,
None => {
// Extern types cannot currently be executed as by-value locals,
// so this path cannot yet be covered by a Priroda UI fixture.
// FIXME: Add coverage once Priroda supports printing dereferenced places.
return interp_ok("<unsupported-unsized>".to_string());
}
let Some((size, _)) = self.ecx.size_and_align_of_val(mplace)? else {
// Extern types cannot currently be executed as by-value locals,
// so this path cannot yet be covered by a Priroda UI fixture.
// FIXME: Add coverage once Priroda supports printing dereferenced places.
return interp_ok("<unsupported-unsized>".to_string());
};

let size = size.bytes_usize();
Expand Down Expand Up @@ -508,20 +505,19 @@ impl<'tcx> PrirodaContext<'tcx> {
// view before fields can be projected. Structs use their sole
// variant directly. Keep the display name tied to the same choice.
let (variant_idx, down, name) = if def.is_enum() {
let variant_idx = match self.ecx.read_discriminant(&op).discard_err() {
Some(variant_idx) => variant_idx,
let Some(variant_idx) = self.ecx.read_discriminant(&op).discard_err() else {
// FIXME: expose this as an explicit render error when
// Priroda grows structured value states. Falling back to
// bytes keeps today's UI usable but hides why the enum
// could not be source-shaped.
None => return self.render_op(op),
return self.render_op(op);
};
let down = match self.ecx.project_downcast(&op, variant_idx).discard_err() {
Some(down) => down,
let Some(down) = self.ecx.project_downcast(&op, variant_idx).discard_err()
else {
// FIXME: distinguish invalid/uninitialized discriminants
// from projection bugs in the rendered output once locals
// can carry structured diagnostics.
None => return self.render_op(op),
return self.render_op(op);
};
let variant_def = &def.variants()[variant_idx];
(
Expand All @@ -542,12 +538,12 @@ impl<'tcx> PrirodaContext<'tcx> {
let field_idx = FieldIdx::from_usize(i);
// `project_field` avoids manual offset math and works for both
// immediate and memory-backed operands through `Projectable`.
let field_op = match self.ecx.project_field(&down, field_idx).discard_err() {
Some(field_op) => field_op,
let Some(field_op) = self.ecx.project_field(&down, field_idx).discard_err()
else {
// FIXME: preserve the successfully rendered fields and
// mark only this field as unavailable once the value model
// can represent partial render failures.
None => return self.render_op(op),
return self.render_op(op);
};
fields.push(self.render_source_shaped_op_inner(field_op, depth + 1));
}
Expand Down Expand Up @@ -578,14 +574,14 @@ impl<'tcx> PrirodaContext<'tcx> {
for i in 0..args.len() {
// Tuples have no field names in source, so preserve their
// source field order and render children positionally.
let field_op =
match self.ecx.project_field(&op, FieldIdx::from_usize(i)).discard_err() {
Some(field_op) => field_op,
// FIXME: render tuple fields independently so one
// projection failure does not throw away the whole
// source-shaped tuple.
None => return self.render_op(op),
};
let Some(field_op) =
self.ecx.project_field(&op, FieldIdx::from_usize(i)).discard_err()
else {
// FIXME: render tuple fields independently so one
// projection failure does not throw away the whole
// source-shaped tuple.
return self.render_op(op);
};
fields.push(self.render_source_shaped_op_inner(field_op, depth + 1));
}

Expand All @@ -600,11 +596,10 @@ impl<'tcx> PrirodaContext<'tcx> {
// `project_array_fields` uses the dynamic length for slices. That
// avoids the classic mistake of treating slice layout as a fixed
// zero-length array.
let mut iter = match self.ecx.project_array_fields(&op).discard_err() {
Some(iter) => iter,
let Some(mut iter) = self.ecx.project_array_fields(&op).discard_err() else {
// FIXME: when slice metadata is invalid, show that as a slice
// length problem instead of silently falling back to raw bytes.
None => return self.render_op(op),
return self.render_op(op);
};

let mut fields = Vec::new();
Expand Down
2 changes: 1 addition & 1 deletion priroda/src/frontend/dap.rs
Original file line number Diff line number Diff line change
Expand Up @@ -553,7 +553,7 @@ impl<R: Read, W: Write> DapSession<R, W> {
let mut breakpoints = Vec::new();
if let Some(ref req_bps) = args.breakpoints {
for req_bp in req_bps {
let line = req_bp.line as usize;
let line = usize::try_from(req_bp.line).unwrap();
session.set_breakpoint(path.clone(), line);
breakpoints.push(DapBreakpoint {
verified: true,
Expand Down
7 changes: 0 additions & 7 deletions priroda/src/main.rs
Original file line number Diff line number Diff line change
@@ -1,19 +1,12 @@
#![feature(rustc_private)]

extern crate miri;
extern crate rustc_abi;
extern crate rustc_codegen_ssa;
extern crate rustc_data_structures;
extern crate rustc_driver;
extern crate rustc_hir;
extern crate rustc_hir_analysis;
extern crate rustc_index;
extern crate rustc_interface;
extern crate rustc_log;
extern crate rustc_middle;
extern crate rustc_session;
extern crate rustc_span;
extern crate rustc_type_ir;

mod debugger;
mod frontend;
Expand Down
2 changes: 1 addition & 1 deletion rust-version
Original file line number Diff line number Diff line change
@@ -1 +1 @@
4667d75565e47ba5df36c0df598c556b543e8624
67854e511de21d881bb16426996cd4259d44aa2e
106 changes: 84 additions & 22 deletions src/bin/miri.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ extern crate rustc_data_structures;
extern crate rustc_driver;
extern crate rustc_interface;
extern crate rustc_log;
extern crate rustc_metadata;
extern crate rustc_middle;
extern crate rustc_session;

Expand All @@ -21,6 +22,7 @@ rustc_driver::override_c_allocator_in_binary!();

mod log;

use std::any::Any;
use std::env;
use std::num::{NonZero, NonZeroI32};
use std::ops::Range;
Expand All @@ -34,6 +36,7 @@ use miri::{
TreeBorrowsParams, ValidationMode, entry_fn, run_genmc_mode,
};
use rustc_codegen_ssa::traits::CodegenBackend;
use rustc_codegen_ssa::{CompiledModules, CrateInfo, TargetConfig};
use rustc_data_structures::sync::{self, DynSync};
use rustc_driver::Compilation;
use rustc_interface::interface::Config;
Expand All @@ -51,6 +54,13 @@ struct MiriCompilerCalls {
many_seeds: Option<ManySeedsConfig>,
}

struct MiriCodegenBackend {
native: Box<dyn CodegenBackend>,
dummy: DummyCodegenBackend,
/// Whether we are in a dependency or in the to-be-interpreted binary crate
dep: bool,
}

struct ManySeedsConfig {
seeds: Range<u32>,
keep_going: bool,
Expand Down Expand Up @@ -97,39 +107,27 @@ fn run_many_seeds(
/// Generates the codegen backend for code that Miri will interpret: we basically
/// use the dummy backend, except that we put the LLVM backend in charge of
/// target features.
fn make_miri_codegen_backend(sess: &Session) -> Box<dyn CodegenBackend> {
fn make_miri_codegen_backend(sess: &Session, dep: bool) -> Box<dyn CodegenBackend> {
let early_dcx = EarlyDiagCtxt::new(sess.opts.error_format);

// Use the target_config method of the default codegen backend (eg LLVM) to ensure the
// calculated target features match said backend by respecting eg -Ctarget-cpu.
let target_config_backend = rustc_interface::util::get_codegen_backend(
let native_codegen_backend = rustc_interface::util::get_codegen_backend(
&early_dcx,
&sess.opts.sysroot,
None,
&sess.target,
);
target_config_backend.init(sess);
native_codegen_backend.init(sess);

Box::new(DummyCodegenBackend {
target_config_override: Some(Box::new(move |sess| {
let mut cfg = target_config_backend.target_config(sess);
// The basic types and ABI always work.
cfg.has_reliable_f16 = true;
cfg.has_reliable_f128 = true;
// We always provide the f16 intrinsics, but some are provided via the host,
// so forward its reliability.
cfg.has_reliable_f16_math = cfg!(target_has_reliable_f16_math);
// Many f128 operations are still missing.
cfg.has_reliable_f128_math = false;
cfg
})),
})
Box::new(MiriCodegenBackend { native: native_codegen_backend, dummy: DummyCodegenBackend, dep })
}

impl rustc_driver::Callbacks for MiriCompilerCalls {
fn config(&mut self, config: &mut rustc_interface::interface::Config) {
// We never reach codegen anyway.
config.make_codegen_backend = Some(Box::new(make_miri_codegen_backend));
config.make_codegen_backend =
Some(Box::new(|sess| make_miri_codegen_backend(sess, /* dep */ false)));

// Register our custom extra symbols.
config.extra_symbols = miri::sym::EXTRA_SYMBOLS.into();
Expand Down Expand Up @@ -201,12 +199,73 @@ impl rustc_driver::Callbacks for MiriCompilerCalls {
// Process interpreter result.
if let Err(return_code) = res {
tcx.dcx().abort_if_errors();
exit(return_code.get());
exit(return_code.get())
} else {
exit(rustc_driver::EXIT_SUCCESS);
// We want to continue here so rustc can do its usual shutdown and finalize the
// incremental session. Our custom codegen backend ensures nothing actually happens.
Compilation::Continue
}
}
}

impl CodegenBackend for MiriCodegenBackend {
fn name(&self) -> &'static str {
"miri"
}

fn target_config(&self, sess: &Session) -> TargetConfig {
let native_target_config = self.native.target_config(sess);
TargetConfig {
internal_target_features: native_target_config.internal_target_features,

// Unreachable.
// The basic types and ABI always work.
has_reliable_f16: true,
has_reliable_f128: true,
// We always provide the f16 intrinsics, but some are provided via the host,
// so forward its reliability.
has_reliable_f16_math: cfg!(target_has_reliable_f16_math),
// Many f128 operations are still missing.
has_reliable_f128_math: false,
}
}

fn target_cpu(&self, _sess: &Session) -> String {
String::new()
}

// Everything complicated is forwarded to the dummy backend.

fn supported_crate_types(&self, sess: &Session) -> Vec<CrateType> {
self.dummy.supported_crate_types(sess)
}

fn codegen_crate<'tcx>(&self, tcx: TyCtxt<'tcx>) -> Box<dyn Any> {
self.dummy.codegen_crate(tcx)
}

fn join_codegen(
&self,
ongoing_codegen: Box<dyn Any>,
sess: &Session,
incr_comp_session: Option<&rustc_session::IncrCompSession>,
outputs: &rustc_session::config::OutputFilenames,
crate_info: &CrateInfo,
) -> (CompiledModules, rustc_middle::dep_graph::WorkProductMap) {
self.dummy.join_codegen(ongoing_codegen, sess, incr_comp_session, outputs, crate_info)
}

fn link(
&self,
sess: &Session,
compiled_modules: CompiledModules,
crate_info: CrateInfo,
metadata: rustc_metadata::EncodedMetadata,
outputs: &rustc_session::config::OutputFilenames,
) {
// In the binary this should do nothing.
if self.dep {
self.dummy.link(sess, compiled_modules, crate_info, metadata, outputs)
}
}
}

Expand All @@ -217,7 +276,8 @@ impl rustc_driver::Callbacks for MiriDepCompilerCalls {
#[allow(rustc::potential_query_instability)] // rustc_codegen_ssa (where this code is copied from) also allows this lint
fn config(&mut self, config: &mut Config) {
// We don't need actual codegen, we just emit an rlib that Miri can later consume.
config.make_codegen_backend = Some(Box::new(make_miri_codegen_backend));
config.make_codegen_backend =
Some(Box::new(|sess| make_miri_codegen_backend(sess, /* dep */ true)));

// Avoid warnings about unsupported crate types. However, only do that we we are *not* being
// queried by cargo about the supported crate types so that cargo still receives the
Expand Down Expand Up @@ -683,4 +743,6 @@ fn main() -> ExitCode {
}
}
run_compiler_and_exit(&rustc_args, &mut MiriCompilerCalls::new(miri_config, many_seeds))
// Note that we *cannot* just return here, in native-lib mode we have to coordinate
// with the supervisor process!
}
2 changes: 1 addition & 1 deletion src/diagnostics.rs
Original file line number Diff line number Diff line change
Expand Up @@ -237,7 +237,7 @@ pub fn prune_stacktrace<'tcx>(
/// Report the result of a Miri execution.
///
/// Returns `Some` if this was regular program termination with a given exit code and a `bool`
/// indicating whether a leak check should happen; `None` otherwise.
/// indicating whether a leak check should happen; `None` if execution was aborted with an error.
pub fn report_result<'tcx>(
ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
res: InterpErrorInfo<'tcx>,
Expand Down
4 changes: 2 additions & 2 deletions src/eval.rs
Original file line number Diff line number Diff line change
Expand Up @@ -510,8 +510,8 @@ fn call_main<'tcx>(
}

/// Evaluates the entry function specified by `entry_id`.
/// Returns `Some(return_code)` if program execution completed.
/// Returns `None` if an evaluation error occurred.
/// Returns `Ok(())` if program execution completed with exit code 0.
/// Returns `Err(code)` if an evaluation error occurred or the program returned a non-0 exit code.
pub fn eval_entry<'tcx>(
tcx: TyCtxt<'tcx>,
entry_id: DefId,
Expand Down
7 changes: 7 additions & 0 deletions tests/fail/validity/maybe_dangling_ref_too_big.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
#![feature(maybe_dangling)]
use std::mem::{MaybeDangling, transmute};

fn main() {
let _x: MaybeDangling<&i8> = unsafe { transmute(usize::MAX) };
//~^ERROR: too close to the end of the address space
}
13 changes: 13 additions & 0 deletions tests/fail/validity/maybe_dangling_ref_too_big.stderr
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
error: Undefined Behavior: constructing invalid value of type std::mem::MaybeDangling<&i8>: encountered a reference that is too close to the end of the address space for a pointee of 1 bytes
--> tests/fail/validity/maybe_dangling_ref_too_big.rs:LL:CC
|
LL | let _x: MaybeDangling<&i8> = unsafe { transmute(usize::MAX) };
| ^^^^^^^^^^^^^^^^^^^^^ Undefined Behavior occurred here
|
= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information

note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace

error: aborting due to 1 previous error

2 changes: 2 additions & 0 deletions tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -27,3 +27,5 @@ LL | | )
| |_________^

Verification complete with 2 executions. No errors found.
warning: 1 warning emitted

2 changes: 2 additions & 0 deletions tests/genmc/pass/atomics/cas_simple.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -18,3 +18,5 @@ LL | let _ = VALUE.compare_exchange_weak(99, 99, Relaxed, SeqCst);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code

Verification complete with 1 executions. No errors found.
warning: 3 warnings emitted

Loading