Frama-C Bug Tracking System

Frama-C - Change Log

Frama-C - Frama-C Nitrogen-20111001 (Released 2011-10-10) View Issues ]
=========================================================
- 0000757: [Documentation] mismatch between configure check and INSTALL requirements for ocamlgraph version (signoles) - closed.
- 0000884: [Documentation > manuals] wrong figure reference in plugin development guide (signoles) - closed.
- 0000821: [Documentation > manuals] Wrong module name for the function prepareCFG and computeCFGInfo in the Frama-C Carbon html API. (signoles) - closed.
- 0000744: [Kernel > ACSL implementation] Too much type promotion for terms (virgile) - closed.
- 0000616: [Kernel] Comments parsing (monate) - closed.
- 0000717: [Plug-in > Eva] possible unsoundness bug (pascal) - closed.
- 0000718: [Plug-in > Eva] possible unsoundness in r11866 (pascal) - closed.
- 0000714: [Kernel > ACSL implementation] Lexing of ACSL characters (patrick) - closed.
- 0000725: [Kernel] passing (C && c) as argument to a function that expects int (csmith) (virgile) - closed.
- 0000723: [Graphical User Interface] r11920: Analyses -> Show callgraph requires a main function (signoles) - closed.
- 0000736: [ptests] the input file should be the first argument to ptests (virgile) - closed.
- 0000732: [Plug-in > Eva] Incorrect states passed to value analysis callbacks in presence of slevel (pascal) - closed.
- 0000727: [Kernel] Function specification not exposed through vspec visitor method (virgile) - closed.
- 0000720: [Kernel] Incorrect handling of nearly-empty switch clauses with -simplify-cfg (virgile) - closed.
- 0000721: [Plug-in > Eva] Unsoundness in value analysis when bitfield initializer exceeds range (csmith) (pascal) - closed.
- 0000752: [Plug-in > Eva] Unexpected error (Ival.Float_abstract.Bottom) (pascal) - closed.
- 0000754: [Kernel > Makefile] Dynamic plugin doc (virgile) - closed.
- 0000774: [Plug-in > slicing] Slicing is sometimes not journalisable anymore (signoles) - closed.
- 0000689: [Plug-in > Eva] Value may be incorrect in presence of several ensures (monate) - closed.
- 0000775: [Kernel] Hex/octal signed constants can be represented in an unsigned extended integer type (csmith) (monate) - closed.
- 0000770: [Kernel] r12430, some assertions are localized at Cabs2cil_start:0 (csmith) (virgile) - closed.
- 0000786: [Plug-in > slicing] 12816: Missing label in sliced program (csmith) (Anne) - closed.
- 0000784: [Plug-in > metrics] Generating metrics.html on demand (monate) - closed.
- 0000781: [Plug-in > from] Sliced program computes value different from original (csmith) (pascal) - closed.
- 0000729: [Kernel] Plugin.is_invisible is not see-through enough (signoles) - closed.
- 0000790: [Kernel > ACSL implementation] integrity problem of the AST on calls to functions with __attribute__ ((noreturn)) (virgile) - closed.
- 0000761: [Kernel > ACSL implementation] typing rule of \old(tab) or tab[index] construct (virgile) - closed.
- 0000798: [Plug-in > Eva] Serial conversions in function result (csmith) (pascal) - closed.
- 0000785: [Kernel] 12799, doubtful choice of promotion x86_64 mode (csmith) (pascal) - closed.
- 0000807: [Plug-in > slicing] sliced program does not terminate (csmith) (Anne) - closed.
- 0000810: [Kernel] pretty-printed program rejected by GCC. Affects -print, slicing, scf (csmith) (monate) - closed.
- 0000719: [Kernel] unsoundness due to packed structs (monate) - closed.
- 0000691: [Kernel > ACSL implementation] Comments parsing not always work (virgile) - closed.
- 0000655: [Kernel > ACSL implementation] using real function ( \max, \min, \abs ) instead of integer one in function contract (virgile) - closed.
- 0000817: [Kernel] r13378, assertion failed with bit-fields (monate) - closed.
- 0000819: [Plug-in > Eva] wrong interpretation when a bit-field receives the result of a function (csmith) (pascal) - closed.
- 0000808: [Plug-in > slicing] r13089 sliced program computes differently from original (csmith) (Anne) - closed.
- 0000823: [Kernel] r13417 unsigned bit-fields of width 32 should be promoted to unsigned int (csmith) (monate) - closed.
- 0000825: [Plug-in > slicing] r13465, crash in slicing (csmith) (Anne) - closed.
- 0000832: [Kernel] r13586 Spurious "assert \separated(...)" (csmith) (virgile) - closed.
- 0000771: [Kernel] r12436, unnecessary warning for side-effects (csmith) (virgile) - closed.
- 0000858: [Plug-in > semantic constant folding] emitted program computes differently from original (csmith) (monate) - closed.
- 0000857: [Kernel] Ocaml 32 bits version 3.11.0 (patrick) - closed.
- 0000861: [Kernel] Incorrect loop unrolling in presence of switch (yakobowski) - closed.
- 0000827: [Plug-in > slicing] sliced program computes differently from original (csmith) (Anne) - closed.
- 0000859: [Kernel > ACSL implementation] ACSL pretty-printer (virgile) - closed.
- 0000751: [Kernel > ACSL implementation] Promotion from integer to boolean (virgile) - closed.
- 0000882: [Kernel] Cil generates incorrect switch (with missing cases) (yakobowski) - closed.
- 0000883: [Plug-in > Eva] Crash du builtin memcpy, par une exception non rattrapable (yakobowski) - closed.
- 0000885: [Kernel > ACSL implementation] Typing error on expression array == pointer (virgile) - closed.
- 0000890: [Plug-in > Eva] Results differ between value analysis and GCC on bitfields (pascal) - closed.
 - 0000871: [Plug-in > semantic constant folding] scfed program behaves differently from original (monate) - closed.
