blob: ddd5539f615c0037e52da1b1e5ee7d948d6fa901 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
//@ charon-args=--no-code-duplication
//@ aeneas-args=-state -split-files
//@ aeneas-args=-test-trans-units
//! This module uses external types and functions
use std::cell::Cell;
pub fn use_get(rc: &Cell<u32>) -> u32 {
rc.get()
}
pub fn incr(rc: &mut Cell<u32>) {
*rc.get_mut() += 1;
}
|
