Skip to content

Commit 5045693

Browse files
committed
Added interior mutability test with UnsafeCell
1 parent 397ec9f commit 5045693

File tree

3 files changed

+28
-1
lines changed

3 files changed

+28
-1
lines changed
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
use std::cell::UnsafeCell;
2+
3+
fn main() {
4+
let data = UnsafeCell::new(0);
5+
6+
unsafe {
7+
*data.get() += 42;
8+
}
9+
10+
assert!(data.into_inner() == 42)
11+
}
Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
2+
┌─ 1 (root, init)
3+
│ #init ( symbol ( "interior_mut3_fail" ) globalAllocEntry ( 1 , Memory ( allocati
4+
│ function: main
5+
│ span: 67
6+
7+
│ (48 steps)
8+
└─ 3 (stuck, leaf)
9+
rvalueAddressOf ( mutabilityNot , place ( ... local: local ( 1 ) , projection: p
10+
span: 52
11+
12+
13+
┌─ 2 (root, leaf, target, terminal)
14+
│ #EndProgram
15+
16+

kmir/src/tests/integration/test_integration.py

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -436,7 +436,7 @@ def test_prove(spec: Path, tmp_path: Path, kmir: KMIR) -> None:
436436

437437
PROVING_DIR = (Path(__file__).parent / 'data' / 'prove-rs').resolve(strict=True)
438438
PROVING_FILES = list(PROVING_DIR.glob('*.rs'))
439-
PROVE_RS_SHOW_SPECS = ['local-raw-fail', 'interior-mut-fail', 'interior-mut2-fail']
439+
PROVE_RS_SHOW_SPECS = ['local-raw-fail', 'interior-mut-fail', 'interior-mut2-fail', 'interior-mut3-fail']
440440

441441

442442
@pytest.mark.parametrize(

0 commit comments

Comments
 (0)