Issues · pub / frama-c · GitLab

Model Variables in Frama C

#249 · created Aug 27, 2018 by mantis-gitlab-migration ACSL enhancement kernel
- 1
updated Feb 22, 2021
Expose ACSL annotations through host language pragmas

#264 · created Mar 08, 2018 by mantis-gitlab-migration ACSL enhancement kernel
- 0
updated Apr 14, 2021
label Pre in function contracts

#386 · created Jan 02, 2017 by Jens Gerlach ACSL bug kernel
- 0
updated Feb 22, 2021
structure in logic not supported?

#383 · created Dec 20, 2016 by Jens Gerlach ACSL bug kernel
- 1
updated Feb 22, 2021
No syntax to apply lambda expressions

#576 · created Dec 05, 2015 by David Cok ACSL enhancement kernel
- 0
updated Feb 22, 2021
ambiguity with consecutive comparison and ternary expressions

#575 · created Dec 05, 2015 by David Cok ACSL bug kernel
- 1
updated Feb 22, 2021
ACSL typing fails when performing unification of type variables

#590 · created Sep 24, 2015 by Patrick Baudin ACSL bug kernel
- 0
updated Mar 29, 2021
implicit conversion of terms to predicates

#611 · created Jul 17, 2015 by David Cok ACSL bug kernel
- 0
updated Feb 22, 2021
Weak and Strong Invariants are not supported

#630 · created Jun 12, 2015 by mantis-gitlab-migration ACSL bug kernel
- 0
updated Feb 22, 2021
Redefintion of variables in same scope is allowed in annotations

#634 · created Jun 01, 2015 by mantis-gitlab-migration ACSL bug confirmed kernel
- 1
updated Feb 22, 2021
bitwise negation of uint introduces "-1" in Alt-Ergo obligation

#865 · created Dec 08, 2014 by Jochen Burghardt ACSL confirmed
- 3
updated Feb 22, 2021
provide option to activate a plugin in command-line help

#829 · created Jun 02, 2014 by Jochen Burghardt ACSL
- 1
updated Feb 22, 2021
Check that all occurrences of *p in assigns are guarded by a \valid(p) in requires

#357 · created Apr 23, 2014 by Jens Gerlach ACSL bug kernel
- 1
updated Feb 22, 2021
Translation of abrupt clause into assert do not take 'for :' clause into account

#955 · created Jan 27, 2014 by Virgile Prevosto ACSL bug kernel
- 0
updated Feb 22, 2021
r24600: confusing error message when t[] is used where t* is expected

#1828 · created Dec 03, 2013 by Pascal Cuoq ACSL enhancement kernel
- 0
updated Feb 22, 2021
crash

#1817 · created Oct 01, 2013 by mantis-gitlab-migration ACSL bug kernel
- 1
updated Feb 22, 2021
Code annotation in the middle of labels

#1926 · created Dec 12, 2012 by Julien Signoles ACSL bug kernel
- 1
updated Mar 29, 2021
wrong proof obligation generated for loop initialization [under why-2.30]

#2097 · created Nov 03, 2011 by Jochen Burghardt ACSL bug kernel
- 4
updated Feb 22, 2021
Functional expression in assigns properties

#2171 · created Oct 06, 2011 by mantis-gitlab-migration ACSL enhancement kernel
- 0
updated Feb 22, 2021
unbound function \length in annotation

#2073 · created Sep 19, 2011 by Mihaela Sighireanu ACSL bug kernel
- 2
updated Feb 22, 2021