| | |  | 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 | 1 | |
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 | 3 | |
Kernel > ACSL implementation | feature | acknowledged (virgile) | 2014-02-12 | Several [invariant] at a program point |
| | | | 0001281 | 1 | |
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 | 3 | 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 |
| | | | 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 | 4 | 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 |
| | | | 0001288 | | 2 |
Plug-in > aoraï | trivial | acknowledged (virgile) | 2012-10-26 | .ya filename missing in error report |
| | | | 0001280 | | |
Plug-in > wp | minor | assigned (correnson) | 2012-10-13 | Printing of function types causes a stack overflow |
| | | | 0001279 | | 1 |
Plug-in > wp | crash | assigned (correnson) | 2012-10-13 | Multiple branches to a label/loop entries crashes wp |
| | | | 0000379 | 2 | 1 |
Plug-in > jessie | crash | assigned (cmarche) | 2012-09-21 | \separated |
| | | | 0001186 | 4 | 1 |
Plug-in > wp | minor | assigned (correnson) | 2012-06-15 | ltl does not accept state charts with transitions invoking dynamic function pointers |
| | | | 0000658 | 1 | 1 |
Plug-in > jessie | feature | assigned (cmarche) | 2012-06-10 | loop assigns crash |
| | | | 0000653 | 1 | 1 |
Plug-in > jessie | minor | assigned (cmarche) | 2012-06-10 | jessie's Unexpected failure |
| | | | 0001010 | | |
Plug-in > wp | feature | assigned (correnson) | 2012-06-09 | warn on stderr about current restrictions, and list them in WP manual |
| | | | 0001190 | 1 | |
Kernel | minor | assigned (virgile) | 2012-06-09 | __builtin_alloca |
| | | | 0001161 | 1 | 1 |
Plug-in > jessie | feature | assigned (cmarche) | 2012-04-17 | error in wp_behav.c |
| | | | 0001154 | 4 | 1 |
Plug-in > jessie | minor | assigned (cmarche) | 2012-04-17 | erroneous left value (structure field) |
| | | | 0001093 | | 1 |
Plug-in > jessie | crash | assigned (cmarche) | 2012-02-14 | Passing multi-dimensional arrays via reference fails |
| | | | 0000967 | | |
Kernel > ACSL implementation | minor | assigned (virgile) | 2012-02-09 | unbound function \length in annotation |
| | | | 0000252 | | |
Plug-in > jessie | feature | assigned (virgile) | 2012-01-21 | type invariants |
