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
Vale.X64.Flags.fst.hints
[
"��W���\u0017m�Y�͚�t�",
[
[
"Vale.X64.Flags.upd",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Flags.flag_val_t", "equation_Vale.X64.Flags.t",
"equation_Vale.X64.Machine_s.flag",
"function_token_typing_Vale.X64.Flags.flag_val_t", "int_inversion",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomUpd1",
"lemma_FStar.Set.lemma_equal_elim",
"lemma_FStar.Set.lemma_equal_intro",
"lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_empty",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_2ea34cbc8e73c89468af536d5146da5a",
"refinement_interpretation_Tm_refine_72758763fd3a331db555502c82719e64",
"typing_FStar.Map.domain", "typing_FStar.Map.upd",
"typing_FStar.Set.complement", "typing_FStar.Set.empty",
"typing_Vale.X64.Machine_s.flag"
],
0,
"f81a5ad3c12f74e6bf82fb6f0cdba97f"
],
[
"Vale.X64.Flags.of_fun",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Vale.X64.Flags_interpretation_Tm_arrow_6d1d81ae558d658d7d34082785eb5144",
"data_typing_intro_FStar.Pervasives.Native.None@tok",
"equation_Prims.eqtype", "equation_Vale.X64.Flags.flag_val_t",
"equation_Vale.X64.Machine_s.flag",
"function_token_typing_Prims.bool",
"function_token_typing_Prims.int",
"function_token_typing_Vale.X64.Flags.flag_val_t",
"haseqTm_refine_a29663a141e931174462ff96f2d1bbb5", "int_inversion",
"int_typing", "lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomConstMap",
"lemma_FStar.Map.lemma_SelUpd1", "lemma_FStar.Map.lemma_SelUpd2",
"lemma_FStar.Map.lemma_UpdDomain",
"lemma_FStar.Set.lemma_equal_elim",
"lemma_FStar.Set.lemma_equal_intro",
"lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_empty",
"lemma_FStar.Set.mem_union", "primitive_Prims.op_BarBar",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Negation", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_72758763fd3a331db555502c82719e64",
"refinement_interpretation_Tm_refine_a29663a141e931174462ff96f2d1bbb5",
"refinement_kinding_Tm_refine_a29663a141e931174462ff96f2d1bbb5",
"typing_FStar.Map.const", "typing_FStar.Map.domain",
"typing_FStar.Map.upd", "typing_FStar.Set.complement",
"typing_FStar.Set.empty", "typing_FStar.Set.singleton",
"typing_FStar.Set.union", "typing_Vale.X64.Machine_s.flag"
],
0,
"8c332660635067e63dd733f6516de158"
],
[
"Vale.X64.Flags.lemma_upd_eq",
1,
1,
0,
[
"@query", "function_token_typing_Vale.X64.Flags.sel",
"function_token_typing_Vale.X64.Flags.upd",
"interpretation_Tm_abs_9fabf848a1a32f51b141d5916bad7662",
"interpretation_Tm_abs_dee13f6801a03886b79150447bc19803"
],
0,
"65ba459e06c9d90641c015f5a85a958a"
],
[
"Vale.X64.Flags.lemma_upd_ne",
1,
1,
0,
[
"@query", "function_token_typing_Vale.X64.Flags.sel",
"function_token_typing_Vale.X64.Flags.upd",
"interpretation_Tm_abs_9fabf848a1a32f51b141d5916bad7662",
"interpretation_Tm_abs_dee13f6801a03886b79150447bc19803"
],
0,
"0d9b58a8dfebb535ca1f2f333823a58c"
],
[
"Vale.X64.Flags.lemma_equal_intro",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_Vale.X64.Flags.equal",
"equation_Vale.X64.Flags.flag_val_t", "equation_Vale.X64.Flags.t",
"equation_Vale.X64.Machine_s.flag",
"function_token_typing_Vale.X64.Flags.flag_val_t",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_equal_elim",
"lemma_FStar.Set.lemma_equal_elim",
"refinement_interpretation_Tm_refine_2ea34cbc8e73c89468af536d5146da5a",
"typing_FStar.Map.domain", "typing_FStar.Set.complement",
"typing_FStar.Set.empty", "typing_Vale.X64.Machine_s.flag"
],
0,
"4e76aff233552761f5570485ba55269d"
],
[
"Vale.X64.Flags.lemma_equal_elim",
1,
1,
0,
[
"@query", "eq2-interp", "equation_Vale.X64.Flags.equal",
"equation_Vale.X64.Flags.t"
],
0,
"17a8cb83fde5dd48d46198774eb669a9"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...