-
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