- 0000889: [Plug-in > Eva] File "src/memory_state/lmap.ml", line 931, characters 22-28: Assertion failed (pascal) - closed.
- 0000897: [Plug-in > slicing] error: label ‘__invalid_label’ used but not defined (csmith) (Anne) - closed.
- 0000896: [Plug-in > wp] Warning for Axiom: From wp: Overloaded operator User defined axiom (correnson) - closed.
- 0000911: [Kernel] incorrect AST generated (yakobowski) - closed.
- 0000892: [Kernel] Cil wrongly authorizes references to local variables in static arrays (monate) - closed.
- 0000835: [Kernel > ACSL implementation] Aggregate logic types containing only C types (virgile) - closed.
- 0000947: [Plug-in > sparecode] -sparecode-analysis option should have -sparecode alias (monate) - closed.
- 0000946: [Plug-in > semantic constant folding] -semantic-const-folding should have a -semantic-constant-folding alias (monate) - closed.
- 0000933: [Kernel] Wrong AST (csmith) (pascal) - closed.
- 0000963: [Plug-in > slicing] Sliced program computes differently from original (csmith) (Anne) - closed.
- 0000954: [Plug-in > metrics] failure: bad initialisation: Too many initializations of the AST (virgile) - closed.
- 0000979: [Plug-in > wp] Unexpected label Old in pre : ignored annotation (Anne) - closed.
- 0000517: [Graphical User Interface] Exception raised if dot not found (monate) - closed.
- 0000576: [Plug-in > wp] axiom ignored because of label, but no label is present in axiom. (Anne) - closed.
- 0000730: [Plug-in > Eva] Print addresses in hexadecimal (pascal) - closed.
- 0000716: [Kernel] crash from r11865 (virgile) - closed.
- 0000724: [Graphical User Interface] Selection of [loop variant] properties in GUI (monate) - closed.
- 0000769: [Kernel] _ not supported as member name in struct (virgile) - closed.
- 0000780: [Plug-in > slicing] r12793: slicing generates uncompilable code (sliced function called with too few arguments) (csmith) (virgile) - closed.
- 0000787: [Plug-in > slicing] same conditions as 786, sliced program does not terminate when original does (csmith) (Anne) - closed.
 - 0000789: [Plug-in > slicing] 12825, sliced program does not terminate (Anne) - closed.
