|
Viewing Issues (151 - 200 / 283)
[ Print Reports ] [ CSV Export ] [ Excel Export ]
[ First Prev 1 2 3 4 5 6 Next Last ]
|
| | | P | ID | # |  |
Category | Severity | Status | Updated | Summary |
|
| | |  | 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 |
| | | | 0001806 | | |
Plug-in > wp | minor | assigned (correnson) | 2014-06-13 | Error in coq code generated by wp |
| | | | 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 |
| | | | 0001576 | | 1 |
Kernel | feature | assigned (virgile) | 2013-11-28 | declaration of variable of type void accepted |
| | | | 0001450 | 1 | |
Kernel | minor | confirmed (signoles) | 2013-09-26 | journalization of -print option |
| | | | 0001471 | 6 | 1 |
Kernel | minor | acknowledged (signoles) | 2013-09-26 | r23410: unsound reporting of pre-condition status |
| | | | 0001430 | 3 | |
Plug-in > report | minor | assigned (correnson) | 2013-05-31 | RTE are not in 'report' |
| | | | 0001428 | 1 | |
Plug-in > wp | minor | assigned (correnson) | 2013-05-24 | Range verification in 2D-array fails |
| | | | 0001418 | | |
Kernel > configure | major | assigned (virgile) | 2013-05-09 | Fatal error: exception Env.Error("C:\Frama-C\lib/pervasives.cmi") |
| | | | 0001417 | | |
Plug-in > jessie | minor | assigned (cmarche) | 2013-05-08 | Config file 'C:\cygwin\home\xiewenlong\.gwhyrc' does not exists, |
| | | | 0001389 | | |
Plug-in > wp | feature | assigned (correnson) | 2013-04-16 | Translation of tsets |
| | | | 0000765 | 5 | 1 |
Plug-in > wp | minor | assigned (correnson) | 2013-03-09 | Post-state of statement spec |
| | | | 0000852 | 4 | 1 |
Kernel | minor | assigned (virgile) | 2013-01-25 | non-constant size of 2-dim array causes error in recursive procedure |
| | | | 0001332 | | |
Plug-in > wp | crash | assigned (correnson) | 2012-12-15 | [wp] failure: not an integer (Blob) |
| | | | 0001327 | | |
Kernel | minor | assigned (virgile) | 2012-12-12 | Code annotation in the middle of labels |
| | | | 0001291 | | |
Kernel > ACSL implementation | minor | acknowledged (virgile) | 2012-10-31 | Typing rejects polymorphic logic constants |
|
[ First Prev 1 2 3 4 5 6 Next Last ]
|
