Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Finish allocate_dtyp_spec_fin_inf and handle_alloca_fin_inf.
- extend_stack_frame_fin_inf does need to be proved for allocate_dtyp_spec_fin_inf - May need to rearrange model_E1E2_23_orutt_strict to use MemState_refine_prop... :|
- Loading branch information