// Set up argv
.decl argv_alloc(alloc: BasicAllocation)
argv_alloc("*argv-alloc").
basic_allocation(argvAlloc) :- argv_alloc(argvAlloc).
dynamically_sized_alloc(argvAlloc) :- argv_alloc(argvAlloc).

// The construction of subregion allocations depends on knowing the type, so we
// have to ascribe one here.
static_allocation_type(argvAlloc, i8PtrPtrType) :-
  int8_type(i8),
  argv_alloc(argvAlloc),
  pointer_type_has_component(i8PtrType, i8),
  pointer_type_has_component(i8PtrPtrType, i8PtrType).

.decl argv_ptr_points_to(from: Allocation, to: Allocation)

// Create a separate string allocation for each pointer in argv
basic_allocation(newAlloc),
static_allocation_type(newAlloc, i8PtrType),
argv_ptr_points_to(subAlloc, newAlloc),
dynamically_sized_alloc(newAlloc)
  :-
  argv_alloc(argvAlloc),
  static_subobjects.alloc_subregion_at_array_index(argvAlloc, index, subAlloc),
  int8_type(i8),
  pointer_type_has_component(i8PtrType, i8),
  newAlloc = cat(cat("*argv[", to_string(index)), "]-alloc").

.decl argv_var_points_to(?aCtx: Context, ?alloc: Allocation, ?ctx: Context, ?var: Variable)
argv_var_points_to(aCtx, argvAlloc, mainCtx, argvVar) :-
  main_func(main),
  argv_alloc(argvAlloc),
  func_param(main, 1, argvVar),
  empty_alloc_context(aCtx),
  main_context(mainCtx).
