val aux_print_reg_from_location (a: location{ALocReg? a}) : string
let aux_print_reg_from_location (a:location{ALocReg? a}) : string =
  let ALocReg (Reg file id) = a in
  match file with
  | 0 -> print_reg_name id
  | 1 -> print_xmm id gcc
val aux_print_reg_from_location (a: location{ALocReg? a}) : string
let aux_print_reg_from_location (a: location{ALocReg? a}) : string =
let ALocReg (Reg file id) = a in
match file with
| 0 -> print_reg_name id
| 1 -> print_xmm id gcc
Vale.Transformers.Locations.fst.checked
Vale.X64.Print_s.fst.checked Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Machine_s.fst.checked Vale.X64.Instructions_s.fsti.checked Vale.X64.Instruction_s.fsti.checked Vale.X64.Bytes_Code_s.fst.checked Vale.Def.PossiblyMonad.fst.checked Vale.Arch.HeapTypes_s.fst.checked Vale.Arch.Heap.fsti.checked prims.fst.checked FStar.Universe.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.FunctionalExtensionality.fsti.checked FStar.Classical.fsti.checked
Vale.Transformers.Locations.fst
Vale.Transformers.Locations.location Prims.b2t Vale.Transformers.Locations.uu___is_ALocReg Vale.X64.Machine_s.reg_file_id Vale.X64.Machine_s.reg_id Vale.X64.Print_s.print_reg_name Vale.X64.Print_s.print_xmm Vale.X64.Print_s.gcc Prims.string
module Vale.Transformers.Locations

open Vale.Arch.HeapTypes_s
open Vale.Arch.Heap
open Vale.X64.Bytes_Code_s
open Vale.X64.Instruction_s
open Vale.X64.Instructions_s
open Vale.X64.Machine_Semantics_s
open Vale.X64.Machine_s
open Vale.X64.Print_s

open Vale.Def.PossiblyMonad

module L = FStar.List.Tot

(* See fsti *)
type location : eqtype =
  | ALocMem : location
  | ALocStack: location
  | ALocReg : reg -> location
  | ALocCf : location
  | ALocOf : location
val aux_print_reg_from_location (a: location{ALocReg? a}) : string
a: Vale.Transformers.Locations.location{ALocReg? a} -> Prims.string