machine_check_common/
iir.rs

1use mck::{abstr::AbstractValue, refin::RefinementValue};
2
3use crate::iir::variable::IVarId;
4
5type IAbstr = mck::misc::Interpretation<IVarId, AbstractValue>;
6type IRefin = mck::misc::Interpretation<IVarId, RefinementValue>;
7
8pub mod context;
9pub mod description;
10pub mod expr;
11pub mod func;
12pub mod path;
13pub mod property;
14pub mod stmt;
15pub mod ty;
16pub mod variable;
17
18fn join_limited(abstr: &IAbstr, refin: &mut IRefin, var_id: IVarId, refin_value: RefinementValue) {
19    let abstr_value = abstr.value(var_id);
20    let refin_value = refin_value.limit(abstr_value);
21    refin.join_value(var_id, refin_value);
22}