creusot-rs creusot issues

creusot-rs / creusot

Creusot helps you prove your code is correct in an automated fashion.

GNU Lesser General Public License v2.1

1.12k stars 50 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Add provenance information for impl hashes

#1137 Lysxia opened 8 minutes ago
0
Specify most of `Option`'s methods

#1136 arnaudgolfouse opened 1 hour ago
2
More stable hash

#1135 Lysxia closed 14 hours ago
12
Identifer names are unstable

#1134 xldenis closed 14 hours ago
6
Structural resolve

#1133 xldenis closed 1 day ago
1
Simple proof of Filter

#1132 xldenis opened 2 days ago
1
creusot-contracts/num.rs: fix Default instance for isize

#1131 Armael closed 3 days ago
0
Xavier's nitpicks for #1129

#1130 jhjourdan closed 3 days ago
0
Remove the default implementation of the Resolve trait.

#1129 jhjourdan closed 3 days ago
0
Condense let-spans

#1128 Lysxia closed 2 days ago
0
Fix typo in why3/README

#1127 Lysxia closed 3 days ago
0
Bump why3 dependency

#1126 jhjourdan closed 3 days ago
1
Integer literals in pearlite should be allowed to be of type i32/i16/...

#1125 jhjourdan opened 4 days ago
0
Implement casts in pearlite

#1124 jhjourdan opened 4 days ago
0
Use more stable naming of impls

#1123 Lysxia closed 3 days ago
7
Static analysis for type invariants

#1122 jhjourdan opened 4 days ago
0
SMT solvers have a hard time unfolding type invariants

#1121 jhjourdan opened 4 days ago
0
Rework the final borrow analysis

#1120 arnaudgolfouse closed 2 days ago
2
Type invariants: type parameters and aliases are not trivial

#1119 jhjourdan closed 4 days ago
4
Pattern in closure argument sometimes generate incorrect coma code

#1118 arnaudgolfouse opened 6 days ago
1
Fix inferred invariants

#1117 jhjourdan closed 6 days ago
2
Clarify the question of normalization of types

#1116 jhjourdan opened 6 days ago
0
Try Bitwise

#1115 laurentder opened 6 days ago
0
Basic Type Privacy

#1114 xldenis closed 1 week ago
2
Allow creusot-contracts to build locally

#1113 xldenis closed 1 week ago
0
Stabilize list_reversal_lasso.

#1112 jhjourdan closed 1 week ago
4
Fix typo in error message: 'Could _not_ determine value of constant'

#1111 Lysxia closed 1 week ago
1
Make sure that all tests that can be replayed are replayed

#1110 jhjourdan closed 1 week ago
0
[WIP] Type invariant fixes

#1109 jhjourdan closed 6 days ago
1
Make translation of names injective

#1108 Lysxia closed 1 week ago
9
snake_case to CamelCase conversion is not injective

#1107 Lysxia closed 1 week ago
11
Allow usage of `proof_assert` in closures

#1106 arnaudgolfouse closed 1 week ago
7
Publish a crate of verified datastructures

#1105 Armael opened 1 week ago
0
cargo creusot doc: attach extern specs to functions

#1104 Armael opened 1 week ago
0
Case study: a map datastructure with an Entry-style API

#1103 Armael opened 1 week ago
0
Html documentation pages for creusot_contracts

#1102 Armael opened 1 week ago
0
Specifications for HashMap in creusot_contracts

#1101 Armael opened 1 week ago
0
Add a test to `should_fail/final_borrows`, and fix existing tests

#1100 arnaudgolfouse closed 1 week ago
0
Clarify Puritty::can_call, make it more robust wrt. future changes.

#1099 jhjourdan closed 1 week ago
0
Type invariants cleanup

#1098 jhjourdan closed 1 week ago
0
Fix typo invarianrs -> invariants.

#1097 jhjourdan closed 1 week ago
0
Disable automatic insertion of type invariant assertions in relevant places.

#1096 jhjourdan closed 1 week ago
1
Various fixes (more or less) related to type invariants

#1095 jhjourdan closed 2 weeks ago
4
abort and unreachable and not diagnostic items anymore

#1094 jhjourdan closed 2 weeks ago
0
`rust-toolchain` is a symlink; bad for windows

#1093 Lysxia opened 2 weeks ago
2
Fix replay of should_fail tests.

#1092 jhjourdan closed 2 weeks ago
0
Support inherent laws

#1091 xldenis opened 2 weeks ago
0
`should_fail` tests are not checked for failing

#1090 jhjourdan closed 2 weeks ago
3
Final borrows fixes

#1089 jhjourdan closed 2 weeks ago
1
Fix `#[derive(DeepModel)]` (for real this time)

#1088 arnaudgolfouse closed 3 weeks ago
0