|
Viewing Issues (151 - 200 / 296)
[ Print Reports ] [ CSV Export ] [ Excel Export ]
[ First Prev 1 2 3 4 5 6 Next Last ]
|
| | | P | ID | # |  |
Category | Severity | Status | Updated | Summary |
|
| | |  | 0001718 | | |
Kernel | feature | assigned (virgile) | 2015-11-04 | Nested VLA are not supported |
| | | | 0002182 | | 1 |
Plug-in > wp | crash | assigned (correnson) | 2015-10-27 | Plug-in wp aborted: internal error, Raised at file "src/wp/register.ml", line 579 |
| | | | 0002179 | 1 | 1 |
Plug-in > wp | minor | assigned (correnson) | 2015-10-18 | Unable to prove things that are provable, gets confused |
| | | | 0002170 | | |
Kernel > ACSL implementation | minor | assigned (virgile) | 2015-09-24 | ACSL typing fails when performing unification of type variables |
| | | | 0002169 | | 1 |
Plug-in > wp | minor | assigned (correnson) | 2015-09-21 | incomplete Alt-Ergo obligation files generated in presence of lemma "forall int x; ..." with "x" not occurring in "..." |
| | | | 0002168 | | 1 |
Plug-in > wp | feature | assigned (correnson) | 2015-09-21 | suggest command-line option to avoid sophisticated expression transformations, in particular for Coq obligations |
| | | | 0002160 | 1 | |
Plug-in > wp | minor | acknowledged (correnson) | 2015-09-15 | assertion failure using memset on a char |
| | | | 0002156 | 1 | 1 |
Plug-in > wp | minor | assigned (correnson) | 2015-09-07 | Slow in proof obligation generation |
| | | | 0002153 | 4 | 3 |
Plug-in > wp | minor | acknowledged (correnson) | 2015-09-03 | bound variable names in Coq file depend on unrelated function later in C source code |
| | | | 0002152 | | |
Kernel | minor | assigned (virgile) | 2015-08-21 | With struct containing arrays, option -unspecified-access is too strict |
| | | | 0001992 | 1 | 1 |
Plug-in > pdg | minor | assigned (maroneze) | 2015-08-03 | Control dependencies between labelled instructuctions and the corresponding goto statement |
| | | | 0002148 | | |
Kernel > ACSL implementation | major | assigned (virgile) | 2015-07-17 | implicit conversion of terms to predicates |
| | | | 0002145 | 3 | 3 |
Plug-in > wp | minor | assigned (correnson) | 2015-07-17 | Error when struct has no members |
| | | | 0002147 | | |
Kernel > ACSL implementation | minor | assigned (virgile) | 2015-07-16 | Frama-C problem with macro substitution in annotations |
| | | | 0002041 | 1 | |
Plug-in > wp | minor | acknowledged (correnson) | 2015-06-29 | unable to use lemma separated_region |
| | | | 0002123 | 2 | 3 |
Plug-in > wp | minor | acknowledged (correnson) | 2015-06-29 | validity of obligation from statement contract depends on whether the statement is enclosed in block {} |
| | | | 0002134 | | |
Kernel > ACSL implementation | minor | assigned (virgile) | 2015-06-12 | Weak and Strong Invariants are not supported |
| | | | 0002125 | 1 | |
Kernel > ACSL implementation | minor | confirmed (virgile) | 2015-06-02 | Redefintion of variables in same scope is allowed in annotations |
| | | | 0002087 | 1 | 2 |
Plug-in > wp | minor | acknowledged (correnson) | 2015-03-09 | Able to assert a false statement |
| | | | 0002054 | | |
ptests | minor | assigned (virgile) | 2015-01-22 | ptest doesn't abort tests for which the command is incorrect |
| | | | 0002039 | | 1 |
Plug-in > wp | crash | assigned (correnson) | 2014-12-22 | WP-Plugin crashes due to an internal error when terms of sets during union have different types |
| | |  | 0002011 | | |
Plug-in > wp | major | assigned (correnson) | 2014-12-02 | Unsoundness bug using native alt-ergo and Why3 due to reordering of lemmas |
| | |  | 0001632 | | |
Kernel > ACSL implementation | minor | assigned (virgile) | 2014-10-29 | Translation of abrupt clause into assert do not take 'for :' clause into account |
| | | | 0001943 | | 1 |
Plug-in > jessie | major | assigned (cmarche) | 2014-10-29 | Jessie crashes with "Assertion failed" |
| | | | 0001936 | | 1 |
Plug-in > wp | crash | assigned (correnson) | 2014-10-14 | WP crashes on \floor builtin |
| | | | 0001913 | 1 | 2 |
Plug-in > jessie | crash | assigned (cmarche) | 2014-08-26 | Jessie crashes on incorrectly declared malloc |
| | | | 0001847 | | |
Plug-in > wp | minor | assigned (correnson) | 2014-07-21 | Problem with _Bool(when casting to int or with ?:) |
| | | | 0001844 | | 1 |
Plug-in > wp | crash | assigned (correnson) | 2014-07-17 | assigns crash on incorrect locations |
| | |  | 0001638 | 4 | 2 |
Plug-in > wp | major | acknowledged (correnson) | 2014-07-17 | assigns clause appears unprovable |
| | | | 0001103 | 2 | |
Kernel | feature | assigned (virgile) | 2014-07-11 | Default @requires property for the [main] function |
| | | | 0001461 | 3 | |
Plug-in > wp | minor | acknowledged (correnson) | 2014-06-17 | assigns, loop assigns and loop invariant |
| | | | 0001812 | 1 | 2 |
Plug-in > wp | minor | acknowledged (correnson) | 2014-06-17 | Assigns not respected in behaviors when using pointers to pointers |
| | | | 0001804 | | |
Plug-in > wp | crash | assigned (correnson) | 2014-06-06 | WP crash when type casting in lemma |
| | | | 0001801 | | |
Plug-in > wp | major | assigned (correnson) | 2014-06-06 | WP doesn't warn about volatile variables |
| | | | 0001800 | | |
Kernel | minor | assigned (virgile) | 2014-06-06 | Cannot use quotes in comments in annotations |
| | | | 0001537 | 7 | |
Plug-in > wp | feature | acknowledged (correnson) | 2014-06-02 | Frama-C should warn about inconsistent specification of declared functions |
| | | | 0001645 | | |
Kernel | minor | assigned (virgile) | 2014-03-24 | Initializer of static variable refers to size of type of local variable |
| | | | 0001712 | | |
Kernel | minor | assigned (virgile) | 2014-03-24 | Statically reject programs that jump over VLA declaration. |
| | | | 0001454 | 2 | |
Kernel > configure | minor | assigned (virgile) | 2014-03-14 | Configure script's autolocation of local OcamlGraph breaks out of tree builds |
| | | | 0001699 | | |
Plug-in > wp | feature | assigned (correnson) | 2014-03-14 | Develop strategies to efficiently run WP with different ATP and Coq |
| | | | 0001693 | | |
Plug-in > wp | feature | assigned (correnson) | 2014-03-14 | Generate footprint from reads clauses of logic declarations |
| | | | 0001694 | | |
Plug-in > wp | feature | assigned (correnson) | 2014-03-13 | Generate proof obligation for drivers when driver instantiate a logic acsl declaration |
| | | | 0001687 | | |
Plug-in > wp | major | assigned (correnson) | 2014-03-12 | Frama-C GUI discards candidate coq proof |
| | | | 0000750 | 4 | |
Kernel > ACSL implementation | feature | acknowledged (virgile) | 2014-02-12 | Several [invariant] at a program point |
| | | | 0001281 | 2 | |
Plug-in > wp | minor | acknowledged (correnson) | 2014-02-05 | do { ... } while (0) pattern causes wp to fail |
| | | | 0001495 | 1 | |
Kernel > ACSL implementation | minor | assigned (virgile) | 2014-02-05 | crash |
| | | | 0001556 | 4 | 1 |
Plug-in > wp | minor | acknowledged (correnson) | 2014-02-05 | unprovable PO in function manipulating structs - issue with Qed's simplifications |
| | | | 0001621 | 2 | |
Plug-in > wp | minor | acknowledged (correnson) | 2014-01-24 | loop invariant as hypothesis |
| | | | 0001577 | | 1 |
Kernel | feature | assigned (virgile) | 2013-12-17 | suggest to insert implicit cast of logic function's expression to return type |
| | | | 0001582 | | |
Kernel > ACSL implementation | tweak | assigned (virgile) | 2013-12-03 | r24600: confusing error message when t[] is used where t* is expected |
|
[ First Prev 1 2 3 4 5 6 Next Last ]
|
