Function isla_axiomatic::footprint_analysis::footprint_analysis[−][src]

pub fn footprint_analysis<'ir, B>(
    num_threads: usize, 
    thread_buckets: &[Vec<EvPath<B>>], 
    lets: &Bindings<'ir, B>, 
    regs: &Bindings<'ir, B>, 
    shared_state: &SharedState<'_, B>, 
    isa_config: &ISAConfig<B>, 
    cache: Option<&Path>
) -> Result<HashMap<B, Footprint>, FootprintError> where
    B: BV, 

Arguments

  • num_threads - How many threads to use for analysing footprints
  • thread_buckets - A vector of paths (event vectors) for each thread in the litmus test
  • lets - The initial state of all top-level letbindings in the Sail specification
  • regs - The initial register state
  • shared_state - The state shared between all symbolic execution runs
  • isa_config - The architecture specific configuration information
  • cache_dir - A directory to cache footprint results