Change Log - Frama-C Bug Tracking System

Frama-C - Change Log
Frama-C - Frama-C Boron-20100401 (Released 2010-04-13) [ View Issues ] ====================================================== - 0000435: [Plug-in > callgraph] Too many edges in call graph (signoles) - closed. - 0000314: [Plug-in > Eva] malloc.h can't be preprocessed: __func__ is not a macro (pascal) - closed. - 0000310: [Kernel] Be careful when activating warnings. (signoles) - closed. - 0000338: [Plug-in > jessie] free() should permit 0 as valid argument (cmarche) - closed. - 0000374: [Graphical User Interface] "-cpp-command ..." parameter lost (signoles) - closed. - 0000388: [Plug-in > Eva] Incorrect 'assert false' in value analysis (monate) - closed. - 0000406: [Plug-in > jessie] assert false (* TODO *) (cmarche) - closed. - 0000381: [Plug-in > Eva] propagation of \result clauses (pascal) - closed. - 0000245: [Kernel] Blocks are removed from the AST (virgile) - closed. - 0000186: [Plug-in > slicing] Stack overflow when slicing functions invoking themselves circularily (Anne) - closed. - 0000257: [Kernel] get_varinfo not exported in src/ai/base.mli (pascal) - closed. - 0000305: [Kernel > configure] After ./confugure with --disable-all-staff options, make holds (signoles) - closed. - 0000329: [Kernel > ACSL implementation] Float promoted to double (cmarche) - closed. - 0000342: [Kernel > ACSL implementation] Assertion failed instead of typing error report (virgile) - closed. - 0000366: [Plug-in > jessie] Unicode minus sign (U+2212) not accepted by Jessie, yet used in documentation, causing mysterious failure (monate) - closed. - 0000346: [Documentation > ACSL] Example 2.31 of ACSL 1.4 (Beryllium implementation) incorrect (virgile) - closed. - 0000272: [Plug-in > jessie] complete behaviors; disjoint behaviors; (virgile) - closed. - 0000213: [Kernel] crash in parser when double definition of variable in two different files, in some order (virgile) - closed. - 0000325: [Plug-in > Eva] Precise widening when a loop condition involves a char or short (pascal) - closed. - 0000398: [Kernel > configure] RTE compiled even with ./configure --disable-rte (signoles) - closed. - 0000361: [Plug-in > jessie] "why" reports "unbound label" (cmarche) - closed. - 0000370: [Plug-in > jessie] pragma JessieIntegerModel (cmarche) - closed. - 0000367: [Plug-in > jessie] bug with constants like 1E-6 (cmarche) - closed. - 0000399: [Plug-in > jessie] Statement contract and "hiding" of statement (cmarche) - closed. - 0000386: [Plug-in > jessie] int32 and real can't be unified (cmarche) - closed. - 0000443: [Plug-in > jessie] assigns clause unchecked on arrays (cmarche) - closed. - 0000391: [Plug-in > jessie] Why keywords as ACSL identifiers (cmarche) - closed. - 0000420: [Plug-in > jessie] same formula translated differently as axiom/lemma (cmarche) - closed. - 0000332: [Kernel] goto generated by Frama-C and not supported by Jessie (virgile) - closed. - 0000393: [Plug-in > slicing] assigns clauses are missing from the sliced program (Anne) - closed. - 0000385: [Kernel] File "src/kernel/cilE.ml", line 372, characters 13-19: Assertion failed (virgile) - closed. - 0000358: [Kernel > ACSL implementation] redeclaration as different kind of symbol (yakobowski) - closed. - 0000364: [Plug-in > jessie] complete/disjoint behaviors shouldn't accept undefined behaviors (virgile) - closed. - 0000372: [Plug-in > Eva] Wrong postconditions are "valid according to value analysis" (virgile) - closed. - 0000327: [Kernel > ACSL implementation] order of 'decreases' and 'behavior' clauses (virgile) - closed. - 0000311: [Kernel] switch and case expressions must be integer (virgile) - closed. - 0000382: [Kernel > Makefile] Should not call install-kernel-opt on bytecode architectures (signoles) - closed. - 0000431: [Kernel] Dgraph.DGraphModel.read_dot (signoles) - closed. - 0000414: [Plug-in > Eva] imprecision in widening/narrowing for char and short index (pascal) - closed. - 0000309: [Kernel > ACSL implementation] After ./confugure with --disable-all-staff options and make static, frama-c-Myplugin.byte crashes (virgile) - closed. - 0000392: [Plug-in > Eva] Failure("Function 'From.find_deps_no_transitivity' not registered yet") (pascal) - closed. - 0000376: [Plug-in > jessie] unsigned long long constant becomes signed (cmarche) - closed. [42 issues]