Skip to content
  • Fonenantsoa Maurica's avatar
    Addresses Julien's review no.2: · 78f9aaab
    Fonenantsoa Maurica authored
    MAJOR:
    - malloc and free
      - Distinct tables for malloc and free
      - Efficient insertion of free and malloc
      - Remove entries for malloc and free when they are not needed anymore
    - Using kf instead of fundec
    - Using closure of vi_at: not (straightforwardly) possible
    - Logic scope:
      - No Lscope.top
      - Proper reseting of the lscope
      - Proper binding of logic variables
      - Module Env.Logic_scope
    - Comment for the over-approximation of t_size
    
    STYLE:
    - No useless new lines
    - Spaces
    - Parentheses
    - Latex style for formula in comment of index_from_sizes_and_shifts
    - match -> function
    - Logical variable -> logic variable
    - Renaming:
      - add_to_lscope ->  extend_lscope
      - memory_infos_from_quantifs -> sizes_and_shifts_from_quantifs
      - res -> sizes_and_shifts, memory_infos -> sizes_and_shifts
    - Typos
    - Forward references at the end of the mli
    - Consistent ordering of arguments inside Lscope API
    
    OTHERS:
    - Auxiliary function append_block_of_env_to_block
    - Squash pattern matching of mk_storing_loops
    - No Interval.infer in to_exp
    - Refactoring of pre_from_label
    - pi_beta_j with fold_left
    - No superfluous env for sizes_and_shifts_from_quantifs
    - More efficient accumulator for computing size
    - Squash pattern matching of sizes_and_shifts_from_quantifs
    - No superfluous option for get_lscope_var
    - Better definition of effective_lscope_from_pred_or_term
    - Using List.find for defining get_lscope_var
    - Do not export get_lscope_var
    - Lscope.empty () -> Lscope.empty
    78f9aaab