Files

 master

/

should_succeed

/

Copy path

Directory actions

More options

Directory actions

More options

Latest commit

jhjourdan

Fix nightly.

Mar 29, 2025

9b369c1 · Mar 29, 2025

History

History

/

should_succeed

/

Top

Folders and files

Name		Name	Last commit message	Last commit date
parent directory ..
100doors		100doors	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
all_zero		all_zero	Merge remote-tracking branch 'origin/master' into simplify_injections	Feb 25, 2025
arc_and_rc		arc_and_rc	Merge remote-tracking branch 'origin/master' into simplify_injections	Feb 25, 2025
bdd		bdd	Fix CI.	Mar 17, 2025
binary_search		binary_search	Fix CI.	Mar 17, 2025
bitvectors		bitvectors	Fix CI.	Mar 17, 2025
bug		bug	Fix CI.	Mar 17, 2025
cc		cc	Update tests	Mar 18, 2025
cell		cell	Fix CI.	Mar 17, 2025
checked_ops		checked_ops	Fix CI.	Mar 17, 2025
clones		clones	Fix CI.	Mar 17, 2025
closures		closures	Update tests	Mar 18, 2025
constrained_types		constrained_types	Fix CI.	Mar 17, 2025
drop_pair		drop_pair	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
duration		duration	Fix CI.	Mar 17, 2025
filter_positive		filter_positive	Fix CI.	Mar 17, 2025
fmap_indexing		fmap_indexing	Move creusot/tests to tests	Feb 21, 2025
ghost		ghost	Add a test	Mar 19, 2025
hashmap		hashmap	Fix CI?	Mar 24, 2025
heapsort_generic		heapsort_generic	Fix CI.	Mar 17, 2025
hillel		hillel	Fix nightly.	Mar 29, 2025
immut		immut	Merge remote-tracking branch 'origin/master' into simplify_injections	Feb 25, 2025
index_range		index_range	Fix CI.	Mar 17, 2025
inferred_invariants		inferred_invariants	Fix CI.	Mar 17, 2025
inplace_list_reversal		inplace_list_reversal	Move creusot/tests to tests	Feb 21, 2025
insertion_sort		insertion_sort	Fix CI.	Mar 17, 2025
instant		instant	Fix CI.	Mar 17, 2025
integer_ops		integer_ops	Fix CI.	Mar 17, 2025
invariant_moves		invariant_moves	Merge remote-tracking branch 'origin/master' into simplify_injections	Feb 25, 2025
ite_normalize		ite_normalize	Fix CI.	Mar 17, 2025
iterators		iterators	Update tests	Mar 18, 2025
knapsack		knapsack	Fix CI.	Mar 17, 2025
knapsack_full		knapsack_full	Fix CI.	Mar 17, 2025
lang		lang	Fix CI.	Mar 17, 2025
linked_list		linked_list	Fix CI.	Mar 17, 2025
list_index_mut		list_index_mut	Merge remote-tracking branch 'origin/master' into simplify_injections	Feb 25, 2025
list_reversal_lasso		list_reversal_lasso	Fix CI.	Mar 17, 2025
loop		loop	Merge remote-tracking branch 'origin/master' into simplify_injections	Feb 25, 2025
mapping_indexing		mapping_indexing	Move creusot/tests to tests	Feb 21, 2025
mapping_test		mapping_test	Merge remote-tracking branch 'origin/master' into simplify_injections	Feb 25, 2025
match_int		match_int	Merge remote-tracking branch 'origin/master' into simplify_injections	Feb 25, 2025
mc91		mc91	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
mutex		mutex	Fix CI.	Mar 17, 2025
one_side_update		one_side_update	Merge remote-tracking branch 'origin/master' into simplify_injections	Feb 25, 2025
open_inv		open_inv	Merge remote-tracking branch 'origin/master' into simplify_injections	Feb 25, 2025
option		option	Use closure spec inference in the option test	Mar 18, 2025
ord_trait		ord_trait	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
pcell		pcell	Fix CI.	Mar 17, 2025
printing		printing	Fix CI.	Mar 17, 2025
projection_toggle		projection_toggle	Merge remote-tracking branch 'origin/master' into simplify_injections	Feb 25, 2025
projections		projections	Fix CI.	Mar 17, 2025
prophecy		prophecy	Merge remote-tracking branch 'origin/master' into simplify_injections	Feb 25, 2025
purity		purity	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
red_black_tree		red_black_tree	Fix CI.	Mar 17, 2025
replace		replace	Move creusot/tests to tests	Feb 21, 2025
resolve_drop		resolve_drop	Merge remote-tracking branch 'origin/master' into simplify_injections	Feb 25, 2025
resolve_uninit		resolve_uninit	Move creusot/tests to tests	Feb 21, 2025
result		result	Update tests	Mar 18, 2025
rusthorn		rusthorn	Fix CI.	Mar 17, 2025
selection_sort_generic		selection_sort_generic	Fix CI.	Mar 17, 2025
simple_trigger		simple_trigger	Move creusot/tests to tests	Feb 21, 2025
slices		slices	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
sparse_array		sparse_array	Fix CI.	Mar 17, 2025
specification		specification	Fix CI.	Mar 17, 2025
split_borrow		split_borrow	Fix CI.	Mar 17, 2025
std_types		std_types	Merge remote-tracking branch 'origin/master' into simplify_injections	Feb 25, 2025
such_that		such_that	Merge remote-tracking branch 'origin/master' into simplify_injections	Feb 25, 2025
sum		sum	Merge remote-tracking branch 'origin/master' into simplify_injections	Feb 25, 2025
sum_of_odds		sum_of_odds	Fix CI.	Mar 17, 2025
swap_borrows		swap_borrows	Fix CI.	Mar 17, 2025
switch		switch	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
switch_struct		switch_struct	Move creusot/tests to tests	Feb 21, 2025
syntax		syntax	Update tests	Mar 18, 2025
take_first_mut		take_first_mut	Merge remote-tracking branch 'origin/master' into simplify_injections	Feb 25, 2025
termination		termination	Fix CI.	Mar 17, 2025
trait		trait	Fix CI.	Mar 17, 2025
trait_impl		trait_impl	Move creusot/tests to tests	Feb 21, 2025
traits		traits	Fix CI.	Mar 17, 2025
trigger		trigger	Fix CI.	Mar 17, 2025
trigger2		trigger2	Move creusot/tests to tests	Feb 21, 2025
two_modules		two_modules	Fix CI.	Mar 17, 2025
type_constructors		type_constructors	Fix CI.	Mar 17, 2025
type_invariants		type_invariants	Fix CI.	Mar 17, 2025
union_find		union_find	Update tests	Mar 20, 2025
unnest		unnest	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
unused_in_loop		unused_in_loop	Fix CI.	Mar 17, 2025
vecdeque		vecdeque	Fix CI.	Mar 17, 2025
vector		vector	Update tests	Mar 18, 2025
100doors.coma		100doors.coma	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
100doors.rs		100doors.rs	Move creusot/tests to tests	Feb 21, 2025
all_zero.coma		all_zero.coma	In generated coma file, move all the use declaration to the begining …	Mar 7, 2025
all_zero.rs		all_zero.rs	Move creusot/tests to tests	Feb 21, 2025
arc_and_rc.coma		arc_and_rc.coma	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
arc_and_rc.rs		arc_and_rc.rs	Move creusot/tests to tests	Feb 21, 2025
bdd.coma		bdd.coma	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
bdd.rs		bdd.rs	Merge remote-tracking branch 'origin/master' into simplify_injections	Feb 25, 2025
binary_search.coma		binary_search.coma	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
binary_search.rs		binary_search.rs	Move creusot/tests to tests	Feb 21, 2025
checked_ops.coma		checked_ops.coma	Update tests	Mar 18, 2025
checked_ops.rs		checked_ops.rs	Move creusot/tests to tests	Feb 21, 2025
constrained_types.coma		constrained_types.coma	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
constrained_types.rs		constrained_types.rs	Move creusot/tests to tests	Feb 21, 2025
drop_pair.coma		drop_pair.coma	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
drop_pair.rs		drop_pair.rs	Move creusot/tests to tests	Feb 21, 2025
duration.coma		duration.coma	Update tests	Mar 18, 2025
duration.rs		duration.rs	Move creusot/tests to tests	Feb 21, 2025
filter_positive.coma		filter_positive.coma	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
filter_positive.rs		filter_positive.rs	Move creusot/tests to tests	Feb 21, 2025
fmap_indexing.coma		fmap_indexing.coma	In generated coma file, move all the use declaration to the begining …	Mar 7, 2025
fmap_indexing.rs		fmap_indexing.rs	Move creusot/tests to tests	Feb 21, 2025
hashmap.coma		hashmap.coma	Update tests	Mar 18, 2025
hashmap.rs		hashmap.rs	Merge remote-tracking branch 'origin/master' into simplify_injections	Feb 25, 2025
heapsort_generic.coma		heapsort_generic.coma	Update tests	Mar 18, 2025
heapsort_generic.rs		heapsort_generic.rs	test: Remove useless requires in heapsort_generic.rs	Mar 13, 2025
hillel.coma		hillel.coma	Update tests	Mar 18, 2025
hillel.rs		hillel.rs	Move creusot/tests to tests	Feb 21, 2025
immut.coma		immut.coma	In generated coma file, move all the use declaration to the begining …	Mar 7, 2025
immut.rs		immut.rs	Move creusot/tests to tests	Feb 21, 2025
index_range.coma		index_range.coma	Update tests	Mar 18, 2025
index_range.rs		index_range.rs	Move creusot/tests to tests	Feb 21, 2025
inferred_invariants.coma		inferred_invariants.coma	Update tests	Mar 18, 2025
inferred_invariants.rs		inferred_invariants.rs	Move creusot/tests to tests	Feb 21, 2025
inplace_list_reversal.coma		inplace_list_reversal.coma	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
inplace_list_reversal.rs		inplace_list_reversal.rs	Move creusot/tests to tests	Feb 21, 2025
insertion_sort.coma		insertion_sort.coma	Update tests	Mar 18, 2025
insertion_sort.rs		insertion_sort.rs	Move creusot/tests to tests	Feb 21, 2025
instant.coma		instant.coma	Update tests	Mar 18, 2025
instant.rs		instant.rs	Move creusot/tests to tests	Feb 21, 2025
integer_ops.coma		integer_ops.coma	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
integer_ops.rs		integer_ops.rs	Move creusot/tests to tests	Feb 21, 2025
invariant_moves.coma		invariant_moves.coma	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
invariant_moves.rs		invariant_moves.rs	Move creusot/tests to tests	Feb 21, 2025
ite_normalize.coma		ite_normalize.coma	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
ite_normalize.rs		ite_normalize.rs	Merge remote-tracking branch 'origin/master' into simplify_injections	Feb 25, 2025
knapsack.coma		knapsack.coma	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
knapsack.rs		knapsack.rs	Merge remote-tracking branch 'origin/master' into simplify_injections	Feb 25, 2025
knapsack_full.coma		knapsack_full.coma	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
knapsack_full.rs		knapsack_full.rs	Merge remote-tracking branch 'origin/master' into simplify_injections	Feb 25, 2025
linked_list.coma		linked_list.coma	Update tests	Mar 18, 2025
linked_list.rs		linked_list.rs	Fix the proof of linked_list	Mar 13, 2025
list_index_mut.coma		list_index_mut.coma	Update tests	Mar 18, 2025
list_index_mut.rs		list_index_mut.rs	Move creusot/tests to tests	Feb 21, 2025
list_reversal_lasso.coma		list_reversal_lasso.coma	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
list_reversal_lasso.rs		list_reversal_lasso.rs	Move creusot/tests to tests	Feb 21, 2025
loop.coma		loop.coma	In generated coma file, move all the use declaration to the begining …	Mar 7, 2025
loop.rs		loop.rs	Move creusot/tests to tests	Feb 21, 2025
mapping_indexing.coma		mapping_indexing.coma	In generated coma file, move all the use declaration to the begining …	Mar 7, 2025
mapping_indexing.rs		mapping_indexing.rs	Move creusot/tests to tests	Feb 21, 2025
mapping_test.coma		mapping_test.coma	Update tests	Mar 18, 2025
mapping_test.rs		mapping_test.rs	Move creusot/tests to tests	Feb 21, 2025
match_int.coma		match_int.coma	In generated coma file, move all the use declaration to the begining …	Mar 7, 2025
match_int.rs		match_int.rs	Move creusot/tests to tests	Feb 21, 2025
mc91.coma		mc91.coma	In generated coma file, move all the use declaration to the begining …	Mar 7, 2025
mc91.rs		mc91.rs	Merge remote-tracking branch 'origin/master' into simplify_injections	Feb 25, 2025
mutex.coma		mutex.coma	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
mutex.rs		mutex.rs	Merge remote-tracking branch 'origin/master' into simplify_injections	Feb 25, 2025
one_side_update.coma		one_side_update.coma	In generated coma file, move all the use declaration to the begining …	Mar 7, 2025
one_side_update.rs		one_side_update.rs	Move creusot/tests to tests	Feb 21, 2025
open_inv.coma		open_inv.coma	In generated coma file, move all the use declaration to the begining …	Mar 7, 2025
open_inv.rs		open_inv.rs	Move creusot/tests to tests	Feb 21, 2025
option.coma		option.coma	Use closure spec inference in the option test	Mar 18, 2025
option.rs		option.rs	Use closure spec inference in the option test	Mar 18, 2025
ord_trait.coma		ord_trait.coma	In generated coma file, move all the use declaration to the begining …	Mar 7, 2025
ord_trait.rs		ord_trait.rs	Move creusot/tests to tests	Feb 21, 2025
pcell.coma		pcell.coma	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
pcell.rs		pcell.rs	Move creusot/tests to tests	Feb 21, 2025
printing.coma		printing.coma	In generated coma file, move all the use declaration to the begining …	Mar 7, 2025
printing.rs		printing.rs	Remove warning about strings being experimental	Mar 3, 2025
projection_toggle.coma		projection_toggle.coma	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
projection_toggle.rs		projection_toggle.rs	Merge remote-tracking branch 'origin/master' into simplify_injections	Feb 25, 2025
projections.coma		projections.coma	In generated coma file, move all the use declaration to the begining …	Mar 7, 2025
projections.rs		projections.rs	Move creusot/tests to tests	Feb 21, 2025
prophecy.coma		prophecy.coma	In generated coma file, move all the use declaration to the begining …	Mar 7, 2025
prophecy.rs		prophecy.rs	Move creusot/tests to tests	Feb 21, 2025
purity.coma		purity.coma	In generated coma file, move all the use declaration to the begining …	Mar 7, 2025
purity.rs		purity.rs	Move creusot/tests to tests	Feb 21, 2025
red_black_tree.coma		red_black_tree.coma	Update tests	Mar 18, 2025
red_black_tree.rs		red_black_tree.rs	Merge remote-tracking branch 'origin/master' into simplify_injections	Feb 25, 2025
replace.coma		replace.coma	In generated coma file, move all the use declaration to the begining …	Mar 7, 2025
replace.rs		replace.rs	Move creusot/tests to tests	Feb 21, 2025
resolve_drop.coma		resolve_drop.coma	In generated coma file, move all the use declaration to the begining …	Mar 7, 2025
resolve_drop.rs		resolve_drop.rs	Move creusot/tests to tests	Feb 21, 2025
resolve_uninit.coma		resolve_uninit.coma	In generated coma file, move all the use declaration to the begining …	Mar 7, 2025
resolve_uninit.rs		resolve_uninit.rs	Move creusot/tests to tests	Feb 21, 2025
selection_sort_generic.coma		selection_sort_generic.coma	Update tests	Mar 18, 2025
selection_sort_generic.rs		selection_sort_generic.rs	Move creusot/tests to tests	Feb 21, 2025
simple_trigger.coma		simple_trigger.coma	In generated coma file, move all the use declaration to the begining …	Mar 7, 2025
simple_trigger.rs		simple_trigger.rs	Merge remote-tracking branch 'origin/master' into simplify_injections	Feb 25, 2025
sparse_array.coma		sparse_array.coma	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
sparse_array.rs		sparse_array.rs	Merge remote-tracking branch 'origin/master' into simplify_injections	Feb 25, 2025
spec_tests.coma		spec_tests.coma	In generated coma file, move all the use declaration to the begining …	Mar 7, 2025
spec_tests.rs		spec_tests.rs	Move creusot/tests to tests	Feb 21, 2025
split_borrow.coma		split_borrow.coma	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
split_borrow.rs		split_borrow.rs	Move creusot/tests to tests	Feb 21, 2025
std_types.coma		std_types.coma	In generated coma file, move all the use declaration to the begining …	Mar 7, 2025
std_types.rs		std_types.rs	Move creusot/tests to tests	Feb 21, 2025
such_that.coma		such_that.coma	In generated coma file, move all the use declaration to the begining …	Mar 7, 2025
such_that.rs		such_that.rs	Move creusot/tests to tests	Feb 21, 2025
sum.coma		sum.coma	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
sum.rs		sum.rs	Move creusot/tests to tests	Feb 21, 2025
sum_of_odds.coma		sum_of_odds.coma	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
sum_of_odds.rs		sum_of_odds.rs	Merge remote-tracking branch 'origin/master' into simplify_injections	Feb 25, 2025
swap_borrows.coma		swap_borrows.coma	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
swap_borrows.rs		swap_borrows.rs	Move creusot/tests to tests	Feb 21, 2025
switch.coma		switch.coma	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
switch.rs		switch.rs	Move creusot/tests to tests	Feb 21, 2025
switch_struct.coma		switch_struct.coma	In generated coma file, move all the use declaration to the begining …	Mar 7, 2025
switch_struct.rs		switch_struct.rs	Move creusot/tests to tests	Feb 21, 2025
take_first_mut.coma		take_first_mut.coma	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
take_first_mut.rs		take_first_mut.rs	Move creusot/tests to tests	Feb 21, 2025
trait.coma		trait.coma	In generated coma file, move all the use declaration to the begining …	Mar 7, 2025
trait.rs		trait.rs	Move creusot/tests to tests	Feb 21, 2025
trait_impl.coma		trait_impl.coma	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
trait_impl.rs		trait_impl.rs	Move creusot/tests to tests	Feb 21, 2025
trigger.coma		trigger.coma	In generated coma file, move all the use declaration to the begining …	Mar 7, 2025
trigger.rs		trigger.rs	Move creusot/tests to tests	Feb 21, 2025
trigger2.coma		trigger2.coma	In generated coma file, move all the use declaration to the begining …	Mar 7, 2025
trigger2.rs		trigger2.rs	Move creusot/tests to tests	Feb 21, 2025
two_modules.coma		two_modules.coma	In generated coma file, move all the use declaration to the begining …	Mar 7, 2025
two_modules.rs		two_modules.rs	Move creusot/tests to tests	Feb 21, 2025
type_constructors.coma		type_constructors.coma	In generated coma file, move all the use declaration to the begining …	Mar 7, 2025
type_constructors.rs		type_constructors.rs	Move creusot/tests to tests	Feb 21, 2025
union_find.coma		union_find.coma	Update tests	Mar 20, 2025
union_find.rs		union_find.rs	Remove the trusted function in union_find	Mar 20, 2025
unnest.coma		unnest.coma	In generated coma file, move all the use declaration to the begining …	Mar 7, 2025
unnest.rs		unnest.rs	Move creusot/tests to tests	Feb 21, 2025
unused_in_loop.coma		unused_in_loop.coma	In generated coma file, move all the use declaration to the begining …	Mar 7, 2025
unused_in_loop.rs		unused_in_loop.rs	Move creusot/tests to tests	Feb 21, 2025
vecdeque.coma		vecdeque.coma	Translate tuples into records, insert type invariant specs in the rig…	Mar 17, 2025
vecdeque.rs		vecdeque.rs	Move creusot/tests to tests	Feb 21, 2025
View all files