summaryrefslogtreecommitdiff
path: root/tests/src/external.rs
blob: baea76e41b79440dbc8d467e794adc3be60de089 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
//@ charon-args=--no-code-duplication
//@ aeneas-args=-state -split-files
//@ aeneas-args=-test-trans-units
//@ [coq,fstar] subdir=misc
//! 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;
}