|
Viewing Issues (51 - 100 / 294)
[ Print Reports ] [ CSV Export ] [ Excel Export ]
[ First Prev 1 2 3 4 5 6 Next Last ]
|
| | | P | ID | # |  |
Category | Severity | Status | Updated | Summary |
|
| | | | 0002371 | 1 | 1 |
Plug-in > wp | feature | assigned (correnson) | 2018-03-26 | suggest to provide results of commandl-line "-wp-prop" evaluation in a file in the wp-out directory |
| | |  | 0002370 | | |
Kernel > ACSL implementation | feature | assigned (virgile) | 2018-03-08 | Expose ACSL annotations through host language pragmas |
| | | | 0002369 | 8 | |
Plug-in > E-ACSL | minor | acknowledged (signoles) | 2018-02-23 | e-acsl-gcc failes on macOS |
| | | | 0002367 | 1 | 1 |
Plug-in > clang | minor | assigned (virgile) | 2018-02-12 | C-function returning a struct causes warning on missing Ctor code/spec when inside 'extern "C" {...}' |
| | | | 0002366 | | 1 |
Plug-in > clang | minor | assigned (virgile) | 2018-02-12 | loop assigns clause ginored under strange circumstances |
| | | | 0002365 | | 1 |
Plug-in > clang | minor | assigned (virgile) | 2018-02-12 | user-defined type not accepted after builtin type in quantifier chain |
| | | | 0002364 | | 1 |
Plug-in > clang | feature | assigned (virgile) | 2018-02-12 | Frama-clang reports overloading ambiguity where Frama-C doesn't |
| | | | 0002363 | | 1 |
Plug-in > clang | minor | assigned (virgile) | 2018-02-12 | variable declared in "for" init-part unrecognized in loop body assigns clause; 100% verification degree reported nevertheless |
| | | | 0002362 | | 1 |
Plug-in > clang | minor | assigned (virgile) | 2018-02-12 | "let" in predicate body unrecognized |
| | | | 0002361 | | 1 |
Plug-in > clang | crash | assigned (virgile) | 2018-02-12 | "assigns" in statement contract causes abort or crash |
| | | | 0002360 | | 1 |
Plug-in > clang | crash | assigned (virgile) | 2018-02-12 | "Here" as predicate label in statement contract causes Segmentation fault |
| | | | 0002359 | | 1 |
Plug-in > clang | feature | assigned (virgile) | 2018-02-12 | Frama-clang complains when reserved keywords are used as property labels, while Frama-C doesn't |
| | | | 0002356 | 2 | 1 |
Plug-in > clang | feature | confirmed (virgile) | 2018-02-09 | insufficient contracts for generated constructors and assignment operator(s) |
| | | | 0002357 | 2 | 1 |
Plug-in > clang | minor | assigned (virgile) | 2018-02-08 | can't handle lemma with 3 labels |
| | | | 0002358 | | 1 |
Plug-in > clang | feature | assigned (virgile) | 2018-02-08 | predicate argument type "struct S" accepted by Frama-C, but not by Frama-clang |
| | | | 0002350 | 2 | 2 |
Plug-in > clang | minor | acknowledged (virgile) | 2018-02-08 | kernel warns about invalid implicit conversion |
| | | | 0002355 | 1 | 1 |
Plug-in > clang | minor | assigned (virgile) | 2018-02-05 | Alt-Ergo reports about " bool and int cannot be unified" |
| | | | 0001484 | 1 | 1 |
Plug-in > wp | minor | assigned (correnson) | 2018-02-05 | ill-typed alt-ergo proof obligation |
| | | | 0002340 | 4 | 3 |
Plug-in > wp | minor | acknowledged (correnson) | 2018-02-02 | Coq translation of predicate name changes when additional files are processed by Frama-C |
| | | | 0002353 | 1 | 5 |
Plug-in > wp | minor | assigned (correnson) | 2018-02-01 | alt-ergo goals generated directly / via why3 differ in provability |
| | | | 0002352 | | 1 |
Plug-in > clang | crash | assigned (virgile) | 2018-01-31 | Frama-Clang crashes on error in contract |
| | | | 0002351 | 1 | 1 |
Plug-in > clang | minor | assigned (virgile) | 2018-01-31 | no diagnostics on wrong keyword |
| | | | 0002349 | 1 | 2 |
Plug-in > clang | feature | confirmed (virgile) | 2018-01-31 | warning from kernel about exceptions |
| | | | 0002348 | 1 | 2 |
Plug-in > clang | minor | assigned (virgile) | 2018-01-30 | unknown variable in contract is not treated as an error |
| | | | 0002347 | 1 | 3 |
Plug-in > clang | crash | assigned (virgile) | 2018-01-23 | direct initialisation of bool by nullptr |
| | | | 0002346 | | 2 |
Plug-in > clang | minor | assigned (virgile) | 2018-01-19 | C++11 delegating constructor not supported |
| | | | 0002345 | | 1 |
Plug-in > clang | minor | assigned (virgile) | 2018-01-19 | range based for loop from C++11 not supported |
| | | | 0002342 | 2 | 1 |
Plug-in > clang | minor | confirmed (virgile) | 2018-01-18 | std::bad_alloc not supported |
| | | | 0001431 | 2 | |
Graphical User Interface | feature | confirmed (maroneze) | 2018-01-12 | How to use the "Callers ..." context menu item |
| | | | 0002337 | 1 | |
Documentation | text | assigned (correnson) | 2017-12-29 | explain wp's syntactic restrictions on "inductive" definitions |
| | |  | 0000945 | 4 | |
Plug-in > Eva | minor | assigned (maroneze) | 2017-12-17 | Should warn for overlapping lv=lv; assignments |
| | | | 0002254 | 1 | 1 |
Plug-in > Eva | minor | assigned (maroneze) | 2017-12-17 | Option "-lib-entry" results misses possible values of function pointers |
| | | | 0002256 | 4 | 1 |
Plug-in > Eva | minor | assigned (maroneze) | 2017-12-17 | "pointer comparison" warning emitted for "p==NULL" |
| | | | 0002180 | 1 | |
Plug-in > wp | crash | assigned (correnson) | 2017-12-17 | Crash on loop with global assigns and per-behavior assigns |
| | | | 0002166 | 8 | |
Plug-in > Eva | minor | assigned (buhler) | 2017-12-17 | Substraction results in unknown values |
| | | | 0002306 | 2 | 1 |
Kernel | minor | assigned (maroneze) | 2017-12-17 | Support for flexible array members |
| | | | 0002336 | 1 | 1 |
Plug-in > wp | tweak | assigned (correnson) | 2017-12-08 | suggest to supply previous "ensures" as hypotheses in proof obligation of next "ensures" |
| | | | 0002276 | 3 | |
Graphical User Interface | tweak | acknowledged (maroneze) | 2017-11-27 | Duplicates are created on the tab "Messages" |
| | | | 0002332 | 3 | 2 |
Plug-in > wp | major | acknowledged (correnson) | 2017-11-22 | Information on C type of array is not present (in Coq) |
| | | | 0002330 | | 1 |
Plug-in > wp | minor | assigned (correnson) | 2017-10-26 | known, but inferrable, yet not inferred, property not given as precodition to provers |
| | | | 0002329 | 1 | 2 |
Plug-in > wp | tweak | assigned (correnson) | 2017-10-12 | suggest unique term normalization for lemmas and goals |
| | | | 0002285 | 1 | 2 |
Plug-in > wp | feature | assigned (correnson) | 2017-10-09 | suggest boolean expressions for "-wp-prop" arguments |
| | | | 0002100 | 5 | 1 |
Plug-in > wp | minor | acknowledged (correnson) | 2017-10-09 | readability of coq(?) names |
| | | | 0002301 | 2 | 1 |
Plug-in > wp | crash | assigned (correnson) | 2017-07-21 | statement contract apparently confuses parser |
| | | | 0002317 | | |
Documentation > manuals | text | assigned (correnson) | 2017-07-19 | Statement contracts and WP |
| | |  | 0002316 | | 1 |
Plug-in > pathcrawler | minor | assigned (nicky) | 2017-07-07 | Instrumentation Failure Error in Online Pathcrawler |
| | | | 0002313 | 1 | |
Documentation > manuals | text | assigned (correnson) | 2017-06-23 | suggestions for improvement of Sect.3.6 and 3.7 of the wp manual |
| | | | 0002312 | 1 | 1 |
Plug-in > wp | tweak | assigned (correnson) | 2017-06-15 | false postcondition shouldn't be verified in default memory-model setting |
| | | | 0002311 | | 1 |
Plug-in > wp | text | assigned (correnson) | 2017-06-15 | poor errors message texts for Hoare memory model checks |
| | | | 0002309 | | 1 |
Plug-in > wp | minor | assigned (correnson) | 2017-06-01 | naming the default behavior influences proven obligations |
|
[ First Prev 1 2 3 4 5 6 Next Last ]
|
