|
Viewing Issues (1 - 50 / 172)
[ Print Reports ] [ CSV Export ]
|
[ First Prev 1 2 3 4 Next Last ]
|
| | | P | ID | # | Category | Severity | Status | Updated | Summary |
|
| | | | 0001082 | | [Frama-C]
Kernel > Makefile | trivial | assigned (signoles) | 2012-02-06 | Bad links in generated documentation modules.svg |
| | | | 0001081 | 2 | [Frama-C]
Kernel | minor | new | 2012-02-06 | foo ? (void)x : (signed char)y (csmithreduction) |
| | | | 0001079 | 3 | [Frama-C]
Plug-in > scope | feature | resolved (yakobowski) | 2012-02-04 | Imprecision of 'Defs' when querying precise location |
| | | | 0001073 | 2 | [Frama-C]
Kernel | major | assigned (virgile) | 2012-02-03 | Some functions lose their formals after File.create_project_from_visitor |
| | | | 0001014 | 1 | [Frama-C]
Documentation | minor | confirmed (signoles) | 2012-02-02 | gui and doc |
| | | | 0000765 | 4 | [Frama-C]
Plug-in > wp | minor | assigned (correnson) | 2012-01-31 | Post-state of statement spec |
| | | | 0001076 | 2 | [Frama-C]
Plug-in > value analysis | minor | assigned (pascal) | 2012-01-31 | "volatile" ignored |
| | | | 0001074 | 5 | [Frama-C]
Plug-in > value analysis | major | resolved (pascal) | 2012-01-30 | Imprecise result on almost deterministic program |
| | | | 0000624 | 3 | [Frama-C]
Kernel | crash | acknowledged (correnson) | 2012-01-30 | Logging huge messages makes kernel crashing |
| | | | 0000989 | 2 | [Frama-C]
Plug-in > syntactic callgraph | minor | resolved (signoles) | 2012-01-27 | Strange dot callgraphs |
| | | | 0001071 | 5 | [Frama-C]
Plug-in > value analysis | tweak | resolved (pascal) | 2012-01-27 | relation chains exploited incompletely |
| | | | 0001072 | 3 | [Frama-C]
Plug-in > value analysis | feature | resolved (yakobowski) | 2012-01-27 | evaluation of && and || in term position |
| | | | 0001036 | 2 | [Frama-C]
Documentation | feature | confirmed (signoles) | 2012-01-27 | In section 5.11.5 of the Plugin developper manual : Reference to modules that neither appear in the API nor in Frama-c source. |
| | | | 0001067 | 5 | [Frama-C]
Documentation | trivial | resolved (pascal) | 2012-01-26 | suggest to mention option "-value-help" in value analysis manual |
| | | | 0001070 | | [Frama-C]
Kernel > configure | feature | assigned (virgile) | 2012-01-23 | Getting frama-c version through --enable-external |
| | | | 0001069 | | [Frama-C]
Kernel > configure | minor | assigned (virgile) | 2012-01-23 | Handling error in external plug-in through --enable-external |
| | | | 0000252 | | [Frama-C]
Plug-in > jessie | feature | assigned (virgile) | 2012-01-21 | type invariants |
| | | | 0001066 | 2 | [Frama-C]
Plug-in > value analysis | trivial | resolved (pascal) | 2012-01-19 | suggest to use "NULL" rather than "&NULL" for null pointer |
| | | | 0001025 | 12 | [Frama-C]
Kernel | minor | assigned (yakobowski) | 2012-01-18 | Unsound lexing position --Cil_types.location-- given as argument of the Skip(loc) -- type : Cil_types.instr, in the Carbon-2011 |
| | | | 0000107 | 6 | [Frama-C]
Plug-in > slicing | major | assigned (yakobowski) | 2012-01-18 | Slicer: slicing preserving some undesired function calls |
| | | | 0001062 | | [Frama-C]
Plug-in > jessie | major | assigned (cmarche) | 2012-01-12 | Jessie incorrectly handles initialization of static array with {} initialization |
| | | | 0001061 | | [Frama-C]
Plug-in > jessie | minor | assigned (cmarche) | 2012-01-12 | Jessie incorrectly handles initialization of array |
| | | | 0001060 | | [Frama-C]
Plug-in > wp | crash | assigned (correnson) | 2012-01-11 | WP 0.5 crashes with an Unbound label parameter 'Here' |
| | | | 0001059 | 1 | [Frama-C]
Kernel | major | assigned (virgile) | 2012-01-08 | Undefined behavior with embedded assignment goes undetected |
| | | | 0001056 | 2 | [Frama-C]
Kernel > ACSL implementation | crash | resolved (virgile) | 2012-01-06 | Frama-c fails when Starting Jessie Translation |
| | | | 0001027 | 2 | [Frama-C]
Kernel > ACSL implementation | crash | resolved (virgile) | 2012-01-06 | incompatible types for a correct spec |
| | | | 0001058 | | [Frama-C]
Plug-in > jessie | minor | assigned (cmarche) | 2012-01-04 | Jessie incorrectly handles labels |
| | | | 0001050 | 2 | [Frama-C]
Plug-in > aoraï | minor | resolved (virgile) | 2012-01-04 | Sequence number generated by aorai is incorrect |
| | | | 0001053 | 1 | [Frama-C]
Kernel | minor | assigned (administrator) | 2011-12-22 | Frama-C for Windows |
| | | | 0001051 | 1 | [Frama-C]
Plug-in > wp | text | assigned (correnson) | 2011-12-16 | suspicious axiomatization of included,zrange,zunion in .sx file |
| | | | 0001034 | 13 | [Frama-C]
Kernel > Makefile | minor | feedback (signoles) | 2011-12-14 | the make errors |
| | | | 0001047 | | [Frama-C]
Plug-in > jessie | major | assigned (cmarche) | 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 (cmarche) | 2011-12-11 | Wrong sequence of lemmas |
| | | | 0001044 | | [Frama-C]
Plug-in > value analysis | feature | assigned (pascal) | 2011-12-11 | Smarter access to array of struct of array |
| | | | 0001038 | | [Frama-C]
Plug-in > wp | text | assigned (correnson) | 2011-12-05 | lemma tacitly ignored in absense of C code |
| | | | 0001028 | 3 | [Frama-C]
Plug-in > wp | minor | acknowledged (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 (correnson) | 2011-12-01 | undefined (or built-in?) predicate "global" in proof obligation |
| | | | 0001033 | | [Frama-C]
Plug-in > jessie | feature | assigned (cmarche) | 2011-11-29 | Feature request (Jessie): \fresh (and \separated) |
| | | | 0001032 | | [Frama-C]
Plug-in > jessie | feature | assigned (cmarche) | 2011-11-29 | assigns nothing is not possible to proof, if malloc is not in a same function |
| | | | 0001026 | | [Frama-C]
Plug-in > value analysis | major | assigned (pascal) | 2011-11-25 | value analysis memory consumption problem when using -lib-entry option |
| | | | 0001024 | 9 | [Frama-C]
Plug-in > value analysis | major | assigned (yakobowski) | 2011-11-21 | Emitted assertion wrongly reduces to bottom (apparently) (csmith) |
| | | | 0000997 | 7 | [Frama-C]
Plug-in > value analysis | minor | resolved (yakobowski) | 2011-11-21 | Warnings in presence of Top floats |
| | | | 0001021 | 2 | [Frama-C]
Graphical User Interface | minor | resolved (yakobowski) | 2011-11-18 | request for pretty printing only one property by lines |
| | | | 0001022 | | [Frama-C]
Documentation | text | assigned (virgile) | 2011-11-18 | suggest to explain semantics of missing loop assigns clause in Acsl manual |
| | | | 0001023 | 1 | [Frama-C]
Documentation | text | assigned (virgile) | 2011-11-18 | \valid_range not mentioned in Acsl manual |
| | | | 0001003 | 6 | [Frama-C]
Plug-in > jessie | tweak | feedback (cmarche) | 2011-11-18 | conditional expression (?:) raises uncaught exception under why-2.30 |
| | | | 0001019 | 1 | [Frama-C]
Kernel > ACSL implementation | minor | resolved (virgile) | 2011-11-16 | #defined variable unrecognized in assigns, except in parentheses |
| | | | 0001008 | 2 | [Frama-C]
Plug-in > jessie | feature | assigned (cmarche) | 2011-11-16 | suggest to supply lower-bound for constant_too_large_2147483647 to Simplify |
| | | | 0001013 | 7 | [Frama-C]
Kernel | crash | resolved (yakobowski) | 2011-11-14 | Crash when casting something to type void |
| | | | 0001017 | 3 | [Frama-C]
Kernel > ACSL implementation | feature | assigned (virgile) | 2011-11-14 | suggest to warn about ensures clauses containing only \old variables |
|
|
[ First Prev 1 2 3 4 Next Last ]
|
