Crucible/LLVM: crucible_elem can't make a pointer one past the end

[langston-barrett]

It is legal according to the C standard to calculate pointers to one past the end of an allocation, so long as they aren't dereferenced. However, we don't have the capability to express this in SAWscript:

/*
  nix-shell --pure -p "with import (fetchTarball https://github.com/NixOS/nixpkgs-channels/archive/nixos-19.03.tar.gz) {}; clang_7" --run "clang -g -O1 -emit-llvm -c *.c"
  nix-shell --pure -p "with import (fetchTarball https://github.com/NixOS/nixpkgs-channels/archive/nixos-19.03.tar.gz) {}; llvm_7" --run "llvm-dis *.bc"
*/

#include "stdlib.h"
#include "string.h"

typedef struct {
  char* begin;
  char* end;
} range;

void make_range(range* r, char* data) {
  memset(data, 0, 10);
  r->begin = data;
  r->end = data+10; // one past the end, technically legal if not dereferenced
}

m <- llvm_load_module "test.bc";
let spec = do {
  range_ptr <- crucible_alloc (llvm_type "%struct.range");
  data_ptr <- crucible_alloc (llvm_array 10 (llvm_int 8));
  crucible_execute_func [range_ptr, data_ptr];
  crucible_points_to data_ptr (crucible_term {{ zero : [10][8] }});
  crucible_points_to (crucible_field range_ptr "begin") data_ptr;
  // Neither of these works:
  // crucible_points_to (crucible_field range_ptr "end") (crucible_elem data_ptr 9);
  // crucible_points_to (crucible_field range_ptr "end") (crucible_elem data_ptr 10);
};
crucible_llvm_verify m "make_range" [] false spec z3;

[22:31:09.379] "crucible_llvm_verify" (/home/siddharthist/code/tmp/range-2/test.saw:12:1-12:21):
at /home/siddharthist/code/tmp/range-2/test.saw:12:1
could not match specified value with actual value:
  actual (simulator) value: concrete pointer: allocation = 5, offset = 10
  specified value:          concrete pointer: allocation = 5, offset = 9
  type of actual value:    i8*
  type of specified value: i8*

[22:17:41.093] "crucible_llvm_verify" (/home/siddharthist/code/tmp/range/test.saw:11:1-11:21):
"spec" (/home/siddharthist/code/tmp/range/test.saw:11:46-11:50):
"crucible_points_to" (/home/siddharthist/code/tmp/range/test.saw:9:3-9:21):
typeOfSetupValue: array type index out of bounds: (10,10)

[langston-barrett]

Fixed in #519