Basile Clément
Basile Clément
> I don't understand anymore why `Dummy.Array.blit` does not check for dummies in the source array. This does not seem correct? (Memory-safety is lost if two different dummies end up...
Thanks for the clarification — I was waiting for you to confirm the comment on `blit_assume_room` was not enough to ensure memory safety.
> (My current review state is that I'm waiting to see if @bclement-ocp wants to fix `Dummy.Array.blit` as part of this PR.) Done.
The following tests are failing: ``` List of failed tests: tests/lib-bigarray-2/bigarrcml.ml tests/statmemprof/bigarray.ml ``` but the errors don't seem related to this PR: ``` > Action 3/5 (check-ocamlc.byte-output) => failed (The...
I have pushed a new version taking into account your comments. Regarding the naming of `unsafe_XXX` functions, I went in a different direction: they are still prefixed with `unsafe_`, but...
Fixed by #1126.
Note: from dev meeting this looks like this is an extensionality issue; we should look at extensionality witness techniques
> I believe we already implement the extensionality witness technique: This is not an extensionality witness (edit: to clarify; this is one half of an extensionality witness since it only...
> Our implementation of ArrayEx is complete I am not sure this is true; we reply `unknown` for the following problem which is clearly `unsat` (arrays `a` and `b` are...
FWIW, if I manually introduce an extensionality witness for arrays `a` and `b` with ```smt-lib (declare-const ext Int) (assert (=> (= (select a ext) (select b ext)) (= a b)))...