machine-check-common 0.7.1

Utility crate for the formal verification tool machine-check
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

use mck::{abstr::AbstractValue, refin::RefinementValue};

use crate::iir::variable::IVarId;

type IAbstr = mck::misc::Interpretation<IVarId, AbstractValue>;
type IRefin = mck::misc::Interpretation<IVarId, RefinementValue>;

pub mod context;
pub mod description;
pub mod expr;
pub mod func;
pub mod path;
pub mod property;
pub mod stmt;
pub mod ty;
pub mod variable;

fn join_limited(abstr: &IAbstr, refin: &mut IRefin, var_id: IVarId, refin_value: RefinementValue) {
    let abstr_value = abstr.value(var_id);
    let refin_value = refin_value.limit(abstr_value);
    refin.join_value(var_id, refin_value);
}