Opencv case study

[MorelElian]

** on branch main**
Issues both with case_studies/opencv/box_filter_rowsum_model.ml and case_studies/opencv/box_filter_rowsum.ml, same error :
Resource computation error: Pure resource not found: range_check: is_subrange(0../*@__564*/(0 + 1)/*__564@*/, 0..n) In context: @ in_range(/*@__564*/0 + 1/*__564@*/, 0..n) _Fraction in_range(c, 0..cn) c: int __is_false(w == 5) bool __is_false(w == 3) bool __is_true(cn >= 0) __is_true(n >= 1) __is_true(w >= 0) cn: int n: int D: uint16_t* S: uint8_t* w: int reduce_spe1: @ matrix3_span_shift: @ matrix2_span_shift: @ MATRIX3_MEMSET_double: @ MATRIX2_MEMSET_double: @ MATRIX1_MEMSET_double: @ MATRIX3_MEMSET_float: @ MATRIX2_MEMSET_float: @ MATRIX1_MEMSET_float: @ MATRIX3_MEMSET_int: @ MATRIX2_MEMSET_int: @ MATRIX1_MEMSET_int: @ MATRIX3_COPY_double: @ MATRIX2_COPY_double: @ MATRIX1_COPY_double: @ MATRIX3_COPY_float: @ MATRIX2_COPY_float: @ MATRIX1_COPY_float: @ MATRIX3_COPY_int: @ MATRIX2_COPY_int: @ MATRIX1_COPY_int: @ ro_matrix3_unfocus: @ ro_matrix3_focus: @ ro_matrix2_unfocus: @ ro_matrix2_focus: @ ro_matrix1_unfocus: @ ro_matrix1_focus: @ ...
on transformation:

!! Reduce.first_then_slide ~mark_alloc:"acc" [nbMulti; cMark "anyw"; cFor "i"]; 

[Bastacyclop]

This might be due to a change in __GHOST(group_split):

  // __requires("bound_check: in_range(split, range(start, stop, step))");
  __requires("range_check: is_subrange(range(start, split, step), range(start, stop, step))");

[Bastacyclop]

I guess the type checker has some decision rules for in_range but not for is_subrange. @charguer

[charguer]

Instances of in_range are automatically generated when typing for-loops. See definition of and call to the function contract_inside_loop. We don't want to extend the typer to discharge complex "is_subrange" propositions. The solution here is to introduce a ghost that requires in_range(split, range(start, stop, step)) and produces is_subrange(range(start, split, step), range(start, stop, step))");