Skip to content

Issues: verifast/verifast

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Clear current search query, filters, and sorts
86 Open 162 Closed
86 Open 162 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Arrays in structures: "Parse error: Array cannot be of this type."
#39 by necto was closed Aug 8, 2016
Typo in lemma take_one_plus?
#6 by georgwaechter was closed Feb 18, 2014
2
How about mailing list for VeriFast community?
#8 by master-q was closed Jan 28, 2016
1
unsigned number overflow not detected
#15 by DrSkunk was closed Oct 21, 2016
1
(a%b) == a Parser error.
#16 by necto was closed Sep 14, 2017
2
Redux forgets facts involving nonlinear multiplication
#17 by necto was closed Sep 7, 2018
2
internal error: Invalid_argument("List.for_all2") when dealing with a generic function predicate in a loop invariant.
#18 by necto was closed Apr 13, 2016
typedef int my_int; + (my_int*)x; - Parser error.
#21 by necto was closed Sep 2, 2016
1
File "verifast1.ml", line 301, characters 23-29: Assertion failed
#24 by jameshfisher was closed Aug 23, 2018
2
malloc argument should not be of type int
#27 by jameshfisher was closed Nov 26, 2018
1
Structure field offset comparison does not work when invoked from a separate header.
#30 by necto was closed May 2, 2016
"struct_field" predicate can not be opened for short/unsigned short fields.
#31 by necto was closed Sep 2, 2016
3
Clarify support for termination
#2 by georgwaechter was closed Jan 20, 2014
2
Deduction for nonlinear arithmetic is highly incomplete and brittle
#37 by necto was closed Mar 30, 2017
3
[feature request] Dereferencing pointers of type uint16 is not yet supported.
#42 by necto was closed Sep 2, 2016
3
Z3 support?
#48 by necto was closed Jan 7, 2018
2
SMT solver incompleteness due to trigger premise checking
#49 by necto was closed Oct 12, 2016
1
VeriFast 'hangs' or crashes due to chars_split/chars_join autolemma loop
#50 by btj was closed Jan 23, 2018
2
How to prove 0 < x => 0/x == 0 ?
#51 by necto was closed Oct 18, 2016
2
VeriFast "forgets" loop invariant on loop exit.
#52 by necto was closed Oct 19, 2016
7
Speed up the crypto test cases
#56 by btj was closed Nov 19, 2018
3
Improve typechecking of shift operators
#59 by Bromind was closed Nov 14, 2016
1
Cast int64 to int32
#61 by Bromind was closed Nov 18, 2016
Commit #d5ee55 breaks tests
#65 by Bromind was closed Nov 23, 2016
2
Incompleteness in truncation arithmetic. (Potential soundness issue?)
#524 by isubasinghe was closed Jun 5, 2024
2
ProTip! Adding no:label will show everything without a label.