From 12b0b4f2477604c606cd3701b5b427b8f9181129 Mon Sep 17 00:00:00 2001 From: Lasse Letager Hansen Date: Thu, 22 Feb 2024 17:07:16 +0100 Subject: [PATCH] testing --- .../toolchain__reordering into-ssprove.snap | 103 +++++++ .../toolchain__side-effects into-ssprove.snap | 275 ++++++++++++++++++ tests/enum-repr/Cargo.toml | 2 +- tests/enum-struct-variant/Cargo.toml | 1 + tests/if-let/Cargo.toml | 2 +- tests/literals/Cargo.toml | 1 + tests/loops/Cargo.toml | 1 + tests/nested-derefs/Cargo.toml | 2 +- tests/pattern-or/Cargo.toml | 1 + tests/reordering/Cargo.toml | 2 +- tests/side-effects/Cargo.toml | 1 + 11 files changed, 387 insertions(+), 4 deletions(-) create mode 100644 test-harness/src/snapshots/toolchain__reordering into-ssprove.snap create mode 100644 test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap diff --git a/test-harness/src/snapshots/toolchain__reordering into-ssprove.snap b/test-harness/src/snapshots/toolchain__reordering into-ssprove.snap new file mode 100644 index 000000000..c510de7b5 --- /dev/null +++ b/test-harness/src/snapshots/toolchain__reordering into-ssprove.snap @@ -0,0 +1,103 @@ +--- +source: test-harness/src/harness.rs +expression: snapshot +info: + kind: + Translate: + backend: ssprove + info: + name: reordering + manifest: reordering/Cargo.toml + description: ~ + spec: + optional: false + broken: false + issue_id: ~ + positive: true + snapshot: + stderr: false + stdout: true + include_flag: ~ +--- +exit = 0 + +[stdout] +diagnostics = [] + +[stdout.files] +"Reordering.v" = ''' +(* File automatically generated by Hacspec *) +Set Warnings "-notation-overridden,-ambiguous-paths". +From Crypt Require Import choice_type Package Prelude. +Import PackageNotation. +From extructures Require Import ord fset. +From mathcomp Require Import word_ssrZ word. +From Jasmin Require Import word. + +From Coq Require Import ZArith. +From Coq Require Import Strings.String. +Import List.ListNotations. +Open Scope list_scope. +Open Scope Z_scope. +Open Scope bool_scope. + +From Hacspec Require Import ChoiceEquality. +From Hacspec Require Import LocationUtility. +From Hacspec Require Import Hacspec_Lib_Comparable. +From Hacspec Require Import Hacspec_Lib_Pre. +From Hacspec Require Import Hacspec_Lib. + +Open Scope hacspec_scope. +Import choice.Choice.Exports. + +Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations. + +Definition t_Foo : choice_type := + ('unit ∐ 'unit). +Notation "'Foo_A_case'" := (inl tt) (at level 100). +Equations Foo_A {L : {fset Location}} {I : Interface} : both L I t_Foo := + Foo_A := + solve_lift (ret_both (inl (tt : 'unit) : t_Foo)) : both L I t_Foo. +Fail Next Obligation. +Notation "'Foo_B_case'" := (inr tt) (at level 100). +Equations Foo_B {L : {fset Location}} {I : Interface} : both L I t_Foo := + Foo_B := + solve_lift (ret_both (inr (tt : 'unit) : t_Foo)) : both L I t_Foo. +Fail Next Obligation. + +(*Not implemented yet? todo(item)*) + +Equations f {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 int32) : both L1 I1 t_Foo := + f _ := + Foo_A : both L1 I1 t_Foo. +Fail Next Obligation. + +Equations no_dependency_1_ {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit := + no_dependency_1_ _ := + solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit. +Fail Next Obligation. + +Equations no_dependency_2_ {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit := + no_dependency_2_ _ := + solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit. +Fail Next Obligation. + +Definition t_Bar : choice_type := + (t_Foo). +Equations 0 {L : {fset Location}} {I : Interface} (s : both L I t_Bar) : both L I t_Foo := + 0 s := + bind_both s (fun x => + solve_lift (ret_both (x : t_Foo))) : both L I t_Foo. +Fail Next Obligation. +Equations Build_t_Bar {L0 : {fset Location}} {I0 : Interface} {0 : both L0 I0 t_Foo} : both L0 I0 (t_Bar) := + Build_t_Bar := + bind_both 0 (fun 0 => + solve_lift (ret_both ((0) : (t_Bar)))) : both L0 I0 (t_Bar). +Fail Next Obligation. +Notation "'Build_t_Bar' '[' x ']' '(' '0' ':=' y ')'" := (Build_t_Bar (0 := y)). + +Equations g {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 t_Bar := + g _ := + Bar (solve_lift (f (ret_both (32 : int32)))) : both L1 I1 t_Bar. +Fail Next Obligation. +''' diff --git a/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap b/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap new file mode 100644 index 000000000..01ca06526 --- /dev/null +++ b/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap @@ -0,0 +1,275 @@ +--- +source: test-harness/src/harness.rs +expression: snapshot +info: + kind: + Translate: + backend: ssprove + info: + name: side-effects + manifest: side-effects/Cargo.toml + description: ~ + spec: + optional: false + broken: false + issue_id: ~ + positive: true + snapshot: + stderr: true + stdout: true + include_flag: ~ +--- +exit = 0 +stderr = ''' +Compiling side-effects v0.1.0 (WORKSPACE_ROOT/side-effects) + Finished dev [unoptimized + debuginfo] target(s) in XXs''' + +[stdout] +diagnostics = [] + +[stdout.files] +"Side_effects.v" = ''' +(* File automatically generated by Hacspec *) +Set Warnings "-notation-overridden,-ambiguous-paths". +From Crypt Require Import choice_type Package Prelude. +Import PackageNotation. +From extructures Require Import ord fset. +From mathcomp Require Import word_ssrZ word. +From Jasmin Require Import word. + +From Coq Require Import ZArith. +From Coq Require Import Strings.String. +Import List.ListNotations. +Open Scope list_scope. +Open Scope Z_scope. +Open Scope bool_scope. + +From Hacspec Require Import ChoiceEquality. +From Hacspec Require Import LocationUtility. +From Hacspec Require Import Hacspec_Lib_Comparable. +From Hacspec Require Import Hacspec_Lib_Pre. +From Hacspec Require Import Hacspec_Lib. + +Open Scope hacspec_scope. +Import choice.Choice.Exports. + +Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations. + +(*Not implemented yet? todo(item)*) + +Equations add3 {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I1 : Interface} {I2 : Interface} {I3 : Interface} (x : both L1 I1 int32) (y : both L2 I2 int32) (z : both L3 I3 int32) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) int32 := + add3 x y z := + solve_lift (impl__u32__wrapping_add (impl__u32__wrapping_add x y) z) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) int32. +Fail Next Obligation. + +Equations direct_result_question_mark {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result 'unit int32)) : both L1 I1 (t_Result int8 int32) := + direct_result_question_mark y := + solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := impl__map_err y f_from in + Result_Ok (Result_Ok (ret_both (0 : int8))))) : both L1 I1 (t_Result int8 int32). +Fail Next Obligation. + +Equations direct_result_question_mark_coercion {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result int8 int16)) : both L1 I1 (t_Result int8 int32) := + direct_result_question_mark_coercion y := + solve_lift (run (letm[choice_typeMonad.result_bind_code int32] hoist1 := impl__map_err y f_from in + Result_Ok (Result_Ok hoist1))) : both L1 I1 (t_Result int8 int32). +Fail Next Obligation. + +Equations early_returns {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both L1 I1 int32 := + early_returns x := + solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (3 : int32)) + then letm[choice_typeMonad.result_bind_code int32] hoist2 := v_Break (ret_both (0 : int32)) in + ControlFlow_Continue (never_to_any hoist2) + else () in + letb hoist3 := x >.? (ret_both (30 : int32)) in + letm[choice_typeMonad.result_bind_code int32] hoist5 := ifb hoist3 + then matchb ret_both (true : 'bool) with + | true => + letm[choice_typeMonad.result_bind_code int32] hoist4 := v_Break (ret_both (34 : int32)) in + ControlFlow_Continue (solve_lift (never_to_any hoist4)) + | _ => + ControlFlow_Continue (solve_lift (ret_both (3 : int32))) + end + else ControlFlow_Continue (letb _ := assign todo(term) in + x .+ (ret_both (1 : int32))) in + letb hoist6 := impl__u32__wrapping_add (ret_both (123 : int32)) hoist5 in + letb hoist7 := impl__u32__wrapping_add hoist6 x in + letm[choice_typeMonad.result_bind_code int32] hoist8 := v_Break hoist7 in + ControlFlow_Continue (never_to_any hoist8))) : both L1 I1 int32. +Fail Next Obligation. + +Definition y_loc : Location := + (int32;0%nat). +Definition y_loc : Location := + (int32;1%nat). +Equations local_mutation {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both (L1 :|: fset [y_loc;y_loc]) I1 int32 := + local_mutation x := + letb y loc(y_loc) := ret_both (0 : int32) in + letb _ := assign todo(term) in + letb hoist9 := x >.? (ret_both (3 : int32)) in + solve_lift (ifb hoist9 + then letb _ := assign todo(term) in + letb y loc(y_loc) := x ./ (ret_both (2 : int32)) in + letb _ := assign todo(term) in + letb hoist10 := ret_both (0 : int32) in + letb hoist11 := Build_t_Range (f_start := hoist10) (f_end := ret_both (10 : int32)) in + letb hoist12 := f_into_iter hoist11 in + letb _ := foldi_both_list hoist12 (fun i => + ssp (fun _ => + assign todo(term) : (both (*1*)(L1:|:fset [y_loc]) (I1) 'unit))) (ret_both (tt : 'unit)) in + impl__u32__wrapping_add x y + else letb hoist15 := matchb x with + | 12 => + letb _ := assign todo(term) in + solve_lift (ret_both (3 : int32)) + | 13 => + letb hoist14 := x in + letb _ := assign todo(term) in + letb hoist13 := impl__u32__wrapping_add (ret_both (123 : int32)) x in + solve_lift (add3 hoist14 hoist13 x) + | _ => + solve_lift (ret_both (0 : int32)) + end in + letb _ := assign todo(term) in + impl__u32__wrapping_add x y) : both (L1 :|: fset [y_loc;y_loc]) I1 int32. +Fail Next Obligation. + +Equations options {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I1 : Interface} {I2 : Interface} {I3 : Interface} (x : both L1 I1 (t_Option int8)) (y : both L2 I2 (t_Option int8)) (z : both L3 I3 (t_Option int64)) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) (t_Option int8) := + options x y z := + solve_lift (run (letm[choice_typeMonad.option_bind_code] hoist19 := x in + letb hoist20 := hoist19 >.? (ret_both (10 : int8)) in + letm[choice_typeMonad.option_bind_code] hoist26 := ifb hoist20 + then letm[choice_typeMonad.option_bind_code] hoist21 := x in + Option_Some (letb hoist22 := impl__u8__wrapping_add hoist21 (ret_both (3 : int8)) in + Option_Some hoist22) + else letm[choice_typeMonad.option_bind_code] hoist24 := x in + letm[choice_typeMonad.option_bind_code] hoist23 := y in + Option_Some (letb hoist25 := impl__u8__wrapping_add hoist24 hoist23 in + Option_Some hoist25) in + letm[choice_typeMonad.option_bind_code] hoist27 := hoist26 in + letm[choice_typeMonad.option_bind_code] v := matchb hoist27 with + | 3 => + Option_None + | 4 => + letm[choice_typeMonad.option_bind_code] hoist16 := z in + Option_Some (letb hoist17 := hoist16 >.? (ret_both (4 : int64)) in + letb hoist18 := ifb hoist17 + then ret_both (0 : int8) + else ret_both (3 : int8) in + solve_lift ((ret_both (4 : int8)) .+ hoist18)) + | _ => + Option_Some (solve_lift (ret_both (12 : int8))) + end in + letm[choice_typeMonad.option_bind_code] hoist28 := x in + letb hoist30 := impl__u8__wrapping_add v hoist28 in + letm[choice_typeMonad.option_bind_code] hoist29 := y in + Option_Some (letb hoist31 := impl__u8__wrapping_add hoist30 hoist29 in + Option_Some hoist31))) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) (t_Option int8). +Fail Next Obligation. + +Definition y_loc : Location := + (int32;2%nat). +Equations question_mark {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both (L1 :|: fset [y_loc]) I1 (t_Result int32 int32) := + question_mark x := + solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (40 : int32)) + then letb y loc(y_loc) := ret_both (0 : int32) in + letb _ := assign todo(term) in + letb _ := assign todo(term) in + letb _ := assign todo(term) in + letb hoist32 := x >.? (ret_both (90 : int32)) in + ifb hoist32 + then impl__map_err (Result_Err (ret_both (12 : int8))) f_from + else () + else () in + Result_Ok (Result_Ok (impl__u32__wrapping_add (ret_both (3 : int32)) x)))) : both (L1 :|: fset [y_loc]) I1 (t_Result int32 int32). +Fail Next Obligation. + +Definition t_A : choice_type := + 'unit. +Equations Build_t_A : both (fset []) (fset []) (t_A) := + Build_t_A := + solve_lift (ret_both (tt (* Empty tuple *) : (t_A))) : both (fset []) (fset []) (t_A). +Fail Next Obligation. + +Definition t_B : choice_type := + 'unit. +Equations Build_t_B : both (fset []) (fset []) (t_B) := + Build_t_B := + solve_lift (ret_both (tt (* Empty tuple *) : (t_B))) : both (fset []) (fset []) (t_B). +Fail Next Obligation. + +Definition t_Bar : choice_type := + ('bool × nseq ('bool × 'bool) 6 × 'bool). +Equations f_a {L : {fset Location}} {I : Interface} (s : both L I t_Bar) : both L I 'bool := + f_a s := + bind_both s (fun x => + solve_lift (ret_both (fst x : 'bool))) : both L I 'bool. +Fail Next Obligation. +Equations f_b {L : {fset Location}} {I : Interface} (s : both L I t_Bar) : both L I (nseq ('bool × 'bool) 6 × 'bool) := + f_b s := + bind_both s (fun x => + solve_lift (ret_both (snd x : (nseq ('bool × 'bool) 6 × 'bool)))) : both L I (nseq ('bool × 'bool) 6 × 'bool). +Fail Next Obligation. +Equations Build_t_Bar {L0 : {fset Location}} {L1 : {fset Location}} {I0 : Interface} {I1 : Interface} {f_a : both L0 I0 'bool} {f_b : both L1 I1 (nseq ('bool × 'bool) 6 × 'bool)} : both (L0:|:L1) (I0:|:I1) (t_Bar) := + Build_t_Bar := + bind_both f_b (fun f_b => + bind_both f_a (fun f_a => + solve_lift (ret_both ((f_a,f_b) : (t_Bar))))) : both (L0:|:L1) (I0:|:I1) (t_Bar). +Fail Next Obligation. +Notation "'Build_t_Bar' '[' x ']' '(' 'f_a' ':=' y ')'" := (Build_t_Bar (f_a := y) (f_b := f_b x)). +Notation "'Build_t_Bar' '[' x ']' '(' 'f_b' ':=' y ')'" := (Build_t_Bar (f_a := f_a x) (f_b := y)). + +Equations monad_lifting {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int8) : both L1 I1 (t_Result t_A t_B) := + monad_lifting x := + solve_lift (run (ifb x >.? (ret_both (123 : int8)) + then letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist33 := ControlFlow_Continue (impl__map_err (Result_Err B) f_from) in + letb hoist34 := Result_Ok hoist33 in + letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist35 := v_Break hoist34 in + ControlFlow_Continue (never_to_any hoist35) + else ControlFlow_Continue (Result_Ok A))) : both L1 I1 (t_Result t_A t_B). +Fail Next Obligation. + +Definition t_Foo : choice_type := + ('bool × 'bool × t_Vec t_Bar t_Global × nseq t_Bar 6 × t_Bar). +Equations f_x {L : {fset Location}} {I : Interface} (s : both L I t_Foo) : both L I 'bool := + f_x s := + bind_both s (fun x => + solve_lift (ret_both (fst (fst (fst x)) : 'bool))) : both L I 'bool. +Fail Next Obligation. +Equations f_y {L : {fset Location}} {I : Interface} (s : both L I t_Foo) : both L I ('bool × t_Vec t_Bar t_Global) := + f_y s := + bind_both s (fun x => + solve_lift (ret_both (snd (fst (fst x)) : ('bool × t_Vec t_Bar t_Global)))) : both L I ('bool × t_Vec t_Bar t_Global). +Fail Next Obligation. +Equations f_z {L : {fset Location}} {I : Interface} (s : both L I t_Foo) : both L I (nseq t_Bar 6) := + f_z s := + bind_both s (fun x => + solve_lift (ret_both (snd (fst x) : (nseq t_Bar 6)))) : both L I (nseq t_Bar 6). +Fail Next Obligation. +Equations f_bar {L : {fset Location}} {I : Interface} (s : both L I t_Foo) : both L I t_Bar := + f_bar s := + bind_both s (fun x => + solve_lift (ret_both (snd x : t_Bar))) : both L I t_Bar. +Fail Next Obligation. +Equations Build_t_Foo {L0 : {fset Location}} {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I0 : Interface} {I1 : Interface} {I2 : Interface} {I3 : Interface} {f_x : both L0 I0 'bool} {f_y : both L1 I1 ('bool × t_Vec t_Bar t_Global)} {f_z : both L2 I2 (nseq t_Bar 6)} {f_bar : both L3 I3 t_Bar} : both (L0:|:L1:|:L2:|:L3) (I0:|:I1:|:I2:|:I3) (t_Foo) := + Build_t_Foo := + bind_both f_bar (fun f_bar => + bind_both f_z (fun f_z => + bind_both f_y (fun f_y => + bind_both f_x (fun f_x => + solve_lift (ret_both ((f_x,f_y,f_z,f_bar) : (t_Foo))))))) : both (L0:|:L1:|:L2:|:L3) (I0:|:I1:|:I2:|:I3) (t_Foo). +Fail Next Obligation. +Notation "'Build_t_Foo' '[' x ']' '(' 'f_x' ':=' y ')'" := (Build_t_Foo (f_x := y) (f_y := f_y x) (f_z := f_z x) (f_bar := f_bar x)). +Notation "'Build_t_Foo' '[' x ']' '(' 'f_y' ':=' y ')'" := (Build_t_Foo (f_x := f_x x) (f_y := y) (f_z := f_z x) (f_bar := f_bar x)). +Notation "'Build_t_Foo' '[' x ']' '(' 'f_z' ':=' y ')'" := (Build_t_Foo (f_x := f_x x) (f_y := f_y x) (f_z := y) (f_bar := f_bar x)). +Notation "'Build_t_Foo' '[' x ']' '(' 'f_bar' ':=' y ')'" := (Build_t_Foo (f_x := f_x x) (f_y := f_y x) (f_z := f_z x) (f_bar := y)). + +Equations assign_non_trivial_lhs {L1 : {fset Location}} {I1 : Interface} (foo : both L1 I1 t_Foo) : both L1 I1 t_Foo := + assign_non_trivial_lhs foo := + letb _ := assign todo(term) in + letb _ := assign todo(term) in + letb _ := assign todo(term) in + letb _ := assign todo(term) in + letb _ := assign todo(term) in + solve_lift foo : both L1 I1 t_Foo. +Fail Next Obligation. +''' diff --git a/tests/enum-repr/Cargo.toml b/tests/enum-repr/Cargo.toml index eec13f544..cfc6cefdf 100644 --- a/tests/enum-repr/Cargo.toml +++ b/tests/enum-repr/Cargo.toml @@ -6,4 +6,4 @@ edition = "2021" [dependencies] [package.metadata.hax-tests] -into."fstar+coq" = { broken = false, snapshot = "none", issue_id = "162" } +into."fstar+coq+ssprove" = { broken = false, snapshot = "none", issue_id = "162" } diff --git a/tests/enum-struct-variant/Cargo.toml b/tests/enum-struct-variant/Cargo.toml index c6fba86f4..5651c0608 100644 --- a/tests/enum-struct-variant/Cargo.toml +++ b/tests/enum-struct-variant/Cargo.toml @@ -9,3 +9,4 @@ edition = "2021" [package.metadata.hax-tests] into."fstar+coq" = {broken = false, snapshot = "none"} +into."ssprove" = {broken = true, snapshot = "none"} \ No newline at end of file diff --git a/tests/if-let/Cargo.toml b/tests/if-let/Cargo.toml index fe86f0b0e..544318ca9 100644 --- a/tests/if-let/Cargo.toml +++ b/tests/if-let/Cargo.toml @@ -6,4 +6,4 @@ edition = "2021" [dependencies] [package.metadata.hax-tests] -into."fstar+coq" = { broken = false, snapshot = "none", issue_id = "85" } +into."fstar+coq+ssprove" = { broken = false, snapshot = "none", issue_id = "85" } diff --git a/tests/literals/Cargo.toml b/tests/literals/Cargo.toml index f70ce2bfc..319378b16 100644 --- a/tests/literals/Cargo.toml +++ b/tests/literals/Cargo.toml @@ -8,3 +8,4 @@ edition = "2021" [package.metadata.hax-tests] into."fstar" = { broken = false, snapshot = "none", issue_id = "85" } into."coq" = { broken = true, snapshot = "none", issue_id = "85" } +into."ssprove" = { broken = true, snapshot = "none", issue_id = "85" } diff --git a/tests/loops/Cargo.toml b/tests/loops/Cargo.toml index 033a5bf29..a6139c47a 100644 --- a/tests/loops/Cargo.toml +++ b/tests/loops/Cargo.toml @@ -8,3 +8,4 @@ edition = "2021" [package.metadata.hax-tests] into."fstar" = { } into."coq" = { broken = true, snapshot = "none", issue_id = "137" } +into."ssprove" = { broken = true, snapshot = "none", issue_id = "137" } diff --git a/tests/nested-derefs/Cargo.toml b/tests/nested-derefs/Cargo.toml index f40fa4504..d28b7545e 100644 --- a/tests/nested-derefs/Cargo.toml +++ b/tests/nested-derefs/Cargo.toml @@ -4,4 +4,4 @@ version = "0.1.0" edition = "2021" [package.metadata.hax-tests] -into."fstar+coq" = { snapshot = "none" } +into."fstar+coq+ssprove" = { snapshot = "none" } diff --git a/tests/pattern-or/Cargo.toml b/tests/pattern-or/Cargo.toml index abce1ec8e..31b4a1901 100644 --- a/tests/pattern-or/Cargo.toml +++ b/tests/pattern-or/Cargo.toml @@ -8,3 +8,4 @@ edition = "2021" [package.metadata.hax-tests] into."coq" = { issue_id = "161" } into."fstar" = { } +# into."ssprove" = { broken = true, snapshot = "none" } \ No newline at end of file diff --git a/tests/reordering/Cargo.toml b/tests/reordering/Cargo.toml index 189657e54..937ec2bf8 100644 --- a/tests/reordering/Cargo.toml +++ b/tests/reordering/Cargo.toml @@ -6,4 +6,4 @@ edition = "2021" [dependencies] [package.metadata.hax-tests] -into."fstar+coq" = { snapshot = "stdout" } +into."fstar+coq+ssprove" = { snapshot = "stdout" } diff --git a/tests/side-effects/Cargo.toml b/tests/side-effects/Cargo.toml index 3f113dc10..f946b27d2 100644 --- a/tests/side-effects/Cargo.toml +++ b/tests/side-effects/Cargo.toml @@ -8,3 +8,4 @@ edition = "2021" [package.metadata.hax-tests] into.fstar = {} into.coq = {broken = true, snapshot = "none", issue_id = 134} +into.ssprove = {}