- 0000788: [Plug-in > wp] initializer completion (dargaye) - closed.
- 0000791: [Plug-in > Eva] Cash in value analysis of sliced project (pascal) - closed.
- 0000709: [Plug-in > slicing] Bug in slicing -- required C-statements getting knocked off from sliced code (Anne) - closed.
- 0000968: [Plug-in > Eva] Slicing generates empty program (csmith) (yakobowski) - closed.
- 0000927: [Plug-in > sparecode] Sparecode could eliminate unnecessary if statements (Anne) - closed.
- 0001464: [Graphical User Interface] "src/project/project.ml", line 678 Assertion failed - closed.
- 0000735: [Kernel] Pretty-printer and generated global annotations (virgile) - closed.
- 0000877: [Plug-in > RTE] RTE does not generate assertions for non initialized arguments (pherrmann) - closed.
- 0000905: [Plug-in > slicing] 14403: last slicing bug (csmith) (Anne) - closed.
- 0000880: [Plug-in > slicing] 14055: sliced program does not terminate (csmith) (Anne) - closed.
- 0000969: [Kernel] Sliced program computes differently from original (csmith) (pascal) - closed.
- 0001041: [Kernel] #pragma diag_suppress 1107 causes syntax error (pascal) - closed.
- 0000024: [Plug-in > jessie] Ordering of lemma in coq output of jessie (cmarche) - closed.
- 0000814: [Plug-in > jessie] memory blocks: pointer assignment and equality treated differently (cmarche) - closed.
- 0000926: [Plug-in > wp] wp-plugin does not generate coq *.v goals. (correnson) - closed.
- 0000913: [Plug-in > Eva] Improve Db.Properties.Interp.loc_to_loc (yakobowski) - closed.
- 0000925: [Plug-in > wp] Wp rises an error in if you use struct and long long type, with wp-rte option (correnson) - closed.
- 0000949: [Plug-in > Eva] Valid access to literal w_chart string address considered invalid (pascal) - closed.
- 0000961: [Kernel] Cil incorrectly cast arguments to switch to int (virgile) - closed.
- 0000966: [Kernel] bad default assigns generation (virgile) - closed.
- 0000522: [Kernel] size of long array can't be represented with OCaml int (virgile) - closed.
- 0000674: [Plug-in > jessie] Crash (cmarche) - closed.
- 0000641: [Plug-in > wp] alt-ergo version managment (dargaye) - closed.
- 0000680: [Plug-in > Eva] Use of Cabs2cil.fresh_global (pascal) - closed.
- 0000715: [Plug-in > Eva] crash bug in r11859 (pascal) - closed.
- 0000737: [Kernel] frama-c always crashes when I install new plugins (signoles) - closed.
- 0000762: [Kernel] unsigned constants truncated (csmith) (virgile) - closed.
- 0000758: [Plug-in > sparecode] Sparecode removes definitions which should be kept. (Anne) - closed.
- 0000768: [Plug-in > impact analysis] Impact analysis does not catch Pdg.Top (returned on variadic calls) (signoles) - closed.
- 0000779: [Plug-in > wp] Hypothesis missing about pointed datatypes (dargaye) - closed.
- 0000796: [Plug-in > wp] initial value of structures (dargaye) - closed.
- 0000800: [Plug-in > RTE] wrong generation of assigns \nothing at function call (pherrmann) - closed.
- 0000801: [Plug-in > slicing] r12951, slicing is slow (Anne) - closed.
- 0000806: [Plug-in > slicing] r13065, missing declaration for tmp variable in sliced program (csmith) (Anne) - closed.
- 0000799: [Plug-in > slicing] r12925: Slicing: missing label (csmith) (Anne) - closed.
- 0000802: [Plug-in > slicing] r12951, sliced program does not terminate (Anne) - closed.
- 0000820: [Plug-in > Eva] Value analysis crashes in lib-entry mode with peculiar context (pascal) - closed.
- 0000809: [Plug-in > slicing] sliced program does not terminate (csmith) (Anne) - closed.
- 0000812: [Kernel > ACSL implementation] Cil does not correctly handle ACSL annotations with nested comments when called with -pp-annot (virgile) - closed.
- 0000828: [Plug-in > slicing] r13521 sliced program does not terminate (csmith) (Anne) - closed.
- 0000844: [Plug-in > Eva] Incorrect results with low slevel (pascal) - closed.
- 0000841: [Kernel > ACSL implementation] no conversion int[] to int* for logic fct arg; exprs a and &a[0] treated differently (virgile) - closed.

[115 issues]


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker