Struct Jiffies 

pub struct Jiffies(/* private fields */);

Jiffies is a term used to denote the units of time measurement by the kernel.

A jiffy represents one tick of the system timer interrupt, whose frequency is equal to TIMER_FREQ Hz.

Implementations

impl Jiffies

pub open spec fn duration_secs(self) -> u64

{ self@ / TIMER_FREQ }

The whole-second component of this jiffy count.

pub open spec fn duration_nanos(self) -> u32

{ (((self@ % TIMER_FREQ) * 1_000_000_000u64) / (TIMER_FREQ as int)) as u32 }

The subsecond nanosecond component of this jiffy count.

impl Jiffies

pub const MAX: Self

The maximum value of Jiffies.

impl Jiffies

pub exec fn new(value: u64) -> ret : Self

ensures

ret@ == value,

Creates a new instance.

pub exec fn elapsed() -> Self

Returns the elapsed time since the system boots up.

pub exec fn as_u64(self) -> u64

returns

self@,

Gets the number of jiffies.

pub exec fn add(&mut self, jiffies: u64)

ensures

final(self)@ == old(self)@.saturating_add(jiffies),

Adds the given number of jiffies, saturating at Jiffies::MAX on overflow.

pub exec fn as_duration(self) -> Duration

returns

Duration::new(self.duration_secs(), self.duration_nanos()),

Gets the Duration calculated from the jiffies counts.

Trait Implementations

impl Clone for Jiffies

fn clone(&self) -> Jiffies

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Jiffies

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl From<Jiffies> for Duration

exec fn from(value: Jiffies) -> Self

impl FromSpecImpl<Jiffies> for Duration

open spec fn obeys_from_spec() -> bool

{ true }

open spec fn from_spec(value: Jiffies) -> Duration

{ Duration::new(value.duration_secs(), value.duration_nanos()) }

impl View for Jiffies

closed spec fn view(&self) -> Self::V

type V = u64

impl Copy for Jiffies