val locations_of_maddr (m: maddr) (mem: location) : locations
let locations_of_maddr (m:maddr) (mem:location) : locations =
  mem :: (
    match m with
    | MConst _ -> []
    | MReg r _ -> [ALocReg r]
    | MIndex b _ i _ -> [ALocReg b; ALocReg i]
  )
val locations_of_maddr (m: maddr) (mem: location) : locations
let locations_of_maddr (m: maddr) (mem: location) : locations =
mem ::
(match m with
  | MConst _ -> []
  | MReg r _ -> [ALocReg r]
  | MIndex b _ i _ -> [ALocReg b; ALocReg i])
Vale.Transformers.BoundedInstructionEffects.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.Transformers.Locations.fst.checked Vale.Transformers.Locations.fst.checked Vale.Def.PossiblyMonad.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Option.fst.checked FStar.List.Tot.fst.checked FStar.Classical.fsti.checked
Vale.Transformers.BoundedInstructionEffects.fst
Vale.X64.Machine_s.maddr Vale.Transformers.Locations.location Prims.Cons Prims.int Prims.Nil Vale.X64.Machine_s.reg Vale.Transformers.Locations.ALocReg Prims.list Vale.Transformers.Locations.locations
module Vale.Transformers.BoundedInstructionEffects

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

open Vale.Transformers.Locations
friend Vale.Transformers.Locations

module L = FStar.List.Tot
val locations_of_maddr (m: maddr) (mem: location) : locations
m: Vale.X64.Machine_s.maddr -> mem: Vale.Transformers.Locations.location
  -> Vale.Transformers.Locations.locations