| | |  | 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 ? |
