Frama-C Bug Tracking System

Frama-C - Change Log

Frama-C - Frama-C Oxygen-20120901 (Released 2012-09-19) View Issues ]
=======================================================
- 0000989: [Plug-in > callgraph] Strange dot callgraphs (signoles) - closed.
- 0001014: [Documentation] gui and doc (signoles) - closed.
- 0001085: [Documentation] Cute boolean options too cute for their own good (signoles) - closed.
- 0001036: [Documentation > manuals] In section 5.11.5 of the Plugin developper manual : Reference to modules that neither appear in the API nor in Frama-c source. (signoles) - closed.
- 0001089: [Documentation > manuals] Updated example in plugin-development-guide (signoles) - closed.
- 0001088: [Documentation > manuals] Plugin-development-guide section 2.1.2 (signoles) - closed.
- 0000419: [Documentation > manuals] Plug-in dev guide: tutorial for kernel integrated plug-in is out-of-date (signoles) - closed.
- 0000991: [Documentation > manuals] outdated manual titles (virgile) - closed.
- 0001067: [Documentation > manuals] suggest to mention option "-value-help" in value analysis manual (pascal) - closed.
- 0001092: [Documentation > manuals] some typos etc. in the value-analysis manual (pascal) - closed.
- 0000745: [Kernel > ACSL implementation] Very big integer constants (virgile) - closed.
- 0001072: [Plug-in > Eva] evaluation of && and || in term position (yakobowski) - closed.
- 0000759: [Plug-in > Eva] wrong treatment for const arrays in lib-entry mode (pascal) - closed.
- 0001073: [Kernel] Some functions lose their formals after File.create_project_from_visitor (virgile) - closed.
- 0001099: [Kernel] Crash when parsing an incorrect program with pointer to arrays (virgile) - closed.
- 0001100: [Kernel] Loop unrolling sub-optimal in presence of some labels (yakobowski) - closed.
- 0000986: [Plug-in > wp] Wrong [\valid(p)] outside the pointed variable scope (correnson) - closed.
- 0001069: [Kernel > configure] Handling error in external plug-in through --enable-external (virgile) - closed.
- 0000990: [Kernel] Crash with multiple incompatible declarations (virgile) - closed.
- 0001023: [Documentation > ACSL] \valid_range not mentioned in Acsl manual (virgile) - closed.
- 0000999: [Kernel] Missing or misleading warnings when merging two functions (virgile) - closed.
- 0000993: [Plug-in > from] Incorrect dependencies in presence of declared functions (yakobowski) - closed.
- 0001009: [Kernel > ACSL implementation] code annotation placed above a local declaration are not correctly handled (virgile) - closed.
- 0001006: [Kernel] Kernel should desugar "complete behaviors" (virgile) - closed.
- 0001132: [Kernel] -cpp-extra-args option should be a list (signoles) - closed.
- 0001135: [Kernel] unrolling loop statements with labels into there annotations are not handled correctly (in conjunction with -ulevel) (patrick) - closed.
- 0001114: [Kernel] 17514, -unspecified-access and if (*p = (*p < 3)) (csmith) (virgile) - closed.
- 0001113: [Kernel] Preprocessing code may yield expanded code with undeclared variables (virgile) - closed.
- 0001126: [Kernel] AST check failure : problem with generated block-local variables (virgile) - closed.
- 0001136: [Kernel] [Globals.Vars.get_astinfo] doesn't work (virgile) - closed.
- 0001116: [Kernel] axiom outside axiomatic tacitly ignored in presence of struct (virgile) - closed.
- 0001139: [Kernel] unrolling labeled loops (patrick) - closed.
- 0001142: [Plug-in > Eva] Bad AST generation ? (yakobowski) - closed.
- 0001144: [Kernel] 17944 using option -unspecified-access, no alarm for x + (x=0) (virgile) - closed.
- 0001145: [Kernel > Makefile] PLUGIN_LINK_GUI_OFLAGS not used ? (signoles) - closed.
- 0001024: [Plug-in > Eva] Emitted assertion wrongly reduces to bottom (apparently) (csmith) (yakobowski) - closed.
- 0001110: [Kernel] Using Filter without Value (yakobowski) - closed.
- 0001165: [Kernel] [libc] erreur: #endif sans #if (virgile) - closed.
- 0001050: [Plug-in > aoraï] Sequence number generated by aorai is incorrect (virgile) - closed.
- 0001027: [Kernel > ACSL implementation] incompatible types for a correct spec (virgile) - closed.
- 0001056: [Kernel > ACSL implementation] Frama-c fails when Starting Jessie Translation (virgile) - closed.
- 0001066: [Plug-in > Eva] suggest to use "NULL" rather than "&NULL" for null pointer (pascal) - closed.
- 0001082: [Kernel > Makefile] Bad links in generated documentation modules.svg (signoles) - closed.
- 0001079: [Plug-in > scope] Imprecision of 'Defs' when querying precise location (yakobowski) - closed.
- 0001025: [Kernel] Cil.prepareCfg (or -simplify-cfg option) insert dummy locations in the ast (yakobowski) - closed.
- 0001071: [Plug-in > Eva] relation chains exploited incompletely (pascal) - closed.
- 0000107: [Plug-in > slicing] Slicer: slicing preserving some undesired function calls (yakobowski) - closed.
- 0000251: [Plug-in > Eva] wrong origin displayed in the GUI (yakobowski) - closed.
- 0000728: [Kernel] Arguments are not checked when function call precedes function declaration (yakobowski) - closed.
- 0001214: [Plug-in > Eva] FRAMA_C_MALLOC_INFINITE not used in stdlib.c (yakobowski) - closed.
- 0000840: [Kernel] syntax error message refers to (true error line + 5 lines) (virgile) - closed.
- 0001226: [Kernel] error with -pp-annot : eof while parsing C comment (virgile) - closed.
- 0001122: [Graphical User Interface] Opening consolidation graph crashes when 'dot' is missing (signoles) - closed.
- 0000932: [Kernel] Journalisation of dynamic functions using abstract types does not work (signoles) - closed.
- 0001254: [Kernel] Documentation for Cil.d_plaininit (signoles) - closed.
- 0001059: [Kernel] Undefined behavior with embedded assignment goes undetected (virgile) - closed.
- 0001104: [Graphical User Interface] value analysis warning disappears from 'Messages' window in gui after 'Reparse' button clicked (yakobowski) - closed.
- 0001070: [Kernel > configure] Getting frama-c version through --enable-external (virgile) - closed.
- 0001000: [Plug-in > Eva] Evaluation in the logic can cause crashes (yakobowski) - closed.
- 0000679: [Plug-in > slicing] untypable ACSL in a sliced program containing \at(p,label) when the label was removed (Anne) - closed.
- 0000888: [Kernel] 14292: warn for unspecified side-effect that are separated by a function call (csmith) (virgile) - closed.
- 0001140: [Kernel] Strange declaration mismatch (monate) - closed.
- 0001261: [Plug-in > wp] Modules defined twice during WP compilation. (correnson) - closed.
- 0001128: [Kernel > Makefile] Install frama-c.top (signoles) - closed.
- 0001274: [Kernel] Things get mixed-up between project (yakobowski) - closed.
- 0000239: [Plug-in > jessie] internal error when analyzing max.h (correnson) - closed.
- 0001265: [Plug-in > jessie] Function with name shift produces error (virgile) - closed.
- 0001158: [Plug-in > jessie] inlining of assembleur is not supported (cmarche) - closed.
- 0001251: [Plug-in > jessie] Binary search doesn't verify anymore after upgrade (cmarche) - closed.
- 0001004: [Plug-in > jessie] Jessie reports syntax error in .mlw file (cmarche) - closed.
- 0001003: [Plug-in > jessie] conditional expression (?:) raises uncaught exception under why-2.30 (cmarche) - closed.
- 0001149: [Plug-in > jessie] function names are restricted due to exclusion of ACSL keywords (virgile) - closed.
- 0001182: [Graphical User Interface] Project menu is empty when Ubuntu/Unity is enabled (monate) - closed.
- 0001117: [Plug-in > wp] addr_eq versus = and <> in generated axioms access_update, access_update_neq (pherrmann) - closed.
- 0000594: [Kernel] Kernel error with RTE generated annotations: invalid operands (bitwise) (virgile) - closed.
- 0000384: [Kernel] Labels in loops are not unrolled (virgile) - closed.
- 0000685: [Kernel] CIL's added return masks issues (virgile) - closed.
- 0000672: [Kernel] Incorrect cil merging in presence of ACSL annotations (virgile) - closed.
- 0000895: [Plug-in > wp] Proof obligations of lemma properties (correnson) - closed.
- 0000764: [Kernel] Specifying several directories in environment variables FRAMAC_* (signoles) - closed.
- 0001001: [Plug-in > Eva] Invalid handling of shift of pointer address (pascal) - closed.
- 0001005: [Kernel] defining two axioms with same name causes kernel crash (virgile) - closed.
- 0000997: [Plug-in > Eva] Warnings in presence of Top floats (yakobowski) - closed.
- 0001013: [Kernel] Crash when casting something to type void (yakobowski) - closed.
- 0001021: [Graphical User Interface] request for pretty printing only one property by lines (yakobowski) - closed.
- 0001026: [Plug-in > Eva] value analysis memory consumption problem when using -lib-entry option (yakobowski) - closed.
- 0001028: [Plug-in > wp] unable to prove that comparison-result is 0 or 1: insufficient axiomatization of eq_int_bool? (correnson) - closed.
- 0001074: [Plug-in > Eva] Imprecise result on almost deterministic program (pascal) - closed.
- 0001081: [Kernel] foo ? (void)x : (signed char)y (csmithreduction) (virgile) - closed.
- 0001076: [Plug-in > Eva] "volatile" ignored (pascal) - closed.
- 0001083: [Plug-in > RTE] RTE does not check for downcast of unsigned integer (pherrmann) - closed.
- 0001108: [Plug-in > wp] Bitwise Operators (correnson) - closed.
- 0001102: [Graphical User Interface] Rename frama-c-gui.config (monate) - closed.
- 0001141: [Kernel] incorrect UINT8_MAX (and others) (monate) - closed.
- 0001162: [Kernel > ACSL implementation] "for" clause is refused (virgile) - closed.
- 0001180: [Kernel] Port to OCamlgraph 1.8.2 (signoles) - closed.
- 0001194: [Plug-in > scope] imprecision in PDG when unreachable statements (yakobowski) - closed.
- 0001225: [Plug-in > wp] Upgrading WP causes crash in Jessie (signoles) - closed.
- 0001243: [Kernel] two axioms with same name cause crash (yakobowski) - closed.
- 0001263: [Kernel] Identical lvals not equal in Cil_datatype.Lval.Hashtbl (virgile) - closed.
- 0001273: [Kernel] Parser does not complain about superfluous } (virgile) - closed.

[101 issues]


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker