Skip to main content

Browse the archive

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 
Merge pull request #298 from project-everest/vdum_ocaml_nits
 
OCaml API: Don't run unit tests which require unsupported features
2 parent s 760addb + 28f416c
Raw File
Vale.AES.X64.AESCTRplain.fsti.hints 
[
  "�\u0015P��f��m�B��I�J",
  [
    [
      "Vale.AES.X64.AESCTRplain.va_lemma_Aes_counter_loop",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_dff147d5c995aa65a971b362dbc2897b"
      ],
      0,
      "02b1aadfb3dd5481a9142863dc2a3768"
    ],
    [
      "Vale.AES.X64.AESCTRplain.va_wp_Aes_counter_loop",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "63fad50784c1fe3f21a59218bc1cd937"
    ],
    [
      "Vale.AES.X64.AESCTRplain.va_quick_Aes_counter_loop",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "77c53e21c704dcf5bf1dafc1604f3405"
    ]
  ]
]
back to top