Revision cef6a8e821f55e71b791555d22b45bd3debc2596 authored by Jonathan Protzenko on 08 May 2020, 16:26:29 UTC, committed by GitHub on 08 May 2020, 16:26:29 UTC
OCaml API: Don't run unit tests which require unsupported features 
2 parent s 760addb + 28f416c
Raw File
Vale.Transformers.DebugPrint.fst.hints
[
  "���\td�Z5�\u001f�PYπ\f",
  [
    [
      "Vale.Transformers.DebugPrint.get_non_space",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "binder_x_4bb2ecabb8dd73bd801eb57f838ec7dc_0",
        "disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
        "equation_FStar.String.char", "fuel_guarded_inversion_Prims.list",
        "subterm_ordering_Prims.Cons"
      ],
      0,
      "35816ee0da20d278b84ecaf313917fc6"
    ],
    [
      "Vale.Transformers.DebugPrint.aux_print_code",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "binder_x_97ef5ff619e486c846fe112d821f649f_0",
        "disc_equation_Vale.X64.Machine_s.Block",
        "disc_equation_Vale.X64.Machine_s.IfElse",
        "disc_equation_Vale.X64.Machine_s.Ins",
        "disc_equation_Vale.X64.Machine_s.While",
        "equation_Vale.X64.Bytes_Code_s.code_t",
        "equation_Vale.X64.Machine_Semantics_s.code",
        "equation_Vale.X64.Machine_Semantics_s.codes",
        "fuel_guarded_inversion_Vale.X64.Machine_s.precode",
        "subterm_ordering_Vale.X64.Machine_s.Block",
        "subterm_ordering_Vale.X64.Machine_s.IfElse",
        "subterm_ordering_Vale.X64.Machine_s.While"
      ],
      0,
      "3c77c4ee15e08fd194760abce1922f37"
    ],
    [
      "Vale.Transformers.DebugPrint.aux_print_code",
      2,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "binder_x_69b3af25a4334715774d1242034fc6f2_0",
        "disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
        "equation_Vale.X64.Bytes_Code_s.codes_t",
        "equation_Vale.X64.Machine_Semantics_s.code",
        "equation_Vale.X64.Machine_Semantics_s.codes",
        "fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
      ],
      0,
      "8cf115952d5ed11347b8651954c9366f"
    ],
    [
      "Vale.Transformers.DebugPrint.get_non_space",
      2,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "binder_x_4bb2ecabb8dd73bd801eb57f838ec7dc_0",
        "disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
        "equation_FStar.String.char", "fuel_guarded_inversion_Prims.list",
        "subterm_ordering_Prims.Cons"
      ],
      0,
      "7c14a0a84515bad767511e9f6e6bdd91"
    ],
    [
      "Vale.Transformers.DebugPrint.aux_print_code",
      3,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "binder_x_97ef5ff619e486c846fe112d821f649f_0",
        "disc_equation_Vale.X64.Machine_s.Block",
        "disc_equation_Vale.X64.Machine_s.IfElse",
        "disc_equation_Vale.X64.Machine_s.Ins",
        "disc_equation_Vale.X64.Machine_s.While",
        "equation_Vale.X64.Bytes_Code_s.code_t",
        "equation_Vale.X64.Machine_Semantics_s.code",
        "equation_Vale.X64.Machine_Semantics_s.codes",
        "fuel_guarded_inversion_Vale.X64.Machine_s.precode",
        "subterm_ordering_Vale.X64.Machine_s.Block",
        "subterm_ordering_Vale.X64.Machine_s.IfElse",
        "subterm_ordering_Vale.X64.Machine_s.While"
      ],
      0,
      "33d064a654e6bb7e55db62de3e2c56e5"
    ],
    [
      "Vale.Transformers.DebugPrint.aux_print_code",
      4,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "binder_x_69b3af25a4334715774d1242034fc6f2_0",
        "disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
        "equation_Vale.X64.Bytes_Code_s.codes_t",
        "equation_Vale.X64.Machine_Semantics_s.code",
        "equation_Vale.X64.Machine_Semantics_s.codes",
        "fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
      ],
      0,
      "7351a4cc31a37c3638b0265c3ef17b99"
    ]
  ]
]
back to top