(* Generated by coq-of-rust *)
Require Import CoqOfRust.CoqOfRust.

(*
fn main() {
    use std::arch::asm;

    fn load_fpu_control_word(control: u16) {
        unsafe {
            asm!("fldcw [{}]", in(reg) &control, options(nostack));
        }
    }
}
*)
Definition main (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [] => ltac:(M.monadic (Value.Tuple []))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_main : M.IsFunction "inline_assembly_memory_address_operands::main" main.

Module main.
  (*
      fn load_fpu_control_word(control: u16) {
          unsafe {
              asm!("fldcw [{}]", in(reg) &control, options(nostack));
          }
      }
  *)
  Definition load_fpu_control_word (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ control ] =>
      ltac:(M.monadic
        (let control := M.alloc (| control |) in
        M.read (|
          let~ _ := InlineAssembly in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_load_fpu_control_word :
    M.IsFunction
      "inline_assembly_memory_address_operands::main::load_fpu_control_word"
      load_fpu_control_word.
End main.
