creusot-rs/creusot

Issues

• Variant checking unsoundly assumes precondition

  #1204 opened 3 days ago by jhjourdan
  5

• Wrong spans for loop invariants

  #1225 opened 14 days ago by Armael
  2

• ghost!{e} requires e to be Sized

  #1219 opened 17 days ago by Armael
  4

• `cargo creusot` rebuilds too much if any `RUSTFLAGS` argument changes

  #1218 opened 18 days ago by Lysxia
  1

• Support for some operations on raw pointers

  #1217 opened 18 days ago by Armael
  0

• "Closure" error in pearlite

  #1215 opened 21 days ago by Armael
  6

• Feature request: a `cargo creusot check` command that does not output .coma files (for IDE support)

  #1207 opened 22 days ago by Armael
  0

• Support for real (and rational?) numbers in pearlite

  #1210 opened 23 days ago by Armael
  0

• Invalid coma output ("unbound function or predicate symbol (+)")

  #1208 opened 24 days ago by Armael
  0

• Generate Coma in a directory outside of `target/`

  #1199 opened a month ago by Lysxia
  1

• Tracking issue: trusted functions in `creusot-contracts`

  #1192 opened a month ago by arnaudgolfouse
  0

• VCs for libraries are dropped if a binary is present

  #1178 opened a month ago by Armael
  9

• Extern specs for `println!` and others

  #1179 opened a month ago by Armael
  6

• "Trigger must be tuples" error with single trigger expression

  #1180 opened a month ago by Armael
  7

• Mechanism to associate "laws" to a type/identifier/etc

  #1182 opened a month ago by Armael
  0

• incorrect spec for `String::len`?

  #1164 opened a month ago by arnaudgolfouse
  4

• Unsupported pattern kind AscribeUserType

  #1171 opened a month ago by Armael
  1

• stop generating empty spans in .coma

  #1157 opened a month ago by Armael
  2

• testsuite: test runner to check that tests can be compiled normally

  #1160 opened a month ago by Armael
  0

• Simplifying 06_knights_tour

  #1148 opened a month ago by Lysxia
  4

• Lost information in loops with iterators

  #1149 opened a month ago by Lysxia
  2

• Self referential types and non-strictly-positive occurrences

  #1146 opened a month ago by nishanthkarthik
  8

• `rust-toolchain` is a symlink; bad for windows

  #1093 opened a month ago by Lysxia
  2

• Add provenance information for impl hashes

  #1137 opened 2 months ago by Lysxia
  3

• Integer literals in pearlite should be allowed to be of type i32/i16/...

  #1125 opened 2 months ago by jhjourdan
  2

• Better detection of available libraries

  #1138 opened 2 months ago by Lysxia
  4

• Identifer names are unstable

  #1134 opened 2 months ago by xldenis
  6

• Implement casts in pearlite

  #1124 opened 2 months ago by jhjourdan
  0

• Static analysis for type invariants

  #1122 opened 2 months ago by jhjourdan
  0

• SMT solvers have a hard time unfolding type invariants

  #1121 opened 2 months ago by jhjourdan
  0

• Pattern in closure argument sometimes generate incorrect coma code

  #1118 opened 2 months ago by arnaudgolfouse
  1

• Clarify the question of normalization of types

  #1116 opened 2 months ago by jhjourdan
  0

• snake_case to CamelCase conversion is not injective

  #1107 opened 2 months ago by Lysxia
  11

• Capturing a variable in a closure introduces a non-local variable in `DebugVarInfo`

  #1072 opened 2 months ago by arnaudgolfouse
  1

• Publish a crate of verified datastructures

  #1105 opened 2 months ago by Armael
  0

• cargo creusot doc: attach extern specs to functions

  #1104 opened 2 months ago by Armael
  0

• Case study: a map datastructure with an Entry-style API

  #1103 opened 2 months ago by Armael
  0

• Html documentation pages for creusot_contracts

  #1102 opened 2 months ago by Armael
  0

• Specifications for HashMap in creusot_contracts

  #1101 opened 2 months ago by Armael
  0

• `should_fail` tests are not checked for failing

  #1090 opened 2 months ago by jhjourdan
  3

• Support inherent laws

  #1091 opened 2 months ago by xldenis
  0

• refactoring: have the `cargo creusot why3 {replay,prove}` subcommands be handled by `cargo-creusot`

  #1016 opened 6 months ago by Armael
  3

• Binary distribution

  #1017 opened 6 months ago by Armael
  1

• Modular verification

  #1067 opened 3 months ago by mojeanmac
  6

• derive Clone emits invalid coma

  #1074 opened 3 months ago by nishanthkarthik
  2

• `impl Trait` generates incorrect coma code

  #1041 opened 4 months ago by arnaudgolfouse
  3

• Logic associated function without parameters causes why3 type error in output mlcfg

  #1030 opened 4 months ago by dewert99
  0

• language file 'Coma' not found, when launching why3 ide

  #1018 opened 4 months ago by Armael
  4

• trouble proving derive PartialEq with v0.1

  #1023 opened 4 months ago by Emilie-Thome
  9

• guide: the `head` example does not work with creusot 0.1

  #1020 opened 4 months ago by Armael
  1