Change Log - Frama-C Bug Tracking System

Frama-C - Change Log
Frama-C - Frama-C Nitrogen-20111001 =================================== - 0000905: [Plug-in > slicing] 14403: last slicing bug (csmith) (Anne) - closed. - 0000897: [Plug-in > slicing] error: label ‘__invalid_label’ used but not defined (csmith) (Anne) - closed. - 0000871: [Plug-in > semantic constant folding] scfed program behaves differently from original (administrator) - closed. - 0000880: [Plug-in > slicing] 14055: sliced program does not terminate (csmith) (Anne) - closed. - 0000968: [Plug-in > value analysis] Slicing generates empty program (csmith) (yakobowski) - closed. - 0000963: [Plug-in > slicing] Sliced program computes differently from original (csmith) (Anne) - closed. - 0000969: [Kernel] Sliced program computes differently from original (csmith) (pascal) - closed. - 0000858: [Plug-in > semantic constant folding] emitted program computes differently from original (csmith) (administrator) - closed. - 0000933: [Kernel] Wrong AST (csmith) (pascal) - closed. - 0001041: [Kernel] #pragma diag_suppress 1107 causes syntax error (pascal) - closed. - 0000814: [Plug-in > jessie] memory blocks: pointer assignment and equality treated differently (cmarche) - closed. - 0000024: [Plug-in > jessie] Ordering of lemma in coq output of jessie (cmarche) - closed. - 0000832: [Kernel] r13586 Spurious "assert \separated(...)" (csmith) (virgile) - closed. - 0000725: [Kernel] passing (C && c) as argument to a function that expects int (csmith) (virgile) - closed. - 0000576: [Plug-in > wp] axiom ignored because of label, but no label is present in axiom. (Anne) - closed. - 0000835: [Kernel > ACSL implementation] Aggregate logic types containing only C types (virgile) - closed. - 0000892: [Kernel] Cil wrongly authorizes references to local variables in static arrays (virgile) - closed. - 0000926: [Plug-in > wp] wp-plugin does not generate coq *.v goals. (correnson) - closed. - 0000913: [Plug-in > value analysis] 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. - 0000911: [Kernel] incorrect AST generated (yakobowski) - closed. - 0000927: [Plug-in > sparecode] Sparecode could eliminate unnecessary if statements (Anne) - closed. - 0000946: [Plug-in > semantic constant folding] -semantic-const-folding should have a -semantic-constant-folding alias (administrator) - closed. - 0000949: [Plug-in > value analysis] Valid access to literal w_chart string address considered invalid (pascal) - closed. - 0000947: [Plug-in > sparecode] -sparecode-analysis option should have -sparecode alias (administrator) - closed. - 0000961: [Kernel] Cil incorrectly cast arguments to switch to int (virgile) - closed. - 0000954: [Plug-in > metrics] failure: bad initialisation: Too many initializations of the AST (virgile) - closed. - 0000966: [Kernel] bad default assigns generation (virgile) - closed. - 0000979: [Plug-in > wp] Unexpected label Old in pre : ignored annotation (correnson) - closed. - 0000517: [Graphical User Interface] Exception raised if dot not found (administrator) - closed. - 0000522: [Kernel] size of long array can't be represented with OCaml int (virgile) - closed. - 0000616: [Kernel] Comments parsing (virgile) - closed. - 0000641: [Plug-in > wp] alt-ergo version managment (dargaye) - closed. - 0000655: [Kernel > ACSL implementation] using real function ( \max, \min, \abs ) instead of integer one in function contract (virgile) - closed. - 0000674: [Plug-in > jessie] Crash (cmarche) - closed. - 0000680: [Plug-in > value analysis] Use of Cabs2cil.fresh_global (pascal) - closed. - 0000689: [Plug-in > value analysis] Value may be incorrect in presence of several ensures (administrator) - closed. - 0000691: [Kernel > ACSL implementation] Comments parsing not always work (virgile) - closed. - 0000709: [Plug-in > slicing] Bug in slicing -- required C-statements getting knocked off from sliced code (Anne) - closed. - 0000718: [Plug-in > value analysis] possible unsoundness in r11866 (pascal) - closed. - 0000717: [Plug-in > value analysis] possible unsoundness bug (pascal) - closed. - 0000719: [Kernel] unsoundness due to packed structs (pascal) - closed. - 0000716: [Kernel] crash from r11865 (virgile) - closed. - 0000715: [Plug-in > value analysis] crash bug in r11859 (pascal) - closed. - 0000714: [Kernel > ACSL implementation] Lexing of ACSL characters (patrick) - closed. - 0000730: [Plug-in > value analysis] Print addresses in hexadecimal (pascal) - closed. - 0000729: [Kernel] Plugin.is_invisible is not see-through enough (signoles) - closed. - 0000727: [Kernel] Function specification not exposed through vspec visitor method (virgile) - closed. - 0000724: [Graphical User Interface] Selection of [loop variant] properties in GUI (administrator) - closed. - 0000723: [Graphical User Interface] r11920: Analyses -> Show callgraph requires a main function (signoles) - closed. - 0000720: [Kernel] Incorrect handling of nearly-empty switch clauses with -simplify-cfg (virgile) - closed. - 0000721: [Plug-in > value analysis] Unsoundness in value analysis when bitfield initializer exceeds range (csmith) (pascal) - closed. - 0000752: [Plug-in > value analysis] Unexpected error (Ival.Float_abstract.Bottom) (pascal) - closed. - 0000751: [Kernel > ACSL implementation] Promotion from integer to boolean (virgile) - closed. - 0000744: [Kernel > ACSL implementation] Too much type promotion for terms (virgile) - closed. - 0000737: [Kernel] frama-c always crashes when I install new plugins (signoles) - closed. - 0000736: [ptests] the input file should be the first argument to ptests (virgile) - closed. - 0000732: [Plug-in > value analysis] Incorrect states passed to value analysis callbacks in presence of slevel (pascal) - closed. - 0000768: [Plug-in > impact analysis] Impact analysis does not catch Pdg.Top (returned on variadic calls) (signoles) - closed. - 0000762: [Kernel] unsigned constants truncated (csmith) (virgile) - closed. - 0000761: [Kernel > ACSL implementation] typing rule of \old(tab) or tab[index] construct (virgile) - closed. - 0000758: [Plug-in > sparecode] Sparecode removes definitions which should be kept. (Anne) - closed. - 0000757: [Documentation] mismatch between configure check and INSTALL requirements for ocamlgraph version (signoles) - closed. - 0000754: [Kernel > Makefile] Dynamic plugin doc (virgile) - closed. - 0000774: [Plug-in > slicing] Slicing is sometimes not journalisable anymore (signoles) - closed. - 0000771: [Kernel] r12436, unnecessary warning for side-effects (csmith) (virgile) - closed. - 0000770: [Kernel] r12430, some assertions are localized at Cabs2cil_start:0 (csmith) (virgile) - closed. - 0000769: [Kernel] _ not supported as member name in struct (virgile) - closed. - 0000775: [Kernel] Hex/octal signed constants can be represented in an unsigned extended integer type (csmith) (administrator) - closed. - 0000780: [Plug-in > slicing] r12793: slicing generates uncompilable code (sliced function called with too few arguments) (csmith) (virgile) - closed. - 0000781: [Plug-in > functional dependencies] Sliced program computes value different from original (csmith) (pascal) - closed. - 0000779: [Plug-in > wp] Hypothesis missing about pointed datatypes (dargaye) - closed. - 0000787: [Plug-in > slicing] same conditions as 786, sliced program does not terminate when original does (csmith) (Anne) - closed. - 0000786: [Plug-in > slicing] 12816: Missing label in sliced program (csmith) (Anne) - closed. - 0000785: [Kernel] 12799, doubtful choice of promotion x86_64 mode (csmith) (pascal) - closed. - 0000784: [Plug-in > metrics] Generating metrics.html on demand (administrator) - closed. - 0000788: [Plug-in > wp] initializer completion (dargaye) - closed. - 0000789: [Plug-in > slicing] 12825, sliced program does not terminate (Anne) - closed. - 0000798: [Plug-in > value analysis] Serial conversions in function result (csmith) (pascal) - closed. - 0000790: [Kernel > ACSL implementation] integrity problem of the AST on calls to functions with __attribute__ ((noreturn)) (virgile) - closed. - 0000796: [Plug-in > wp] initial value of structures (dargaye) - closed. - 0000791: [Plug-in > value analysis] Cash in value analysis of sliced project (pascal) - closed. - 0000801: [Plug-in > slicing] r12951, slicing is slow (Anne) - closed. - 0000800: [Plug-in > RTE] wrong generation of assigns \nothing at function call (pherrmann) - closed. - 0000802: [Plug-in > slicing] r12951, sliced program does not terminate (Anne) - closed. - 0000799: [Plug-in > slicing] r12925: Slicing: missing label (csmith) (Anne) - closed. - 0000806: [Plug-in > slicing] r13065, missing declaration for tmp variable in sliced program (csmith) (Anne) - closed. - 0000807: [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. - 0000808: [Plug-in > slicing] r13089 sliced program computes differently from original (csmith) (Anne) - closed. - 0000820: [Plug-in > value analysis] Value analysis crashes in lib-entry mode with peculiar context (pascal) - closed. - 0000819: [Plug-in > value analysis] wrong interpretation when a bit-field receives the result of a function (csmith) (pascal) - closed. - 0000809: [Plug-in > slicing] sliced program does not terminate (csmith) (Anne) - closed. - 0000810: [Kernel] pretty-printed program rejected by GCC. Affects -print, slicing, scf (csmith) (administrator) - closed. - 0000817: [Kernel] r13378, assertion failed with bit-fields (administrator) - closed. - 0000828: [Plug-in > slicing] r13521 sliced program does not terminate (csmith) (Anne) - closed. - 0000827: [Plug-in > slicing] sliced program computes differently from original (csmith) (Anne) - closed. - 0000825: [Plug-in > slicing] r13465, crash in slicing (csmith) (Anne) - closed. - 0000823: [Kernel] r13417 unsigned bit-fields of width 32 should be promoted to unsigned int (csmith) (administrator) - closed. - 0000821: [Documentation] Wrong module name for the function prepareCFG and computeCFGInfo in the Frama-C Carbon html API. (signoles) - closed. - 0000841: [Kernel > ACSL implementation] no conversion int[] to int* for logic fct arg; exprs a and &a[0] treated differently (virgile) - closed. - 0000844: [Plug-in > value analysis] Incorrect results with low slevel (pascal) - closed. - 0000857: [Kernel] Ocaml 32 bits version 3.11.0 (patrick) - closed. - 0000859: [Kernel > ACSL implementation] ACSL pretty-printer (virgile) - closed. - 0000861: [Kernel] Incorrect loop unrolling in presence of switch (virgile) - closed. - 0000889: [Plug-in > value analysis] File "src/memory_state/lmap.ml", line 931, characters 22-28: Assertion failed (pascal) - closed. - 0000884: [Documentation] wrong figure reference in plugin development guide (signoles) - closed. - 0000883: [Plug-in > value analysis] Crash du builtin memcpy, par une exception non rattrapable (pascal) - closed. - 0000882: [Kernel] Cil generates incorrect switch (with missing cases) (virgile) - closed. - 0000885: [Kernel > ACSL implementation] Typing error on expression array == pointer (virgile) - closed. - 0000896: [Plug-in > wp] Warning for Axiom: From wp: Overloaded operator User defined axiom (correnson) - closed. - 0000890: [Plug-in > value analysis] Results differ between value analysis and GCC on bitfields (pascal) - closed.Frama-C - Frama-C Carbon-20110201 ================================= - 0000836: [Plug-in > value analysis] Unexpected error (File "cil/ocamlutil/cilutil.ml", line 918, characters 10-16: Assertion failed). (pascal) - closed. - 0000642: [Plug-in > wp] unprovable po with -split (dargaye) - closed. - 0000662: [Plug-in > wp] warning: Degenerated goal (dargaye) - closed. - 0000665: [Plug-in > wp] Unexpected error (Stack overflow) during WP (correnson) - closed. - 0000646: [Plug-in > wp] [wp] warning: Stronger goal store_AppelerVerifier_post_6 (1 warning) (dargaye) - closed. - 0000701: [Plug-in > wp] Unexpected error (Failure("int_of_string")). (correnson) - closed. - 0000710: [Plug-in > slicing] Crash during slicing (Anne) - closed. - 0000677: [Kernel] Help options are wrongly described as "aliases" when they have the same description. (signoles) - closed. - 0000630: [Kernel] bad location with tmp CIL variable (virgile) - closed. - 0000635: [Kernel] losing messages doing save/load (signoles) - closed. - 0000637: [Kernel > Makefile] actions done with make install -n (svn 10897) (signoles) - closed. - 0000645: [Kernel] lose of location displayed by Cil.warning (administrator) - closed. - 0000647: [Kernel > configure] lib apron not found in configure (signoles) - closed. - 0000673: [Plug-in > slicing] untypable ACSL in a sliced program containing \result (patrick) - closed. - 0000666: [Graphical User Interface] Wrong evaluation of expression in the GUI (pascal) - closed.Frama-C - Frama-C Carbon-20101202-beta2 ======================================= - 0000639: [Plug-in > wp] Carbon beta coqide: need write rights to /usr/local/share/frama-c (correnson) - closed. - 0000656: [Plug-in > jessie] crash with wrong commandline option (cmarche) - closed. - 0000033: [Plug-in > jessie] Launching several instances of the prover in parallel from the GUI? (cmarche) - closed. - 0000240: [Plug-in > jessie] Problems with solver configuration (cmarche) - closed. - 0000404: [Plug-in > jessie] Jessie translation unexpected failure (cmarche) - closed. - 0000299: [Plug-in > jessie] Frama-C stops with unexpected failure (Ref. "norm.ml:1105:8") (cmarche) - closed. - 0000363: [Plug-in > jessie] Plugin jessie aborted because of an internal error. (cmarche) - closed. - 0000537: [Plug-in > jessie] Predicate Sorted causes crash (norm.ml:1524:10) (cmarche) - closed. - 0000530: [Plug-in > jessie] crash (cmarche) - closed. - 0000523: [Plug-in > jessie] struct-type expression in loop-assigns causes crash (cmarche) - closed. - 0000509: [Plug-in > jessie] Unexpected exception if no input file (cmarche) - closed. - 0000476: [Plug-in > jessie] Partial support of tset leads to assert failure (cmarche) - closed. - 0000434: [Plug-in > jessie] assertion at line 2772 of jc/jc_typing.ml fails (cmarche) - closed. - 0000427: [Plug-in > jessie] Jessie crashes on \old(*ptr) (cmarche) - closed. - 0000426: [Plug-in > jessie] Jessie internal error (cmarche) - closed. - 0000500: [Plug-in > jessie] Uncaught exception in jc/jc_effect.ml caused by union type (cmarche) - closed.Frama-C - Frama-C Carbon-20101201-beta1 ======================================= - 0000588: [Kernel] Error when function contract defined after function definition and with different parameter names (virgile) - closed. - 0000448: [Plug-in > slicing] invariant with quantifier not kept in computed slice (Anne) - closed. - 0000524: [Kernel] Missing declared inline functions in Globals (administrator) - closed. - 0000569: [Graphical User Interface] Stoping external process (why) (administrator) - closed. - 0000482: [Kernel > ACSL implementation] for behav : invariant INV ; (patrick) - closed. - 0000244: [Plug-in > value analysis] block-local variables not handled correctly in conjunction with -ulevel (pascal) - closed. - 0000259: [Plug-in > value analysis] Problem with is_finite predicate generated by -val (pascal) - closed. - 0000365: [Documentation] Jessie tutorial binary_search examples fail with Why 2.23 - loop variant must be added (cmarche) - closed. - 0000339: [Documentation] wrong option name in Jessie Plugin Tutorial (signoles) - closed. - 0000452: [Kernel] "Body of function main falls-through" warning could be improved (virgile) - closed. - 0000451: [Kernel] Crash when a 'break' occurs outside a proper statement (virgile) - closed. - 0000460: [Kernel > Makefile] .make-ocamlgraph is not needed when using non-local ocamlgraph (signoles) - closed. - 0000461: [Kernel > Makefile] Frama-c-gui doesn't install on bytecode architecture (signoles) - closed. - 0000462: [Kernel > Makefile] Makefile.dynamic should not change known_plugins.ac (virgile) - closed. - 0000472: [Plug-in > value analysis] Comparing a function pointer will NULL might raise incorrect warning (pascal) - closed. - 0000470: [Graphical User Interface] In the GUI, it is impossible to talk about variables generated by Value's -lib-entry (pascal) - closed. - 0000489: [Kernel] Cint64 user constants have no textual representation (virgile) - closed. - 0000484: [Kernel > ACSL implementation] function and statement behaviors (patrick) - closed. - 0000474: [Documentation] Multiple definition of function iter_stmt (signoles) - closed. - 0000519: [Kernel] int t[static 2] is not supported as function argument (virgile) - closed. - 0000525: [Kernel] inchoherence of types between enumitems and enum type with multi-files (virgile) - closed. - 0000512: [Kernel] suggest to refer to fct-contract's clauses-order in error message (virgile) - closed. - 0000505: [Kernel > ACSL implementation] Predicate/Functions depending only on a state are not handled correctly (virgile) - closed. - 0000506: [Kernel] line command option for doCollapseCallCast configuration (virgile) - closed. - 0000538: [Kernel] Frama-C should produce more specific error messages when parsing annotations (virgile) - closed. - 0000529: [Plug-in > sparecode] slicing produces uncompilable program when formal used as a local variable (Anne) - closed. - 0000528: [Kernel > Makefile] Makefile.dynamic should always write to $(DESTDIR) (signoles) - closed. - 0000550: [Plug-in > occurrence] Selecting "occurrence" crashes Frama-C (signoles) - closed. - 0000549: [Kernel > ACSL implementation] Typing problem into the logic about C variable of an array type. (virgile) - closed. - 0000541: [Kernel > ACSL implementation] When using -pp-annot and including stdbool.h, can't parse \false in annotations (virgile) - closed. - 0000552: [Kernel] Checking number of arguments passed to C functions (virgile) - closed. - 0000568: [Kernel > ACSL implementation] cast to const type not handled in acsl annotations (virgile) - closed. - 0000554: [Documentation] Logic_utils and Logic_const documentation ... (signoles) - closed. - 0000570: [Kernel > ACSL implementation] Incorrect typing of annotations (virgile) - closed. - 0000595: [Documentation] Implementation <-> Documentation Inconsistency (virgile) - closed. - 0000584: [Plug-in > jessie] incorrect(?) jessie code generated from strcpy (cmarche) - closed. - 0000612: [Documentation] Mention that invariant does not hold after for-loop (virgile) - closed. - 0000440: [Plug-in > jessie] Pb with annot.c in (virgile) - closed. - 0000620: [Kernel] Default assigns generation (patrick) - closed. - 0000510: [Plug-in > jessie] Jessie generates error when called to be executed. (signoles) - closed. - 0000634: [Plug-in > value analysis] Superfluous ';' in value analysis output (pascal) - closed. - 0000548: [Kernel] Header limit.h is nonsense (pascal) - closed.Frama-C - Frama-C Boron-20100401 ================================ - 0000370: [Plug-in > jessie] pragma JessieIntegerModel (cmarche) - closed. - 0000367: [Plug-in > jessie] bug with constants like 1E-6 (cmarche) - closed. - 0000338: [Plug-in > jessie] free() should permit 0 as valid argument (cmarche) - closed. - 0000361: [Plug-in > jessie] "why" reports "unbound label" (cmarche) - closed. - 0000406: [Plug-in > jessie] assert false (* TODO *) (cmarche) - closed. - 0000399: [Plug-in > jessie] Statement contract and "hiding" of statement (cmarche) - closed. - 0000420: [Plug-in > jessie] same formula translated differently as axiom/lemma (cmarche) - closed. - 0000386: [Plug-in > jessie] int32 and real can't be unified (cmarche) - closed. - 0000391: [Plug-in > jessie] Why keywords as ACSL identifiers (cmarche) - closed. - 0000443: [Plug-in > jessie] assigns clause unchecked on arrays (cmarche) - closed. - 0000346: [Documentation] Example 2.31 of ACSL 1.4 (Beryllium implementation) incorrect (virgile) - closed. - 0000382: [Kernel > Makefile] Should not call install-kernel-opt on bytecode architectures (signoles) - closed. - 0000385: [Kernel] File "src/kernel/cilE.ml", line 372, characters 13-19: Assertion failed (virgile) - closed. - 0000388: [Plug-in > value analysis] Incorrect 'assert false' in value analysis (administrator) - closed. - 0000376: [Plug-in > jessie] unsigned long long constant becomes signed (cmarche) - closed. - 0000381: [Plug-in > value analysis] propagation of \result clauses (pascal) - 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. - 0000366: [Plug-in > jessie] Unicode minus sign (U+2212) not accepted by Jessie, yet used in documentation, causing mysterious failure (administrator) - closed. - 0000372: [Plug-in > value analysis] Wrong postconditions are "valid according to value analysis" (virgile) - closed. - 0000374: [Graphical User Interface] "-cpp-command ..." parameter lost (signoles) - closed. - 0000431: [Kernel] Dgraph.DGraphModel.read_dot (signoles) - closed. - 0000435: [Plug-in > syntactic callgraph] Too many edges in call graph (signoles) - closed. - 0000414: [Plug-in > value analysis] imprecision in widening/narrowing for char and short index (pascal) - closed. - 0000392: [Plug-in > value analysis] Failure("Function 'From.find_deps_no_transitivity' not registered yet") (pascal) - closed. - 0000393: [Plug-in > slicing] assigns clauses are missing from the sliced program (Anne) - closed. - 0000398: [Kernel > configure] RTE compiled even with ./configure --disable-rte (signoles) - closed. - 0000272: [Plug-in > jessie] complete behaviors; disjoint behaviors; (virgile) - closed. - 0000257: [Kernel] get_varinfo not exported in src/ai/base.mli (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. - 0000213: [Kernel] crash in parser when double definition of variable in two different files, in some order (virgile) - closed. - 0000325: [Plug-in > value analysis] Precise widening when a loop condition involves a char or short (pascal) - closed. - 0000327: [Kernel > ACSL implementation] order of 'decreases' and 'behavior' clauses (virgile) - closed. - 0000329: [Kernel > ACSL implementation] Float promoted to double (cmarche) - closed. - 0000332: [Kernel] goto generated by Frama-C and not supported by Jessie (virgile) - closed. - 0000342: [Kernel > ACSL implementation] Assertion failed instead of typing error report (virgile) - closed. - 0000305: [Kernel > configure] After ./confugure with --disable-all-staff options, make holds (signoles) - closed. - 0000309: [Kernel > ACSL implementation] After ./confugure with --disable-all-staff options and make static, frama-c-Myplugin.byte crashes (virgile) - closed. - 0000310: [Kernel] Be careful when activating warnings. (signoles) - closed. - 0000311: [Kernel] switch and case expressions must be integer (virgile) - closed. - 0000314: [Plug-in > value analysis] malloc.h can't be preprocessed: __func__ is not a macro (pascal) - closed.Frama-C - Frama-C Beryllium-20090902 ==================================== - 0000187: [Plug-in > jessie] Error while processing legitimate C construction (cmarche) - closed. - 0000273: [Plug-in > jessie] Uncaught exception: assert false on bitvector (cmarche) - closed. - 0000071: [Plug-in > jessie] labels are not correctly translated in jessie+why (cmarche) - closed. - 0000347: [Plug-in > jessie] Using Z3 dumps plenty logs of texts in the console (cmarche) - closed. - 0000170: [Documentation] Impossible to pass option to jessie or why through jessie plugin (correnson) - closed. - 0000222: [Plug-in > jessie] Recursive logic definitions are not correctly translated. (cmarche) - closed. - 0000260: [Plug-in > jessie] is_finite predicate: type double expected instead of real in .jc file (ayad) - closed. - 0000285: [Plug-in > jessie] jessie problem - closed. - 0000068: [Plug-in > value analysis] Plug-in inout fails to parse clause /*@ assigns s[..]; */ (pascal) - closed. - 0000223: [Kernel] -warn-unspecified-order false positive (virgile) - closed. - 0000242: [Graphical User Interface] 'Go to definition' and 'Go to caller' do not update main view of GUI (administrator) - closed. - 0000237: [Graphical User Interface] Warning repetition in Messages window (correnson) - closed. - 0000236: [Graphical User Interface] Error when linking the viewer (signoles) - closed. - 0000234: [Kernel] Wrong display of call stacks in value analysis (correnson) - closed. - 0000230: [Kernel] Missing functions to convert logic terms directly to abstract values (pascal) - closed. - 0000253: [Kernel] Extlib.deprecated does not use Log.* to print messages (correnson) - closed. - 0000224: [Kernel] Non-exhaustive pattern matching leads to compilation error (signoles) - closed. - 0000250: [Plug-in > obfuscator] obfuscator loses link between logic and C variables (administrator) - closed. - 0000238: [Graphical User Interface] Files of a project state not displayed on reload in GUI (administrator) - closed.Frama-C - Frama-C Beryllium-20090901 ==================================== - 0000216: [Plug-in > scope] Uncaught exception in scope (pascal) - closed. - 0000197: [Kernel] Options <plug-in>-debug and <plug-in>-verbose for dynamic plug-ins do not work (signoles) - closed. - 0000180: [Kernel] Save/Load elapsed time (pascal) - closed. - 0000182: [Kernel] The file `share/configure.ac' is missing (virgile) - closed. - 0000225: [Graphical User Interface] Incorrect linking order for the viewer (signoles) - closed. - 0000189: [Kernel] the configure script does not work properly with libocamlgraph-ocaml-dev 1.1-1 (signoles) - closed. - 0000190: [Plug-in > slicing] crash when unbound variable (patrick) - closed. - 0000195: [Plug-in > value analysis] wrongly synthesized assert (pascal) - closed. - 0000184: [Plug-in > slicing] slicing crashes when there is no entry point to the function (Anne) - closed. - 0000163: [Kernel] crash for untyped_metrics example plugin (administrator) - closed. - 0000169: [Kernel] Build fails due to Printexc.record_backtrace (signoles) - closed. - 0000183: [Kernel] 'make top' fails (virgile) - closed. - 0000193: [Plug-in > slicing] crash with information [kernel] error: unexpected error Extlib.NotYetImplemented("[logic_interp] not a lvalue") (correnson) - closed. - 0000211: [Kernel] "make doc" error (signoles) - closed. - 0000192: [Kernel] -ocode causes crach (pascal) - closed. - 0000198: [Kernel] Packing for dynamic plug-in is not done in current directory (signoles) - closed. - 0000200: [Kernel] Error while linking lib/plugins/Jessie.cmo (signoles) - closed.Frama-C - Frama-C Beryllium-20090601-beta1 ========================================== - 0000096: [Kernel] "logic set<struct something *> f(...)" throw a syntax error (virgile) - closed. - 0000160: [Plug-in > jessie] \at(...,Post) in assigns clause (cmarche) - closed. - 0000117: [Kernel] int -> integer -> real (virgile) - closed. - 0000115: [Plug-in > aoraï] problem for making dynamic plugin (signoles) - closed. - 0000111: [Kernel] Compilation error if options --with-jessie-static --with-ltl_to_acsl-static are present. (signoles) - closed. - 0000095: [Plug-in > jessie] "//@ assert i >= CHAR_MIN;" not proven for char (cmarche) - closed. - 0000094: [Plug-in > jessie] "assert i >= 0;" not proven for unsigned char (cmarche) - closed. - 0000148: [Kernel] cmdline.ml assertion error at line 88 (signoles) - closed. - 0000046: [Plug-in > jessie] Jessie/GWhy/Gappa: format file and invalid POs proved valid (cmarche) - closed. - 0000041: [Plug-in > jessie] Inability to prove assigns clauses on simple array code (cmarche) - closed. - 0000036: [Plug-in > jessie] GUI blocked (100% cpu used) when requested to display an assertion (virgile) - closed. - 0000029: [Plug-in > jessie] Lithium fool the tool (cmarche) - closed. - 0000028: [Plug-in > jessie] Jessie-gui : call of coqide and --project option (cmarche) - closed. - 0000049: [Plug-in > jessie] Jessie/Gwhy: cpulimit-win.c (cmarche) - closed. - 0000088: [Kernel] Frama-C should stop on error in annotations instead of issuing a warning (virgile) - closed. - 0000077: [Plug-in > value analysis] if((int)(&a+2)) fails to warn about being unspecified (pascal) - closed. - 0000076: [Plug-in > value analysis] int a; main(){ return 100 / (int)(&a + 2); } fails to report a division by zero (pascal) - closed. - 0000073: [Plug-in > jessie] A pure predicate in an axiomatic with some "unpure" axioms have some strange results (cmarche) - closed. - 0000062: [Kernel] integer is not well-casted in real (virgile) - closed. - 0000061: [Kernel] frama-c --help (signoles) - closed. - 0000060: [Kernel] Conversion from integer to real (virgile) - closed. - 0000059: [Kernel] code normalisation issue when return variable is named __retres (administrator) - closed.

Mantis 1.1.6[^]