|
Viewing Issues ( 1 - 220 ) |
|
| | P | ID | # | Category | Severity | Status | Updated | Summary |
|
| | 0000690 | 7 | [Frama-C]
Plug-in > slicing | feature | assigned (Boris Yakobowski) | 2012-05-16 | Slicing does not preserve some ACSL constructs |
| | 0001180 | 1 | [Frama-C]
Kernel | minor | resolved (Julien Signoles) | 2012-05-16 | Port to OCamlgraph 1.8.2 |
|  | 0000419 | 1 | [Frama-C]
Documentation | text | resolved (Julien Signoles) | 2012-05-16 | Plug-in dev guide: tutorial for kernel integrated plug-in is out-of-date |
| | 0000764 | 3 | [Frama-C]
Kernel | feature | resolved (Julien Signoles) | 2012-05-16 | Specifying several directories in environment variables FRAMAC_* |
| | 0001179 | 8 | [Frama-C]
Plug-in > wp | tweak | feedback (Loïc Correnson) | 2012-05-15 | Suggest to supply values of global consts to provers |
| | 0001089 | 2 | [Frama-C]
Documentation | minor | resolved (Julien Signoles) | 2012-05-10 | Updated example in plugin-development-guide |
| | 0001036 | 3 | [Frama-C]
Documentation | feature | resolved (Julien Signoles) | 2012-05-09 | In section 5.11.5 of the Plugin developper manual : Reference to modules that neither appear in the API nor in Frama-c source. |
| | 0001178 | 3 | [Frama-C]
Kernel | major | resolved (Virgile Prevosto) | 2012-05-07 | Several types for the same function |
| | 0001085 | 5 | [Frama-C]
Documentation | minor | resolved (Julien Signoles) | 2012-04-30 | Cute boolean options too cute for their own good |
| | 0001127 | 4 | [Frama-C]
Kernel | minor | resolved (Julien Signoles) | 2012-04-26 | Error in Type.pp_ml_name with Datatype.String.Set.ty |
| | 0001165 | 2 | [Frama-C]
Kernel | minor | resolved (Virgile Prevosto) | 2012-04-24 | [libc] erreur: #endif sans #if |
| | 0001136 | 2 | [Frama-C]
Kernel | minor | feedback (Virgile Prevosto) | 2012-04-24 | [Globals.Vars.get_astinfo] doesn't work |
| | 0001110 | 6 | [Frama-C]
Kernel | crash | resolved (Boris Yakobowski) | 2012-04-18 | Using Filter without Value |
| | 0001161 | 1 | [Frama-C]
Plug-in > jessie | feature | assigned (Claude Marché) | 2012-04-17 | error in wp_behav.c |
| | 0001159 | 2 | [Frama-C]
Plug-in > jessie | feature | assigned (Claude Marché) | 2012-04-17 | cast of pointer to structures |
| | 0001162 | 1 | [Frama-C]
Kernel > ACSL implementation | minor | resolved (Virgile Prevosto) | 2012-04-17 | "for" clause is refused |
| | 0001154 | 4 | [Frama-C]
Plug-in > jessie | minor | assigned (Claude Marché) | 2012-04-17 | erroneous left value (structure field) |
| | 0001156 | 3 | [Frama-C]
Plug-in > jessie | feature | assigned (Claude Marché) | 2012-04-17 | struct type not supported in type invariant |
| | 0001149 | 6 | [Frama-C]
Plug-in > jessie | minor | resolved (Virgile Prevosto) | 2012-04-17 | function names are restricted due to exclusion of ACSL keywords |
| | 0001148 | 6 | [Frama-C]
Plug-in > jessie | feature | feedback (Claude Marché) | 2012-04-17 | tsets union not accepted in predicates |
| | 0001155 | 3 | [Frama-C]
Plug-in > jessie | feature | assigned (Claude Marché) | 2012-04-17 | inductive clause seems not to pass jessie translation |
| | 0001092 | 1 | [Frama-C]
Documentation | text | resolved (Pascal Cuoq) | 2012-04-17 | some typos etc. in the value-analysis manual |
| | 0001157 | 3 | [Frama-C]
Plug-in > jessie | minor | assigned (Claude Marché) | 2012-04-17 | erroneous logic syntax |
| | 0001160 | 4 | [Frama-C]
Plug-in > jessie | feature | assigned (Claude Marché) | 2012-04-17 | struct not supported as logic argument |
| | 0001151 | 4 | [Frama-C]
Plug-in > jessie | feature | assigned (Claude Marché) | 2012-04-17 | comparison of structures not implemented |
| | 0001158 | 3 | [Frama-C]
Plug-in > jessie | feature | assigned (Claude Marché) | 2012-04-17 | inlining of assembleur is not supported |
| | 0001153 | 3 | [Frama-C]
Plug-in > jessie | feature | assigned (Claude Marché) | 2012-04-17 | pointer casts not supported |
| | 0001024 | 11 | [Frama-C]
Plug-in > value analysis | major | resolved (Boris Yakobowski) | 2012-04-16 | Emitted assertion wrongly reduces to bottom (apparently) (csmith) |
| | 0000687 | 6 | [Frama-C]
Kernel | minor | assigned (Julien Signoles) | 2012-04-15 | Losing some cmdline option settings when loading |
| | 0001145 | 2 | [Frama-C]
Kernel > Makefile | minor | resolved (Julien Signoles) | 2012-04-12 | PLUGIN_LINK_GUI_OFLAGS not used ? |
| | 0000728 | 3 | [Frama-C]
Kernel | minor | resolved (Virgile Prevosto) | 2012-04-12 | Arguments are not checked when function call precedes function declaration |
| | 0000759 | 6 | [Frama-C]
Plug-in > value analysis | major | assigned (Boris Yakobowski) | 2012-04-11 | wrong treatment for const arrays in lib-entry mode |
| | 0001144 | 1 | [Frama-C]
Kernel | minor | resolved (Virgile Prevosto) | 2012-04-09 | 17944 using option -unspecified-access, no alarm for x + (x=0) |
| | 0001142 | 4 | [Frama-C]
Plug-in > value analysis | minor | resolved (Boris Yakobowski) | 2012-04-09 | Bad AST generation ? |
| | 0001026 | | [Frama-C]
Plug-in > value analysis | major | assigned (Boris Yakobowski) | 2012-04-08 | value analysis memory consumption problem when using -lib-entry option |
| | 0001141 | 2 | [Frama-C]
Kernel | minor | resolved (Benjamin Monate) | 2012-04-06 | incorrect UINT8_MAX (and others) |
| | 0001140 | 8 | [Frama-C]
Kernel | minor | resolved (Benjamin Monate) | 2012-04-06 | Strange declaration mismatch |
| | 0000915 | 2 | [Frama-C]
Plug-in > value analysis | feature | assigned (Pascal Cuoq) | 2012-04-05 | interest for a built-in memset function |
| | 0000831 | 2 | [Frama-C]
Kernel | major | feedback (Virgile Prevosto) | 2012-04-05 | Successive calls of Cil.emptyfunction generate a Failure("trying to redefine an existing kernel function") |
| | 0000594 | 1 | [Frama-C]
Kernel | minor | resolved (Virgile Prevosto) | 2012-04-05 | Kernel error with RTE generated annotations: invalid operands (bitwise) |
| | 0000384 | 2 | [Frama-C]
Kernel | minor | resolved (Virgile Prevosto) | 2012-04-05 | Labels in loops are not unrolled |
| | 0001116 | 3 | [Frama-C]
Kernel | trivial | resolved (Virgile Prevosto) | 2012-04-02 | axiom outside axiomatic tacitly ignored in presence of struct |
| | 0001139 | 2 | [Frama-C]
Kernel | crash | resolved (Patrick Baudin) | 2012-04-02 | unrolling labeled loops |
| | 0001135 | 2 | [Frama-C]
Kernel | major | resolved (Virgile Prevosto) | 2012-04-02 | unrolling loop statements with labels into there annotations are not handled correctly (in conjunction with -ulevel) |
| | 0001126 | 1 | [Frama-C]
Kernel | minor | resolved (Virgile Prevosto) | 2012-03-30 | AST check failure : problem with generated block-local variables |
| | 0001113 | 2 | [Frama-C]
Kernel | minor | resolved (Virgile Prevosto) | 2012-03-30 | Preprocessing code may yield expanded code with undeclared variables |
| | 0001128 | 9 | [Frama-C]
Kernel > Makefile | feature | acknowledged (Julien Signoles) | 2012-03-29 | Install frama-c.top |
| | 0000888 | 2 | [Frama-C]
Kernel | minor | assigned (Virgile Prevosto) | 2012-03-28 | 14292: warn for unspecified side-effect that are separated by a function call (csmith) |
| | 0001114 | 1 | [Frama-C]
Kernel | minor | resolved (Virgile Prevosto) | 2012-03-27 | 17514, -unspecified-access and if (*p = (*p < 3)) (csmith) |
| | 0001134 | | [Frama-C]
Kernel | minor | assigned (Virgile Prevosto) | 2012-03-26 | Crash when #include <complex.h> |
| | 0001132 | 3 | [Frama-C]
Kernel | minor | resolved (Julien Signoles) | 2012-03-26 | -cpp-extra-args option should be a list |
| | 0000929 | 1 | [Frama-C]
Kernel | feature | assigned (Virgile Prevosto) | 2012-03-22 | syntax error in value binary assignment |
| | 0001122 | | [Frama-C]
Graphical User Interface | minor | acknowledged (Julien Signoles) | 2012-03-19 | Opening consolidation graph crashes when 'dot' is missing |
| | 0001117 | 2 | [Frama-C]
Plug-in > wp | tweak | resolved (Philippe Herrmann) | 2012-03-14 | addr_eq versus = and <> in generated axioms access_update, access_update_neq |
| | 0001119 | 2 | [Frama-C]
Plug-in > wp | minor | assigned (Philippe Herrmann) | 2012-03-14 | couldn't verify series of struct member initializations |
| | 0000107 | 10 | [Frama-C]
Plug-in > slicing | major | resolved (Boris Yakobowski) | 2012-03-09 | Slicer: slicing preserving some undesired function calls |
| | 0001003 | 8 | [Frama-C]
Plug-in > jessie | tweak | feedback (Claude Marché) | 2012-03-06 | conditional expression (?:) raises uncaught exception under why-2.30 |
| | 0001108 | 2 | [Frama-C]
Plug-in > wp | minor | resolved (Loïc Correnson) | 2012-03-01 | Bitwise Operators |
| | 0001098 | 2 | [Frama-C]
Documentation | minor | confirmed (Benjamin Monate) | 2012-02-28 | Non working example in the documentation |
| | 0001102 | 2 | [Frama-C]
Graphical User Interface | tweak | resolved (Benjamin Monate) | 2012-02-28 | Rename frama-c-gui.config |
| | 0001104 | 1 | [Frama-C]
Graphical User Interface | minor | assigned (Loïc Correnson) | 2012-02-24 | value analysis warning disappears from 'Messages' window in gui after 'Reparse' button clicked |
| | 0001023 | 2 | [Frama-C]
Documentation | text | resolved (Virgile Prevosto) | 2012-02-23 | \valid_range not mentioned in Acsl manual |
| | 0000733 | 4 | [Frama-C]
Plug-in > inout | major | acknowledged (Boris Yakobowski) | 2012-02-23 | Invalid results in presence of pseudo-recursive calls in inout and from |
| | 0001103 | 2 | [Frama-C]
Kernel | feature | assigned (Virgile Prevosto) | 2012-02-23 | Default @requires property for the [main] function |
| | 0001081 | 3 | [Frama-C]
Kernel | minor | resolved (Virgile Prevosto) | 2012-02-22 | foo ? (void)x : (signed char)y (csmithreduction) |
| | 0001070 | 1 | [Frama-C]
Kernel > configure | feature | resolved (Virgile Prevosto) | 2012-02-22 | Getting frama-c version through --enable-external |
| | 0001069 | 1 | [Frama-C]
Kernel > configure | minor | resolved (Virgile Prevosto) | 2012-02-21 | Handling error in external plug-in through --enable-external |
| | 0001099 | 5 | [Frama-C]
Kernel | crash | resolved (Virgile Prevosto) | 2012-02-21 | Crash when parsing an incorrect program with pointer to arrays |
| | 0001100 | 2 | [Frama-C]
Kernel | minor | resolved (Boris Yakobowski) | 2012-02-20 | Loop unrolling sub-optimal in presence of some labels |
| | 0001073 | 3 | [Frama-C]
Kernel | major | resolved (Virgile Prevosto) | 2012-02-17 | Some functions lose their formals after File.create_project_from_visitor |
| | 0001093 | | [Frama-C]
Plug-in > jessie | crash | assigned (Claude Marché) | 2012-02-14 | Passing multi-dimensional arrays via reference fails |
| | 0000967 | 2 | [Frama-C]
Kernel > ACSL implementation | minor | assigned (Virgile Prevosto) | 2012-02-09 | unbound function \length in annotation |
| | 0001088 | 1 | [Frama-C]
Documentation | minor | resolved (Julien Signoles) | 2012-02-09 | Plugin-development-guide section 2.1.2 |
| | 0001014 | 2 | [Frama-C]
Documentation | minor | resolved (Julien Signoles) | 2012-02-09 | gui and doc |
| | 0001025 | 15 | [Frama-C]
Kernel | minor | resolved (Boris Yakobowski) | 2012-02-08 | Cil.prepareCfg (or -simplify-cfg option) insert dummy locations in the ast |
| | 0001083 | 5 | [Frama-C]
Plug-in > RTE | major | resolved (Philippe Herrmann) | 2012-02-08 | RTE does not check for downcast of unsigned integer |
| | 0001082 | 1 | [Frama-C]
Kernel > Makefile | trivial | resolved (Julien Signoles) | 2012-02-07 | Bad links in generated documentation modules.svg |
| | 0001079 | 3 | [Frama-C]
Plug-in > scope | feature | resolved (Boris Yakobowski) | 2012-02-04 | Imprecision of 'Defs' when querying precise location |
| | 0000765 | 4 | [Frama-C]
Plug-in > wp | minor | assigned (Loïc Correnson) | 2012-01-31 | Post-state of statement spec |
| | 0001076 | 2 | [Frama-C]
Plug-in > value analysis | minor | assigned (Pascal Cuoq) | 2012-01-31 | "volatile" ignored |
| | 0001074 | 5 | [Frama-C]
Plug-in > value analysis | major | resolved (Pascal Cuoq) | 2012-01-30 | Imprecise result on almost deterministic program |
| | 0000624 | 3 | [Frama-C]
Kernel | crash | acknowledged (Loïc Correnson) | 2012-01-30 | Logging huge messages makes kernel crashing |
| | 0000989 | 2 | [Frama-C]
Plug-in > syntactic callgraph | minor | resolved (Julien Signoles) | 2012-01-27 | Strange dot callgraphs |
| | 0001071 | 5 | [Frama-C]
Plug-in > value analysis | tweak | resolved (Pascal Cuoq) | 2012-01-27 | relation chains exploited incompletely |
| | 0001072 | 3 | [Frama-C]
Plug-in > value analysis | feature | resolved (Boris Yakobowski) | 2012-01-27 | evaluation of && and || in term position |
| | 0001067 | 5 | [Frama-C]
Documentation | trivial | resolved (Pascal Cuoq) | 2012-01-26 | suggest to mention option "-value-help" in value analysis manual |
| | 0000252 | | [Frama-C]
Plug-in > jessie | feature | assigned (Virgile Prevosto) | 2012-01-21 | type invariants |
| | 0001066 | 2 | [Frama-C]
Plug-in > value analysis | trivial | resolved (Pascal Cuoq) | 2012-01-19 | suggest to use "NULL" rather than "&NULL" for null pointer |
| | 0001062 | | [Frama-C]
Plug-in > jessie | major | assigned (Claude Marché) | 2012-01-12 | Jessie incorrectly handles initialization of static array with {} initialization |
| | 0001061 | | [Frama-C]
Plug-in > jessie | minor | assigned (Claude Marché) | 2012-01-12 | Jessie incorrectly handles initialization of array |
| | 0001060 | | [Frama-C]
Plug-in > wp | crash | assigned (Loïc Correnson) | 2012-01-11 | WP 0.5 crashes with an Unbound label parameter 'Here' |
| | 0001059 | 1 | [Frama-C]
Kernel | major | assigned (Virgile Prevosto) | 2012-01-08 | Undefined behavior with embedded assignment goes undetected |
| | 0001056 | 2 | [Frama-C]
Kernel > ACSL implementation | crash | resolved (Virgile Prevosto) | 2012-01-06 | Frama-c fails when Starting Jessie Translation |
| | 0001027 | 2 | [Frama-C]
Kernel > ACSL implementation | crash | resolved (Virgile Prevosto) | 2012-01-06 | incompatible types for a correct spec |
| | 0001058 | | [Frama-C]
Plug-in > jessie | minor | assigned (Claude Marché) | 2012-01-04 | Jessie incorrectly handles labels |
| | 0001050 | 2 | [Frama-C]
Plug-in > aoraï | minor | resolved (Virgile Prevosto) | 2012-01-04 | Sequence number generated by aorai is incorrect |
| | 0001051 | 1 | [Frama-C]
Plug-in > wp | text | assigned (Loïc Correnson) | 2011-12-16 | suspicious axiomatization of included,zrange,zunion in .sx file |
| | 0001047 | | [Frama-C]
Plug-in > jessie | major | assigned (Claude Marché) | 2011-12-12 | labels defined before loops and used after loops are not correctly translated in jessie |
| | 0001046 | 1 | [Frama-C]
Plug-in > jessie | minor | assigned (Claude Marché) | 2011-12-11 | Wrong sequence of lemmas |
| | 0001044 | | [Frama-C]
Plug-in > value analysis | feature | assigned (Pascal Cuoq) | 2011-12-11 | Smarter access to array of struct of array |
| | 0001038 | | [Frama-C]
Plug-in > wp | text | assigned (Loïc Correnson) | 2011-12-05 | lemma tacitly ignored in absense of C code |
| | 0001028 | 3 | [Frama-C]
Plug-in > wp | minor | acknowledged (Loïc Correnson) | 2011-12-01 | unable to prove that comparison-result is 0 or 1: insufficient axiomatization of eq_int_bool? |
| | 0001037 | | [Frama-C]
Plug-in > wp | minor | assigned (Loïc Correnson) | 2011-12-01 | undefined (or built-in?) predicate "global" in proof obligation |
| | 0001033 | | [Frama-C]
Plug-in > jessie | feature | assigned (Claude Marché) | 2011-11-29 | Feature request (Jessie): \fresh (and \separated) |
| | 0001032 | | [Frama-C]
Plug-in > jessie | feature | assigned (Claude Marché) | 2011-11-29 | assigns nothing is not possible to proof, if malloc is not in a same function |
| | 0000997 | 7 | [Frama-C]
Plug-in > value analysis | minor | resolved (Boris Yakobowski) | 2011-11-21 | Warnings in presence of Top floats |
| | 0001021 | 2 | [Frama-C]
Graphical User Interface | minor | resolved (Boris Yakobowski) | 2011-11-18 | request for pretty printing only one property by lines |
| | 0001022 | | [Frama-C]
Documentation | text | assigned (Virgile Prevosto) | 2011-11-18 | suggest to explain semantics of missing loop assigns clause in Acsl manual |
| | 0001019 | 1 | [Frama-C]
Kernel > ACSL implementation | minor | resolved (Virgile Prevosto) | 2011-11-16 | #defined variable unrecognized in assigns, except in parentheses |
| | 0001008 | 2 | [Frama-C]
Plug-in > jessie | feature | assigned (Claude Marché) | 2011-11-16 | suggest to supply lower-bound for constant_too_large_2147483647 to Simplify |
| | 0001013 | 7 | [Frama-C]
Kernel | crash | resolved (Boris Yakobowski) | 2011-11-14 | Crash when casting something to type void |
| | 0001017 | 3 | [Frama-C]
Kernel > ACSL implementation | feature | assigned (Virgile Prevosto) | 2011-11-14 | suggest to warn about ensures clauses containing only \old variables |
| | 0001007 | 4 | [Frama-C]
Kernel > ACSL implementation | major | assigned (Virgile Prevosto) | 2011-11-10 | wrong proof obligation generated for loop initialization [under why-2.30] |
| | 0001009 | 1 | [Frama-C]
Kernel > ACSL implementation | minor | resolved (Virgile Prevosto) | 2011-11-09 | code annotation placed above a local declaration are not correctly handled |
| | 0001006 | 2 | [Frama-C]
Kernel | minor | resolved (Virgile Prevosto) | 2011-11-07 | Kernel should desugar "complete behaviors" |
| | 0001002 | | [Frama-C]
Plug-in > jessie | feature | assigned (Claude Marché) | 2011-11-07 | weak feature request for \separated under why-2.30 |
| | 0001011 | | [Frama-C]
Plug-in > wp | feature | assigned (Loïc Correnson) | 2011-11-04 | suggest to provide FILE,LINE references for proof obligations in WP cmd-line output |
| | 0001010 | | [Frama-C]
Documentation | feature | assigned (Loïc Correnson) | 2011-11-04 | warn on stderr about current restrictions, and list them in WP manual |
| | 0000679 | 13 | [Frama-C]
Plug-in > slicing | crash | resolved (Anne Pacalet) | 2011-11-04 | untypable ACSL in a sliced program containing \at(p,label) when the label was removed |
| | 0000993 | 10 | [Frama-C]
Plug-in > functional dependencies | major | resolved (Boris Yakobowski) | 2011-11-04 | Incorrect dependencies in presence of declared functions |
| | 0001005 | 1 | [Frama-C]
Kernel | crash | resolved (Virgile Prevosto) | 2011-10-31 | defining two axioms with same name causes kernel crash |
| | 0001004 | 1 | [Frama-C]
Plug-in > jessie | major | resolved (Claude Marché) | 2011-10-28 | Jessie reports syntax error in .mlw file |
| | 0000999 | 1 | [Frama-C]
Kernel | minor | resolved (Virgile Prevosto) | 2011-10-27 | Missing or misleading warnings when merging two functions |
| | 0001001 | 2 | [Frama-C]
Plug-in > value analysis | major | resolved (Pascal Cuoq) | 2011-10-27 | Invalid handling of shift of pointer address |
| | 0001000 | 1 | [Frama-C]
Plug-in > value analysis | crash | resolved (Boris Yakobowski) | 2011-10-26 | Evaluation in the logic can cause crashes |
| | 0000990 | 1 | [Frama-C]
Kernel | crash | resolved (Virgile Prevosto) | 2011-10-20 | Crash with multiple incompatible declarations |
|  | 0000992 | 1 | [Frama-C]
Plug-in > wp | major | assigned (Loïc Correnson) | 2011-10-20 | Wrong WP computation when calling a function with behaviors (assigns problem ?) |
| | 0000672 | 2 | [Frama-C]
Kernel | crash | resolved (Virgile Prevosto) | 2011-10-20 | Incorrect cil merging in presence of ACSL annotations |
| | 0000991 | | [Frama-C]
Documentation | text | acknowledged (Julien Signoles) | 2011-10-20 | outdated manual titles |
| | 0000986 | 1 | [Frama-C]
Plug-in > wp | minor | resolved (Loïc Correnson) | 2011-10-17 | Wrong [\valid(p)] outside the pointed variable scope |
| | 0000945 | 1 | [Frama-C]
Plug-in > value analysis | minor | confirmed (Pascal Cuoq) | 2011-10-10 | Should warn for overlapping lv=lv; assignments |
| | 0000980 | | [Frama-C]
Kernel > ACSL implementation | feature | assigned (Virgile Prevosto) | 2011-10-06 | Functional expression in assigns properties |
| | 0000936 | 6 | [Frama-C]
Kernel | minor | acknowledged (Virgile Prevosto) | 2011-09-14 | Cil does not reject incorrect initializers |
| | 0000912 | 4 | [Frama-C]
Plug-in > functional dependencies | minor | assigned (Pascal Cuoq) | 2011-09-07 | Functional dependencies are incorrect in presence of value analysis builtins |
| | 0000932 | 1 | [Frama-C]
Kernel | tweak | confirmed (Julien Signoles) | 2011-08-23 | Journalisation of dynamic functions using abstract types does not work |
| | 0000923 | | [Frama-C]
Plug-in > jessie | major | assigned (Claude Marché) | 2011-08-12 | Jessie Plugin returns an error. Code with struct-statement, cannot be compiled. |
| | 0000922 | 1 | [Frama-C]
Plug-in > jessie | major | assigned (Claude Marché) | 2011-08-12 | Jessie Plugin returns an error. Code with struct-statement, cannot be compiled in a function by call by value. |
| | 0000903 | | [Frama-C]
Plug-in > wp | minor | assigned (Loïc Correnson) | 2011-07-29 | Support of \block_length |
| | 0000895 | | [Frama-C]
Plug-in > wp | minor | assigned (Loïc Correnson) | 2011-07-28 | Proof obligations of lemma properties |
| | 0000745 | 3 | [Frama-C]
Kernel > ACSL implementation | minor | assigned (Virgile Prevosto) | 2011-07-26 | Very big integer constants |
| | 0000794 | 1 | [Frama-C]
Plug-in > wp | feature | assigned (Loïc Correnson) | 2011-07-04 | initial value of strings |
| | 0000875 | 4 | [Frama-C]
Plug-in > value analysis | feature | feedback (Pascal Cuoq) | 2011-07-01 | suggest to issue a warning on (<)-comparisons between pointers, unless both are non-null |
| | 0000873 | | [Frama-C]
Plug-in > value analysis | feature | assigned (Pascal Cuoq) | 2011-06-28 | Alignment of global charachter arrays |
| | 0000856 | 4 | [Frama-C]
Plug-in > value analysis | crash | feedback (Pascal Cuoq) | 2011-06-14 | non-constant size of 2-dim array leads to crash (some similarities to issue 0000852) |
| | 0000862 | | [Frama-C]
Kernel > ACSL implementation | tweak | assigned (Virgile Prevosto) | 2011-06-10 | ACSL parser + pretty-printer |
| | 0000852 | 3 | [Frama-C]
Kernel | minor | assigned (Virgile Prevosto) | 2011-06-01 | non-constant size of 2-dim array causes error in recursive procedure |
| | 0000846 | | [Frama-C]
Plug-in > jessie | minor | assigned (Claude Marché) | 2011-05-30 | array access in "decreases"-clause causes "Unexpected internal region in logic" |
| | 0000816 | | [Frama-C]
Plug-in > wp | feature | assigned (Loïc Correnson) | 2011-05-27 | ACSL builtins |
| | 0000840 | | [Frama-C]
Kernel | text | assigned (Virgile Prevosto) | 2011-05-27 | syntax error message refers to (true error line + 5 lines) |
| | 0000834 | | [Frama-C]
Plug-in > jessie | minor | assigned (Claude Marché) | 2011-05-24 | Computation of regions for axioms in axiomatics |
| | 0000829 | 3 | [Frama-C]
Plug-in > jessie | minor | assigned (Claude Marché) | 2011-05-24 | alias between int* and uint* handled incorrectly |
|  | 0000251 | 2 | [Frama-C]
Plug-in > value analysis | minor | assigned (Pascal Cuoq) | 2011-05-16 | wrong origin displayed in the GUI |
| | 0000772 | 4 | [Frama-C]
Plug-in > value analysis | tweak | assigned (Pascal Cuoq) | 2011-05-14 | Incorrect location of warnings emitted by value analysis |
| | 0000813 | | [Frama-C]
Plug-in > jessie | minor | assigned (Claude Marché) | 2011-05-09 | struct dereferencing causes uncaught exception |
| | 0000811 | 2 | [Frama-C]
Plug-in > jessie | minor | assigned (Claude Marché) | 2011-05-06 | double struct dereferencing causes unbound variable error |
| | 0000750 | 4 | [Frama-C]
Kernel > ACSL implementation | feature | acknowledged (Virgile Prevosto) | 2011-03-11 | Several [invariant] at a program point |
| | 0000735 | | [Frama-C]
Kernel | minor | assigned (Virgile Prevosto) | 2011-02-22 | Pretty-printer and generated global annotations |
| | 0000734 | | [Frama-C]
Kernel | tweak | assigned (Loïc Correnson) | 2011-02-21 | Command.command_generic may raise Sys_error |
| | 0000722 | 2 | [Frama-C]
Kernel > ACSL implementation | minor | assigned (Virgile Prevosto) | 2011-02-14 | bitwise operator |
| | 0000713 | | [Frama-C]
Kernel > ACSL implementation | feature | assigned (Virgile Prevosto) | 2011-02-10 | Any number of ";" should be allowed in specifications |
| | 0000712 | | [Frama-C]
Plug-in > jessie | major | assigned (Claude Marché) | 2011-02-10 | Validity of valid pointer to struct member cannot be verified |
| | 0000667 | 3 | [Frama-C]
Plug-in > jessie | crash | assigned (Claude Marché) | 2011-01-25 | /usr/share/frama-c/libc/stdio.h:107:[jessie] failure: Unexpected exception. |
| | 0000685 | 1 | [Frama-C]
Kernel | feature | assigned (Virgile Prevosto) | 2011-01-24 | CIL's added return masks issues |
| | 0000676 | | [Frama-C]
Kernel | minor | assigned (Virgile Prevosto) | 2011-01-18 | Strange AST produced with unspecified side-effects involve function calls in expressions |
| | 0000670 | | [Frama-C]
Plug-in > jessie | minor | assigned (Claude Marché) | 2011-01-12 | In certain circumstances Jessie cannot analyse files that it generates |
| | 0000658 | | [Frama-C]
Plug-in > jessie | crash | assigned (Claude Marché) | 2010-12-29 | loop assigns crash |
| | 0000654 | | [Frama-C]
Plug-in > jessie | minor | assigned (Claude Marché) | 2010-12-25 | Incorrect translation (Unbound variable) |
| | 0000653 | | [Frama-C]
Plug-in > jessie | crash | assigned (Claude Marché) | 2010-12-25 | jessie's Unexpected failure |
| | 0000652 | | [Frama-C]
Plug-in > jessie | minor | assigned (Claude Marché) | 2010-12-24 | pointer arithmetic |
| | 0000651 | | [Frama-C]
Plug-in > jessie | minor | assigned (Claude Marché) | 2010-12-24 | array id "shift" |
| | 0000643 | 2 | [Frama-C]
Kernel > ACSL implementation | minor | assigned (Virgile Prevosto) | 2010-12-18 | Incorrect parsing of complex lemma |
| | 0000636 | 1 | [Frama-C]
Plug-in > jessie | crash | feedback (Claude Marché) | 2010-12-16 | Unexpected exception in block_length |
| | 0000601 | | [Frama-C]
Kernel > ACSL implementation | feature | assigned (Virgile Prevosto) | 2010-12-16 | no multiple assert-clauses accepted in /*@...*/-style comment |
| | 0000605 | 1 | [Frama-C]
Kernel > ACSL implementation | minor | assigned (Virgile Prevosto) | 2010-12-16 | Empty specification causes syntax error |
| | 0000632 | | [Frama-C]
Plug-in > jessie | feature | assigned (Claude Marché) | 2010-11-29 | Suggest to rename user identifiers to avoid name clashes in ..._why.sx files |
| | 0000617 | 2 | [Frama-C]
Plug-in > jessie | minor | confirmed (Claude Marché) | 2010-11-17 | assigns nothing ? |
| | 0000629 | 1 | [Frama-C]
Plug-in > jessie | minor | assigned (Claude Marché) | 2010-11-17 | Incorrect processing of "type var[]" constructions |
| | 0000628 | | [Frama-C]
Plug-in > jessie | minor | assigned (Claude Marché) | 2010-11-13 | Frama-C/Jessie does not recognize the length of array in struct |
| | 0000615 | 1 | [Frama-C]
Plug-in > jessie | major | assigned (Claude Marché) | 2010-10-22 | separately verified files show code-bug when linked together |
| | 0000614 | | [Frama-C]
Plug-in > jessie | minor | assigned (Claude Marché) | 2010-10-22 | "\valid(&aaa)" unprovable for global variable aaa - missing antecedens in proof obligation? |
| | 0000593 | 4 | [Frama-C]
Kernel | minor | confirmed (Virgile Prevosto) | 2010-10-01 | Parse error when using a wide string literal to initialize uint16 array |
| | 0000590 | | [Frama-C]
Plug-in > jessie | minor | assigned (Claude Marché) | 2010-09-22 | Jessie plugin does not support logic label Post in ensures clause |
| | 0000575 | 2 | [Frama-C]
Kernel > ACSL implementation | minor | assigned (Virgile Prevosto) | 2010-08-25 | set of set |
| | 0000544 | | [Frama-C]
Plug-in > jessie | feature | assigned (Claude Marché) | 2010-07-17 | Enhancement on assigns annotation and the name of proof obligation |
| | 0000102 | 1 | [Frama-C]
Plug-in > jessie | major | confirmed (Claude Marché) | 2010-07-13 | Jessie: struct field's validity |
| | 0000518 | | [Frama-C]
Plug-in > jessie | minor | assigned (Claude Marché) | 2010-06-22 | Loop assigns are not taken into account when proving a safety PO |
| | 0000502 | 2 | [Frama-C]
Plug-in > jessie | minor | assigned (Claude Marché) | 2010-06-13 | Unbound label in Jessie-generated Why file when using logic function in assigns clause |
| | 0000289 | 2 | [Frama-C]
Plug-in > jessie | major | acknowledged (Virgile Prevosto) | 2010-06-09 | unsoundness of Jessie with respect to expression evaluation of ANSI-C |
| | 0000485 | | [Frama-C]
Plug-in > jessie | feature | assigned (Claude Marché) | 2010-05-18 | Code containing consts should be verifiable |
| | 0000480 | | [Frama-C]
Plug-in > jessie | crash | assigned (Claude Marché) | 2010-05-12 | volatile annotation breaks type checker |
| | 0000444 | 2 | [Frama-C]
Kernel > ACSL implementation | minor | feedback (Virgile Prevosto) | 2010-05-11 | predicate definitions should be of type prop |
| | 0000249 | 2 | [Frama-C]
Kernel | minor | confirmed (Julien Signoles) | 2010-04-26 | dynamically link a library |
| | 0000456 | | [Frama-C]
Plug-in > jessie | minor | assigned (Claude Marché) | 2010-04-23 | Lack of parameter generation |
| | 0000433 | | [Frama-C]
Plug-in > jessie | tweak | assigned (Virgile Prevosto) | 2010-03-23 | different translation of casted constants in program-code and in assertion |
| | 0000424 | 3 | [Frama-C]
Plug-in > jessie | minor | assigned (Claude Marché) | 2010-03-22 | Uncaught exception: Failure("Unexpected internal region in logic") |
| | 0000416 | | [Frama-C]
Plug-in > jessie | minor | assigned (Claude Marché) | 2010-02-22 | local array decl with non-constant size causes Why error |
| | 0000072 | 1 | [Frama-C]
Plug-in > jessie | minor | assigned (Claude Marché) | 2010-02-12 | The specifications of statements are not translated |
| | 0000079 | 2 | [Frama-C]
Kernel > ACSL implementation | feature | assigned (Virgile Prevosto) | 2010-02-05 | Better support of //@ style |
| | 0000387 | | [Frama-C]
Kernel > ACSL implementation | feature | assigned (Virgile Prevosto) | 2010-02-05 | ghost integer ? |
| | 0000336 | 1 | [Frama-C]
Plug-in > jessie | major | assigned (Claude Marché) | 2010-01-22 | cast between homogenous struct and array |
| | 0000379 | | [Frama-C]
Plug-in > jessie | crash | assigned (Claude Marché) | 2010-01-21 | \separated |
| | 0000373 | | [Frama-C]
Plug-in > jessie | major | assigned (Claude Marché) | 2010-01-14 | Global invariants are not verified |
| | 0000348 | 1 | [Frama-C]
Plug-in > jessie | major | assigned (Claude Marché) | 2009-12-03 | Arithmetic safety of bitwise operators cannot be verified |
| | 0000039 | 1 | [Frama-C]
Plug-in > jessie | minor | confirmed (Claude Marché) | 2009-11-24 | Frama-C/Jessie: memory set problem |
| | 0000335 | | [Frama-C]
Plug-in > jessie | minor | assigned (Claude Marché) | 2009-11-20 | Unbound reference raised by Why |
| | 0000328 | | [Frama-C]
Plug-in > jessie | major | assigned (Claude Marché) | 2009-11-13 | assertion failed in Jessie with bitfields inside union |
| | 0000291 | | [Frama-C]
Plug-in > jessie | minor | assigned (Claude Marché) | 2009-10-20 | Unbound variable raised by why in presence of an unsafe cast |
| | 0000040 | | [Frama-C]
Plug-in > jessie | minor | confirmed (Claude Marché) | 2009-10-15 | Frama-C/Jessie: typing error |
| | 0000261 | 2 | [Frama-C]
Kernel | minor | acknowledged (Virgile Prevosto) | 2009-10-01 | Frama-C fails to parse a file |
| | 0000256 | | [Frama-C]
Plug-in > jessie | minor | assigned (Claude Marché) | 2009-09-25 | array range in requires predicate |
| | 0000025 | | [Frama-C]
Plug-in > jessie | minor | acknowledged (Virgile Prevosto) | 2009-09-21 | type invariants |
| | 0000239 | 1 | [Frama-C]
Plug-in > jessie | minor | assigned (Loïc Correnson) | 2009-09-14 | internal error when analyzing max.h |
| | 0000215 | | [Frama-C]
Plug-in > jessie | minor | assigned (Claude Marché) | 2009-08-25 | Mise en hypothèse de la précondition d'une opération appelée |
| | 0000185 | 1 | [Frama-C]
Plug-in > jessie | major | assigned (Claude Marché) | 2009-07-17 | Frama-C cannot process properly arrays of structures |
| | 0000178 | 1 | [Frama-C]
Plug-in > jessie | minor | confirmed (Claude Marché) | 2009-07-09 | type error in generated why file |
| | 0000092 | 1 | [Frama-C]
Plug-in > jessie | minor | assigned (Claude Marché) | 2009-06-19 | Why error with logic functions returning a pointer |
| | 0000042 | 2 | [Frama-C]
Plug-in > jessie | feature | assigned (Claude Marché) | 2009-06-17 | Default invariant should be inferred for loops |
| | 0000031 | | [Frama-C]
Plug-in > jessie | minor | acknowledged (Claude Marché) | 2009-06-17 | Why- error :-jessie-no-regions and assigns does not work |
| | 0000032 | | [Frama-C]
Plug-in > jessie | minor | assigned (Claude Marché) | 2009-04-10 | Internal error with assign specification on bi-dimensional arrays |
| | 0000038 | | [Frama-C]
Plug-in > jessie | minor | assigned (Claude Marché) | 2009-04-10 | Jessie crashes on simple program without annotations |