rapx/analysis/senryx/contracts/
checker.rs

1use super::abstract_state::*;
2use super::contract::*;
3use core::mem;
4use std::collections::HashMap;
5use std::marker::PhantomData;
6
7pub trait Checker<'tcx> {
8    fn variable_contracts(&self) -> &HashMap<usize, Vec<Contract<'tcx>>>;
9}
10
11pub struct SliceFromRawPartsChecker<'tcx, T> {
12    pub variable_contracts: HashMap<usize, Vec<Contract<'tcx>>>,
13    _marker: PhantomData<T>,
14}
15
16impl<'tcx, T> Checker<'tcx> for SliceFromRawPartsChecker<'tcx, T> {
17    fn variable_contracts(&self) -> &HashMap<usize, Vec<Contract<'tcx>>> {
18        &self.variable_contracts
19    }
20}
21
22impl<'tcx, T> SliceFromRawPartsChecker<'tcx, T> {
23    pub fn new() -> Self {
24        let mut map = HashMap::new();
25        map.insert(
26            0,
27            vec![
28                // Contract::StateCheck {
29                //     op: Op::GE,
30                //     state: StateType::AllocatedState(AllocatedState::Alloc),
31                // },
32                Contract::StateCheck {
33                    op: Op::GT,
34                    state: StateType::AlignState(AlignState::Unaligned),
35                },
36            ],
37        );
38        map.insert(
39            1,
40            vec![Contract::ValueCheck {
41                op: Op::LE,
42                value: Value::Usize((isize::MAX as usize) / mem::size_of::<T>()),
43            }],
44        );
45        Self {
46            variable_contracts: map,
47            _marker: PhantomData,
48        }
49    }
50}
rapx/analysis/senryx/contracts/checker.rs

rapx/analysis/senryx/contracts/
checker.rs
