Error message involving loading presumably arbitrarily-aligned pointer could be improved

[nano-o]

In the following example, test_4 casts an unsigned char (which I presume may be considered arbitrarily aligned by SAW) to an unsigned long and loads it into an unsigned long. Although the error message contains the information, it is not immediately clear that there is an alignment error. In this case it is pretty easy to find out, but I can imagine it could be harder when the memory state is bigger. Maybe SAW could print on the first line that it is an alignment error.

void test_4(unsigned char * ptr) {
  unsigned long * ptr_ = (unsigned long *)ptr;
  unsigned long l = *ptr_;
}

m <- llvm_load_module "/workdir/test_4.o.bc";

let alloc_init ty v = do {
  p <- crucible_alloc ty;
  crucible_points_to p v;
  return p;
};

let ptr_to_fresh n ty = do {
  x <- crucible_fresh_var n ty;
  p <- alloc_init ty (crucible_term x);
  return (x, p);
};

let test_4_spec = do {
  (_, ptr) <- ptr_to_fresh "ptr" (llvm_array 8 (llvm_int 1));
  crucible_execute_func [ptr];
};

_ <- crucible_llvm_verify m "test_4" [] false test_4_spec abc;

[01:40:00.911] Simulating test_4 ...
[01:40:00.911] Stack trace:
"crucible_llvm_verify" (/workdir/tests/misc/test_4.saw:20:6-20:26):
Symbolic execution failed.
Abort due to false assumption:
  Error during memory load
  in test_4 at /workdir/tests/misc/test_4.c:3:21
  Details:
  Operation failed due to previous errors: 
  While concatenating bitvectors
    Operation failed due to previous errors: 
    While concatenating bitvectors
      Operation failed due to previous errors: 
      While concatenating bitvectors
        Operation failed due to previous errors: 
        While concatenating bitvectors
          Operation failed due to previous errors: 
          While concatenating bitvectors
            Operation failed due to previous errors: 
            While concatenating bitvectors
              Unexpected argument type:
              Non-byte-sized bitvectors
                bitvectorType 1
                bitvectorType 1
Stack frame
  Allocations:

  Writes:

Base memory
  Allocations:
    HeapAlloc 3 0x8:[64] Mutable 1-byte-aligned /workdir/tests/misc/test_4.saw:4:8
    GlobalAlloc 2 0x0:[64] Immutable 1-byte-aligned test_4
    GlobalAlloc 1 0x0:[64] Immutable 1-byte-aligned llvm.dbg.declare
  Writes:
    Indexed chunk:
      3 |->
        *(3, 0x0:[64]) := [c@5:bv
                          ,c@6:bv
                          ,c@7:bv
                          ,c@8:bv
                          ,c@9:bv
                          ,c@10:bv
                          ,c@11:bv
                          ,c@12:bv]

[atomb]

It could be that our upcoming refactoring of the LLVM memory model might make it easier to make this clearer, especially if we keep this sort of thing in mind as we go.