Oops, same issue in my cbmc version. 
Fixed: http://svn.clifford.at/handicraft/2018/cbmc/bsort.c …
Proving that what I do in check?b() is sufficient to prove that it is a permutation, given that elements of data[] are only copied, is left as an exercise for the reader. 
(Spoiler: It's probably not. :)
-
This Tweet is unavailable.
-
This Tweet is unavailable.
-
This Tweet is unavailable.
-
This Tweet is unavailable.
-
Well, actually afaict the antecedent is insufficient because it does not only depend on the type of write-op performed (copy in this case) but we'd also need to define the set of read-ops allowed by the algorithm (just > in this case).
Assume an algorithm that checks if one of the data[] elements has all-bits set. Say if all bits are set on at one element, then we copy that to all the other elements, otherwise we sort. This will pass that checker even though it does not sort in all cases.
-
-
For the case where SZ<=8*sizeof(T) I can easily see that my check is sufficient for the case where all data elements are distinct. But there is an argument to be had here that we use SMT solvers because we don't want to make arguments like that using our inferior human brains. :)
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.