Refactor annotlib.acsl preds & logic functions to ensure sound casting of ptrs (void ptrs in particular)

[jennalwise]

WP's Typed+cast memory model (Byte not implemented yet) does support heterogeneous casts of polymorphic void ptrs, so long as it is casted to the proper type ptr that it should be.

Ie.

    bool b = (bool)true;
    bool *b_ptr = &b;
    void* f = (void*)b_ptr;
    //@ assert \valid((bool*)f);

Therefore, annotlib.acsl predicates and logic functions must be refactored to ensure sound casting of void ptrs. Otherwise, proofs will be unsound following the Typed+cast memory model.

[jennalwise]

I can fairly easily correct valid predicates involving void ptrs for the built-in GraphBLAS types only (see experimental-no-eva branch for these annotations), but the annotated logic for separated predicates will become extremely verbose/inelegant if they are refactored to ensure sound casting of ptrs. However, running the Value Analysis plug-in before running WP will prove separated and valid predicates with heterogenous casts (including ones with function pointers) without any refactoring or unsoundness. This is the best option, because the annotations will be simpler and written the way they should be for when the Byte model is introduced. The only downside is not relying solely on WP for verification (at this time).