|
Viewing Issues (1 - 50 / 236)
[ Print Reports ] [ CSV Export ] [ Excel Export ]
[ First Prev 1 2 3 4 5 Next Last ]
|
| | | P | ID | # |  |
Category | Severity | Status | Updated | Summary |
|
| | |  | 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 |
| | | | 0002253 | 3 | |
Kernel > libc | minor | resolved (maroneze) | 2017-06-14 | File frama-c/libc/features.h should include definition of the macro __GNUC_PREREQ from file /usr/include/features.h |
| | | | 0002310 | | 1 |
Plug-in > E-ACSL | minor | assigned (kvorobyov) | 2017-06-14 | Incorrect handling of \initialized when initialized struct is passed to a function by value |
| | | | 0001467 | 3 | |
Kernel | feature | resolved (valentin.perrelle) | 2017-06-09 | Parser does not handle mixed concatenations of wide and non-wide strings |
| | | | 0002309 | | 1 |
Plug-in > wp | minor | assigned (correnson) | 2017-06-01 | naming the default behavior influences proven obligations |
| | |  | 0002308 | | 1 |
Plug-in > wp | feature | assigned (correnson) | 2017-06-01 | suggest to check (loop) assigns clauses by data flow analysis |
| | | | 0002297 | 2 | 1 |
Kernel | minor | resolved (maroneze) | 2017-05-31 | syntax error before loop contract reported after loop contract |
| | | | 0002306 | 2 | 1 |
Kernel | minor | assigned (yakobowski) | 2017-05-31 | Support for flexible array members |
| | | | 0002307 | 5 | 2 |
Kernel | minor | assigned (virgile) | 2017-05-31 | preprocessor fail: unterminated comment |
| | | | 0002305 | | 2 |
Plug-in > E-ACSL | minor | assigned (kvorobyov) | 2017-05-31 | E-ACSL: proper bitfileds handling |
| | | | 0002304 | | 2 |
Plug-in > E-ACSL | major | assigned (kvorobyov) | 2017-05-29 | E-ACSL: compilation fail: generated functions doesn't have static inline attributes |
| | | | 0002303 | | 2 |
Plug-in > E-ACSL | major | assigned (kvorobyov) | 2017-05-29 | E-ACSL generates functions definitions without argument-names |
| | |  | 0002302 | | 1 |
Plug-in > slicing | major | assigned (Nikolai_Kosmatov) | 2017-05-23 | the return statement of a called function was wrongly removed |
| | | | 0002301 | 1 | 1 |
Kernel | crash | new | 2017-05-11 | statement contract apparently confuses parser |
| | | | 0002298 | 2 | 2 |
Plug-in > wp | crash | assigned (correnson) | 2017-05-11 | "loop assigns" clause ignored in presence of "for"-prefixed clauses |
| | | | 0002300 | | 1 |
Documentation > ACSL | text | assigned (patrick) | 2017-05-11 | suggest to clarify semantics of statement contract in ACSL implementation manual |
| | | | 0002299 | | 1 |
Plug-in > wp | block | assigned (correnson) | 2017-05-10 | Some ACSL mathematical functions crash WP |
| | | | 0002296 | | 1 |
Plug-in > wp | feature | assigned (correnson) | 2017-05-08 | axiom about bounds of lsl result needed in the long run |
| | | | 0002293 | | 3 |
Plug-in > wp | minor | assigned (correnson) | 2017-03-16 | Frama-C gives succeeding lemma, rather than preceding lemmas, as hypothesis to e.g. Cvc4 |
| | | | 0002292 | 1 | 7 |
Plug-in > wp | minor | assigned (correnson) | 2017-03-16 | signature axiom omitted in Coq and Alt-ergo translation |
| | | | 0001761 | 1 | |
Kernel > ACSL implementation | major | assigned (virgile) | 2017-03-14 | Check that all occurrences of *p in assigns are guarded by a \valid(p) in requires |
| | | | 0000628 | 1 | 1 |
Plug-in > jessie | minor | assigned (cmarche) | 2017-03-14 | Frama-C/Jessie does not recognize the length of array in struct |
| | | | 0002291 | 1 | 3 |
Plug-in > wp | minor | assigned (correnson) | 2017-03-13 | suggestion: translate axioms and implication premises in forward order to coq |
| | | | 0002290 | 1 | 1 |
Kernel | minor | assigned (correnson) | 2017-03-10 | incomplete loading of saved state when using WP? |
| | | | 0002270 | 4 | |
Graphical User Interface | major | confirmed (maroneze) | 2017-03-06 | Command "Show callgraph" fails. |
| | | | 0002259 | 3 | |
Plug-in > value analysis | text | assigned (yakobowski) | 2017-03-06 | suggest to provide and document a unique warning string to grep for in value-analysis output files |
| | | | 0002256 | 3 | 1 |
Plug-in > value analysis | minor | assigned (yakobowski) | 2017-03-06 | "pointer comparison" warning emitted for "p==NULL" |
| | | | 0002289 | | |
Plug-in > wp | feature | assigned (correnson) | 2017-03-01 | Why3ide cannot be opened in this version |
| | | | 0002286 | 1 | 4 |
Plug-in > wp | minor | assigned (correnson) | 2017-02-27 | lemma tacitly omitted from prover assumptions |
| | | | 0002285 | | 1 |
Plug-in > wp | feature | assigned (correnson) | 2017-02-27 | suggest boolean expressions for "-wp-prop" arguments |
| | | | 0002282 | | 2 |
Plug-in > wp | minor | assigned (correnson) | 2017-02-16 | applicability of Coq proof script depends on order of include files |
| | | | 0002280 | | 1 |
Plug-in > wp | tweak | assigned (correnson) | 2017-02-14 | Frama-C sleeps too much when discharging trivial goals |
| | | | 0002278 | 1 | 2 |
Plug-in > wp | minor | acknowledged (correnson) | 2017-02-06 | problem with Qed's simplification power |
| | | | 0002276 | 2 | |
Graphical User Interface | tweak | feedback (maroneze) | 2017-02-06 | Duplicates are created on the tab "Messages" |
| | | | 0002275 | 5 | 6 |
Plug-in > wp | minor | confirmed (correnson) | 2017-02-03 | translation to why3 of int* argument to logic function |
| | | | 0002274 | 1 | |
Kernel | tweak | confirmed (maroneze) | 2017-01-24 | It is impossble to change log file without kinds of message changing. |
| | | | 0002272 | 2 | 1 |
Kernel | minor | assigned (virgile) | 2017-01-16 | WP appears to assume left-to-right evaluation order for int addition |
| | | | 0000945 | 3 | |
Plug-in > value analysis | minor | assigned (maroneze) | 2017-01-12 | Should warn for overlapping lv=lv; assignments |
| | | | 0002264 | 1 | 1 |
Kernel > ACSL implementation | major | assigned (virgile) | 2017-01-04 | structure in logic not supported? |
| | | | 0002266 | | |
Plug-in > wp | minor | assigned (correnson) | 2017-01-02 | WP inserts unwanted new lines into Coq proofs |
| | | | 0002265 | | 1 |
Kernel > ACSL implementation | minor | assigned (virgile) | 2017-01-02 | label Pre in function contracts |
| | | | 0002263 | 1 | |
Plug-in > wp | minor | assigned (correnson) | 2016-12-16 | Why3 warning |
| | | | 0002262 | 3 | 1 |
Plug-in > wp | minor | assigned (correnson) | 2016-12-16 | more prover processes run than expected |
| | | | 0002261 | 8 | |
Plug-in > wp | minor | assigned (virgile) | 2016-12-16 | wp: the example from Getting Started guide doesn't work (all goals are Unknown) |
| | | | 0002248 | 2 | 1 |
Kernel | text | assigned (virgile) | 2016-12-08 | option "-print" prints array upper bound in type before parameter name, rather than after it |
| | | | 0002260 | | |
Plug-in > wp | minor | assigned (correnson) | 2016-12-03 | error in Coq file generation |
| | | | 0002254 | | 1 |
Plug-in > value analysis | minor | assigned (yakobowski) | 2016-11-07 | Option "-lib-entry" results misses possible values of function pointers |
| | | | 0002194 | | |
Plug-in > E-ACSL | minor | assigned (signoles) | 2016-09-13 | Failure to record global variable with initialiser |
|
[ First Prev 1 2 3 4 5 Next Last ]
|
