| |  | 0002508 | | 1 |
Kernel | minor | assigned (AllanBlanchard) | 2020-10-06 | cabs2cil fails with statements in expression in a question |
| |  | 0002420 | 1 | 1 |
Plug-in > wp | crash | resolved (correnson) | 2020-09-09 | Wp crashes on a recursive function |
| | | 0002505 | | |
Documentation > manuals | minor | acknowledged (maroneze) | 2020-05-07 | WP manual: hyperlink in table of contents sometimes one off |
| | | 0002504 | | 1 |
Kernel | minor | acknowledged (virgile) | 2020-05-07 | more precise error message for missing closing } of axiomatic block |
| | | 0002498 | | 2 |
Plug-in > wp | minor | assigned (correnson) | 2020-02-24 | munmap() breaks WP analysis |
| | | 0002497 | 2 | 1 |
Plug-in > wp | minor | assigned (correnson) | 2020-02-03 | quantifiers over logic types do not restrict to valid instances |
| | | 0002491 | | 1 |
Plug-in > clang | minor | assigned (fvedrine) | 2020-01-23 | incompatibilité de libc/math.h ?? |
| |  | 0002486 | 2 | 1 |
Graphical User Interface | major | assigned (correnson) | 2019-11-18 | Left pan (file tree and plugin views) inaccessible upon resize in frama-c-gui |
| | | 0002485 | | 1 |
Plug-in > wp | minor | assigned (correnson) | 2019-11-08 | -wp-out missing output for Why3 provers in Frama-C 20 beta |
| | | 0002484 | | |
Plug-in > wp | minor | assigned (correnson) | 2019-11-08 | alt-ergo support in Frama-C 20 beta |
| | | 0002483 | | 1 |
Plug-in > wp | minor | assigned (correnson) | 2019-11-08 | Eprover in Frama-C 20 beta |
| | | 0002404 | 3 | 1 |
Plug-in > wp | minor | acknowledged (correnson) | 2019-10-17 | Shape of VC depends on selection of properties |
| | | 0002427 | 5 | 1 |
Plug-in > wp | minor | acknowledged (correnson) | 2019-10-17 | Prove of \false |
| | | 0002480 | 2 | |
Plug-in > clang | block | confirmed (virgile) | 2019-10-06 | Syntax error in reorder_defs.ml after running make |
| | | 0002474 | 3 | |
Documentation > website | minor | assigned (bobot) | 2019-09-18 | Can't view publications on the wiki |
| |  | 0002463 | 1 | |
Plug-in > clang | major | assigned (virgile) | 2019-07-08 | Error in frama-clang make file |
| | | 0002462 | 2 | |
Plug-in > clang | major | assigned (virgile) | 2019-07-05 | frama-clang failed to install |
| | | 0002457 | 3 | |
Kernel > configure | minor | assigned (virgile) | 2019-06-20 | configure does not detect gtksourceview due to wrong path |
| | | 0002458 | 1 | |
Kernel > configure | minor | assigned (virgile) | 2019-06-20 | build failure due to mangled variable assignment in Makefile |
| | | 0002456 | 1 | |
Kernel > Makefile | minor | assigned (bobot) | 2019-06-18 | Does not build with OCaml 4.08.0 |
| | | 0002449 | 1 | |
Documentation > website | trivial | confirmed (virgile) | 2019-06-10 | invalid links to "ACSL by Example" |
| | | 0002448 | 1 | |
Documentation > website | minor | assigned (bobot) | 2019-06-04 | frama-c installation needs dune > 1.5 package installed |
| | | 0002435 | | 1 |
Kernel | major | assigned (virgile) | 2019-05-08 | kernel generates UnspecifiedSequence when 2 following ternary operators |
| | | 0002327 | | |
Plug-in > E-ACSL | minor | assigned (signoles) | 2019-01-25 | Failure to detect overflows into an allocated area within a struct |
| | | 0002194 | | |
Plug-in > E-ACSL | minor | assigned (signoles) | 2019-01-25 | Failure to record global variable with initialiser |
| | | 0002310 | | 1 |
Plug-in > E-ACSL | minor | assigned (signoles) | 2019-01-25 | Incorrect handling of \initialized when initialized struct is passed to a function by value |
| | | 0002422 | 2 | 1 |
Plug-in > E-ACSL | crash | confirmed (signoles) | 2019-01-23 | Can't use e-acsl on a dynamic library containing all the instrumentations |
| | | 0002412 | 9 | 1 |
Plug-in > E-ACSL | crash | confirmed (signoles) | 2018-12-17 | E-ACSL crash with RTE generated assertion with booleans |
| | | 0002419 | | |
Plug-in > RTE | minor | confirmed (signoles) | 2018-12-17 | Missing cast in code generated by RTE |
| | | 0002416 | 3 | |
Plug-in > E-ACSL | minor | acknowledged (signoles) | 2018-12-11 | missing E-ACSL code, control flow graph, function pointer |
| | | 0002413 | 2 | 1 |
Plug-in > E-ACSL | major | confirmed (signoles) | 2018-12-06 | missing E-ACSL code when ignoring asm annotation |
| | | 0001648 | | |
Kernel | major | assigned (maroneze) | 2018-11-30 | Wrong specification for standard library function memmove |
| | | 0002402 | 3 | |
Plug-in > clang | block | assigned (virgile) | 2018-10-03 | frama-clang fails to compile |
| | | 0002395 | 2 | |
Plug-in > clang | minor | assigned (virgile) | 2018-09-07 | const fields in constructors |
| | | 0002397 | 1 | |
Kernel > ACSL implementation | feature | assigned (virgile) | 2018-08-27 | Model Variables in Frama C |
| | | 0002396 | | |
Plug-in > clang | minor | assigned (virgile) | 2018-08-24 | cast error with reference fields |
| | | 0002376 | | 1 |
Plug-in > jessie | crash | assigned (cmarche) | 2018-05-29 | frama-c/jessie crashes with Unexpected error (Cil.SizeOfError("Undefined sizeof on a function.", _)). |
| | | 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" |
| | | 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 | 1 | |
Graphical User Interface | feature | confirmed (maroneze) | 2018-01-12 | How to use the "Callers ..." context menu item |
| | | 0000945 | 3 | |
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 | 2 | 1 |
Plug-in > Eva | minor | assigned (maroneze) | 2017-12-17 | "pointer comparison" warning emitted for "p==NULL" |
| | | 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 |
| | | 0002276 | 3 | |
Graphical User Interface | tweak | acknowledged (maroneze) | 2017-11-27 | Duplicates are created on the tab "Messages" |
| | | 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 |
| | | 0002308 | | 1 |
Plug-in > wp | feature | assigned (correnson) | 2017-06-01 | suggest to check (loop) assigns clauses by data flow analysis |
| | | 0002307 | 3 | 2 |
Kernel | minor | assigned (virgile) | 2017-05-31 | preprocessor fail: unterminated comment |
| | | 0002298 | 2 | 2 |
Plug-in > wp | crash | assigned (correnson) | 2017-05-11 | "loop assigns" clause ignored in presence of "for"-prefixed clauses |
| | | 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 |
| | | 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 |
| | | 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 |
| | | 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 |
| | | 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 |
| | | 0002245 | | 1 |
Plug-in > wp | major | assigned (correnson) | 2016-08-17 | Nested scopes may cause issues with the validity of created pointers |
| | | 0002244 | | 1 |
Plug-in > wp | major | assigned (correnson) | 2016-08-08 | Logic with read clauses can have their values invalidated by writes to separated memory locations |
| | | 0002241 | | 1 |
Plug-in > wp | major | assigned (correnson) | 2016-07-29 | Implicit casting from integer to real causes failure in WP proof generation |
| | | 0002234 | | |
Plug-in > wp | major | assigned (correnson) | 2016-06-21 | Creating a pointer to a local causes valid pointers above it to lose thier valid status |
| | | 0001278 | 1 | |
Kernel > Makefile | tweak | assigned (bobot) | 2016-06-21 | Path for 'make install-doc-code' for external plug-in |
| | | 0002162 | | |
Kernel > Makefile | minor | assigned (bobot) | 2016-06-21 | Compilation of kernel native cmx is messed up with plugin makefile |
| | | 0002163 | 1 | |
Kernel | feature | assigned (bobot) | 2016-06-21 | Namespace through packs - packing frama-c cmx into a cmxa |
| | | 0002198 | 1 | |
Documentation | minor | assigned (correnson) | 2016-06-21 | typo in output of 'frama-c -wp-help' |
| | | 0002232 | | 1 |
Plug-in > wp | crash | assigned (correnson) | 2016-06-14 | Use of very large real constants cause failures in proof generation in WP |
| | | 0002229 | | 1 |
Plug-in > wp | minor | assigned (correnson) | 2016-05-31 | Validation fails when predicate is used with implicit type conversion. |
| | | 0002228 | | |
Plug-in > wp | minor | assigned (correnson) | 2016-05-16 | Oddities in the modeling of floats and doubles |
| | | 0002223 | 7 | 2 |
Kernel > Makefile | text | assigned (virgile) | 2016-05-10 | Frama-C upgrade installation not foolproof |
| | | 0002226 | 3 | 1 |
Kernel | minor | assigned (correnson) | 2016-05-04 | insertion of "assert true" after a statement influences provability of the statement's contract |
| | | 0002222 | | 1 |
Plug-in > wp | minor | assigned (correnson) | 2016-04-09 | Make find(1) command POSIX-compliant |
| | | 0002219 | | 1 |
Plug-in > wp | crash | assigned (correnson) | 2016-03-22 | Crash with large array initialisation |
| | | 0001911 | 3 | 1 |
Plug-in > wp | minor | acknowledged (correnson) | 2016-03-07 | WP detect a non-natural loop on a do-while(0) loop |
| | | 0002205 | 4 | 4 |
Plug-in > wp | minor | confirmed (correnson) | 2016-02-04 | zombie processes (again) |
| | | 0002207 | | 1 |
Plug-in > wp | crash | assigned (correnson) | 2016-02-03 | WP crashes with \pointer_comparable |
| | | 0002197 | | 1 |
Kernel > ACSL implementation | feature | assigned (virgile) | 2015-12-07 | expression "term!=term" is considered always a predicate, rather than (in some contexts) a term |
| | | 0002195 | 1 | |
Kernel > ACSL implementation | major | assigned (virgile) | 2015-12-06 | ambiguity with consecutive comparison and ternary expressions |
| | | 0002196 | | |
Kernel > ACSL implementation | feature | assigned (virgile) | 2015-12-05 | No syntax to apply lambda expressions |
| | | 0002189 | | 1 |
Plug-in > wp | tweak | assigned (correnson) | 2015-12-03 | Frama-C runs out of memory on small C program (combinatorial explosion in analysis of "main"?) |
| | | 0002188 | | 3 |
Plug-in > wp | minor | assigned (correnson) | 2015-11-30 | bit_test axiomatization doesn't imply == equality from bit-by-bit equality for e.g. uint32 |
| | | 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 |
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 | 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 |
| | | 0001062 | | |
Plug-in > jessie | major | assigned (cmarche) | 2012-01-12 | Jessie incorrectly handles initialization of static array with {} initialization |
| | | 0001058 | | |
Plug-in > jessie | minor | assigned (cmarche) | 2012-01-04 | Jessie incorrectly handles labels |
| | | 0001051 | 1 | 2 |
Plug-in > wp | text | assigned (correnson) | 2011-12-16 | suspicious axiomatization of included,zrange,zunion in .sx file |
| | | 0001047 | | 1 |
Plug-in > jessie | major | assigned (cmarche) | 2011-12-12 | labels defined before loops and used after loops are not correctly translated in jessie |
| | | 0001033 | | |
Plug-in > jessie | feature | assigned (cmarche) | 2011-11-29 | Feature request (Jessie): \fresh (and \separated) |
| | | 0001032 | | 2 |
Plug-in > jessie | feature | assigned (cmarche) | 2011-11-29 | assigns nothing is not possible to proof, if malloc is not in a same function |
| | | 0001008 | 2 | 2 |
Plug-in > jessie | feature | assigned (cmarche) | 2011-11-16 | suggest to supply lower-bound for constant_too_large_2147483647 to Simplify |
| | | 0001007 | 4 | 1 |
Kernel > ACSL implementation | major | assigned (virgile) | 2011-11-10 | wrong proof obligation generated for loop initialization [under why-2.30] |
| | | 0001011 | | |
Plug-in > wp | feature | assigned (correnson) | 2011-11-04 | suggest to provide FILE,LINE references for proof obligations in WP cmd-line output |
| | | 0000980 | | |
Kernel > ACSL implementation | feature | assigned (virgile) | 2011-10-06 | Functional expression in assigns properties |
| | | 0000923 | | 1 |
Plug-in > jessie | major | assigned (cmarche) | 2011-08-12 | Jessie Plugin returns an error. Code with struct-statement, cannot be compiled. |
| | | 0000922 | 1 | 1 |
Plug-in > jessie | major | assigned (cmarche) | 2011-08-12 | Jessie Plugin returns an error. Code with struct-statement, cannot be compiled in a function by call by value. |
| | | 0000846 | | 1 |
Plug-in > jessie | minor | assigned (cmarche) | 2011-05-30 | array access in "decreases"-clause causes "Unexpected internal region in logic" |
| | | 0000834 | | |
Plug-in > jessie | minor | assigned (cmarche) | 2011-05-24 | Computation of regions for axioms in axiomatics |
| | | 0000829 | 3 | 1 |
Plug-in > jessie | minor | assigned (cmarche) | 2011-05-24 | alias between int* and uint* handled incorrectly |
| | | 0000813 | | 1 |
Plug-in > jessie | minor | assigned (cmarche) | 2011-05-09 | struct dereferencing causes uncaught exception |
| | | 0000811 | 2 | 1 |
Plug-in > jessie | minor | assigned (cmarche) | 2011-05-06 | double struct dereferencing causes unbound variable error |
| | | 0000734 | | |
Kernel | tweak | assigned (correnson) | 2011-02-21 | Command.command_generic may raise Sys_error |
| | | 0000713 | | |
Kernel > ACSL implementation | feature | assigned (virgile) | 2011-02-10 | Any number of ";" should be allowed in specifications |
| | | 0000712 | | |
Plug-in > jessie | major | assigned (cmarche) | 2011-02-10 | Validity of valid pointer to struct member cannot be verified |
| | | 0000667 | 3 | 2 |
Plug-in > jessie | crash | assigned (cmarche) | 2011-01-25 | /usr/share/frama-c/libc/stdio.h:107:[jessie] failure: Unexpected exception. |
| | | 0000676 | | |
Kernel | minor | assigned (virgile) | 2011-01-18 | Strange AST produced with unspecified side-effects involve function calls in expressions |
| | | 0000670 | | 1 |
Plug-in > jessie | minor | assigned (cmarche) | 2011-01-12 | In certain circumstances Jessie cannot analyse files that it generates |
| | | 0000654 | | |
Plug-in > jessie | minor | assigned (cmarche) | 2010-12-25 | Incorrect translation (Unbound variable) |
| | | 0000652 | | 1 |
Plug-in > jessie | minor | assigned (cmarche) | 2010-12-24 | pointer arithmetic |
| | | 0000651 | | 1 |
Plug-in > jessie | minor | assigned (cmarche) | 2010-12-24 | array id "shift" |
| | | 0000643 | 2 | 1 |
Kernel > ACSL implementation | minor | assigned (virgile) | 2010-12-18 | Incorrect parsing of complex lemma |
| | | 0000601 | | 1 |
Kernel > ACSL implementation | feature | assigned (virgile) | 2010-12-16 | no multiple assert-clauses accepted in /*@...*/-style comment |
| | | 0000605 | 1 | |
Kernel > ACSL implementation | minor | assigned (virgile) | 2010-12-16 | Empty specification causes syntax error |
| | | 0000632 | | 1 |
Plug-in > jessie | feature | assigned (cmarche) | 2010-11-29 | Suggest to rename user identifiers to avoid name clashes in ..._why.sx files |
| | | 0000617 | 2 | |
Plug-in > jessie | minor | confirmed (cmarche) | 2010-11-17 | assigns nothing ? |
| | | 0000629 | 1 | |
Plug-in > jessie | minor | assigned (cmarche) | 2010-11-17 | Incorrect processing of "type var[]" constructions |
| | | 0000615 | 1 | 1 |
Plug-in > jessie | major | assigned (cmarche) | 2010-10-22 | separately verified files show code-bug when linked together |
| | | 0000614 | | 1 |
Plug-in > jessie | minor | assigned (cmarche) | 2010-10-22 | "\valid(&aaa)" unprovable for global variable aaa - missing antecedens in proof obligation? |
| | | 0000593 | 4 | 1 |
Kernel | minor | confirmed (virgile) | 2010-10-01 | Parse error when using a wide string literal to initialize uint16 array |
| | | 0000590 | | 1 |
Plug-in > jessie | minor | assigned (cmarche) | 2010-09-22 | Jessie plugin does not support logic label Post in ensures clause |
| | | 0000544 | | |
Plug-in > jessie | feature | assigned (cmarche) | 2010-07-17 | Enhancement on assigns annotation and the name of proof obligation |
| | | 0000102 | 1 | |
Plug-in > jessie | major | confirmed (cmarche) | 2010-07-13 | Jessie: struct field's validity |
| | | 0000518 | | 1 |
Plug-in > jessie | minor | assigned (cmarche) | 2010-06-22 | Loop assigns are not taken into account when proving a safety PO |
| | | 0000502 | | |
Plug-in > jessie | minor | assigned (cmarche) | 2010-06-13 | Unbound label in Jessie-generated Why file when using logic function in assigns clause |
| | | 0000289 | 1 | 1 |
Plug-in > jessie | major | acknowledged (virgile) | 2010-06-09 | unsoundness of Jessie with respect to expression evaluation of ANSI-C |
| | | 0000485 | | |
Plug-in > jessie | feature | assigned (cmarche) | 2010-05-18 | Code containing consts should be verifiable |
| | | 0000480 | | |
Plug-in > jessie | crash | assigned (cmarche) | 2010-05-12 | volatile annotation breaks type checker |
| | | 0000456 | | 1 |
Plug-in > jessie | minor | assigned (cmarche) | 2010-04-23 | Lack of parameter generation |
| | | 0000433 | | 1 |
Plug-in > jessie | tweak | assigned (virgile) | 2010-03-23 | different translation of casted constants in program-code and in assertion |
| | | 0000424 | 3 | 1 |
Plug-in > jessie | minor | assigned (cmarche) | 2010-03-22 | Uncaught exception: Failure("Unexpected internal region in logic") |
| | | 0000416 | | 1 |
Plug-in > jessie | minor | assigned (cmarche) | 2010-02-22 | local array decl with non-constant size causes Why error |
| | | 0000072 | 1 | |
Plug-in > jessie | minor | assigned (cmarche) | 2010-02-12 | The specifications of statements are not translated |
| | | 0000079 | 2 | |
Kernel > ACSL implementation | feature | assigned (virgile) | 2010-02-05 | Better support of //@ style |
| | | 0000387 | | |
Kernel > ACSL implementation | feature | assigned (virgile) | 2010-02-05 | ghost integer ? |
| | | 0000336 | 1 | |
Plug-in > jessie | major | assigned (cmarche) | 2010-01-22 | cast between homogenous struct and array |
| | | 0000373 | | |
Plug-in > jessie | major | assigned (cmarche) | 2010-01-14 | Global invariants are not verified |
| | | 0000348 | 1 | |
Plug-in > jessie | major | assigned (cmarche) | 2009-12-03 | Arithmetic safety of bitwise operators cannot be verified |
| | | 0000039 | 1 | |
Plug-in > jessie | minor | confirmed (cmarche) | 2009-11-24 | Frama-C/Jessie: memory set problem |
| | | 0000335 | | 1 |
Plug-in > jessie | minor | assigned (cmarche) | 2009-11-20 | Unbound reference raised by Why |
| | | 0000328 | | 1 |
Plug-in > jessie | major | assigned (cmarche) | 2009-11-13 | assertion failed in Jessie with bitfields inside union |
| | | 0000291 | | 1 |
Plug-in > jessie | minor | assigned (cmarche) | 2009-10-20 | Unbound variable raised by why in presence of an unsafe cast |
| | | 0000040 | | |
Plug-in > jessie | minor | confirmed (cmarche) | 2009-10-15 | Frama-C/Jessie: typing error |
| | | 0000261 | 2 | 1 |
Kernel | minor | acknowledged (virgile) | 2009-10-01 | Frama-C fails to parse a file |
| | | 0000256 | | |
Plug-in > jessie | minor | assigned (cmarche) | 2009-09-25 | array range in requires predicate |
| | | 0000025 | | |
Plug-in > jessie | minor | acknowledged (virgile) | 2009-09-21 | type invariants |
| | | 0000215 | | 1 |
Plug-in > jessie | minor | assigned (cmarche) | 2009-08-25 | Mise en hypothèse de la précondition d'une opération appelée |
| | | 0000185 | 1 | |
Plug-in > jessie | major | assigned (cmarche) | 2009-07-17 | Frama-C cannot process properly arrays of structures |
| | | 0000178 | 1 | |
Plug-in > jessie | minor | confirmed (cmarche) | 2009-07-09 | type error in generated why file |
| | | 0000092 | 1 | |
Plug-in > jessie | minor | assigned (cmarche) | 2009-06-19 | Why error with logic functions returning a pointer |
| | | 0000042 | 1 | |
Plug-in > jessie | feature | assigned (cmarche) | 2009-06-17 | Default invariant should be inferred for loops |
| | | 0000031 | | |
Plug-in > jessie | minor | acknowledged (cmarche) | 2009-06-17 | Why- error :-jessie-no-regions and assigns does not work |
| | | 0000032 | | |
Plug-in > jessie | minor | assigned (cmarche) | 2009-04-10 | Internal error with assign specification on bi-dimensional arrays |
| | | 0000038 | | |
Plug-in > jessie | minor | assigned (cmarche) | 2009-04-10 | Jessie crashes on simple program without annotations |
