Change Log - Frama-C Bug Tracking System

Frama-C - Change Log
Frama-C - Frama-C Neon-20140301 (Released 2014-03-07) [ View Issues ] ===================================================== - 0001518: [Kernel] Cast on funspec not considering typedef (virgile) - closed. - 0001620: [Documentation > manuals] RTE - Documentation on Unary Minus (signoles) - closed. - 0001503: [Kernel] failure: invalid implicit conversion from void to int (virgile) - closed. - 0001818: [Plug-in > E-ACSL] Global variables are not marked as initialized (signoles) - closed. - 0001831: [Plug-in > E-ACSL] Command line arguments (argc/argv) are not marked as valid (signoles) - closed. - 0001716: [Plug-in > E-ACSL] Dynamically allocated variables in body of while without break are not instrumented (signoles) - closed. - 0001696: [Plug-in > E-ACSL] warning: E_ACSL function 'initialize' called with null pointer - seems to affect the behavior (signoles) - closed. - 0001717: [Plug-in > E-ACSL] Instrumentation of statements with labels are not inserted at the correct location (signoles) - closed. - 0001715: [Plug-in > E-ACSL] "[...]/e_acsl_bittree.c:341: __get_exact: Assertion `0' failed." using full memory model, asserting validty of local var (signoles) - closed. - 0001836: [Plug-in > E-ACSL] A pointer can be reported as belonging to an adjacent memory blocks in the bittree memory model (signoles) - closed. - 0001692: [Plug-in > E-ACSL] Wrong localisation of not yet supported constructs (signoles) - closed. - 0001695: [Plug-in > E-ACSL] Impossible to compile the eacsl produced source (signoles) - closed. - 0001903: [Kernel > configure] Configure fails for GNU Make 4.0 (signoles) - closed. - 0001574: [Kernel > configure] make version 4.0 is rejected (virgile) - closed. - 0001416: [Plug-in > Eva] 22446: unknown sizes of types and value initialization (yakobowski) - closed. - 0001587: [Plug-in > wp] syntax error for alt-ergo with memset spec (correnson) - closed. - 0001634: [Plug-in > E-ACSL] e-acsl translation: unexpected error (signoles) - closed. - 0001369: [Plug-in > Eva] strange warning "postcondition got status invalid" (yakobowski) - closed. - 0001352: [Kernel] Error message could be better (virgile) - closed. - 0001388: [Kernel] Frama-C should not honor -save if when it aborts (signoles) - closed. - 0001415: [Plug-in > Eva] Logging just enough information for failed pre-conditions (yakobowski) - closed. - 0001435: [Plug-in > Eva] The post-conditon of [gets] got status invalid (yakobowski) - closed. - 0001440: [Kernel] AST integrity check failure with kernel-debug (virgile) - closed. - 0001441: [Kernel] frama-c.toplevel not working anymore (signoles) - closed. - 0001457: [Kernel] Incorrect printing of designated initializers (virgile) - closed. - 0001353: [Plug-in > wp] ACSL label LoopEntry not handled by WP (correnson) - closed. - 0001451: [Kernel] Journalisation of -no-unicode option (signoles) - closed. - 0001447: [Plug-in > Eva] uninitialized value can be passed through pointer, through return, but not through function argument (yakobowski) - closed. - 0001462: [Plug-in > wp] invalid loop invariant marked as valid (without pending hypothesis) (correnson) - closed. - 0001475: [Kernel] Frama-C Kernel on a specific C file (unexpected error, assertion failed) (virgile) - closed. - 0001469: [Kernel] Unsound transformation of ACSL annotations (virgile) - closed. - 0001502: [Kernel] goto L; with L: in a if/else branch (virgile) - closed. - 0001500: [Kernel] r24011: failure: Invalid combination of type specifiers (virgile) - closed. - 0001536: [Kernel > ACSL implementation] Binding of label in annotations is strange (virgile) - closed. - 0001562: [Plug-in > obfuscator] Obfuscator for C Labels (signoles) - closed. - 0001584: [Plug-in > Eva] Assertion failure in Ival.scale_div (pascal) - closed. - 0001589: [Kernel] access to volatile variable is eliminated from AST (virgile) - closed. - 0001588: [Plug-in > wp] WP ignores some goal (correnson) - closed. - 0001586: [Plug-in > wp] Bug in let-elimination (due to <==> and assert false). (correnson) - closed. - 0001590: [Plug-in > scope] Feedback from -remove-redundant-alarms (yakobowski) - closed. - 0001626: [Plug-in > wp] Qedlib.v definition of tactic "replace by" clashes with standard tactic "replace with" (correnson) - closed. - 0001623: [Plug-in > wp] Allow starting coq from Frama-C GUI also for proven obligations (correnson) - closed. - 0001631: [Plug-in > wp] Confusing bullets for unproven obligations under OSX (correnson) - closed. - 0000929: [Kernel] syntax error in value binary assignment (virgile) - closed. - 0000624: [Kernel] Logging huge messages makes kernel crashing (correnson) - closed. - 0001330: [Kernel] inconsistent redefinition of type undetected (virgile) - closed. - 0001044: [Plug-in > Eva] Smarter access to array of struct of array (yakobowski) - closed. - 0001443: [Plug-in > wp] Property reported as inconditionnally valid when its dependency graph shows some orange box (signoles) - closed. - 0001436: [Plug-in > pdg] Stack overflow when computing a PDG (yakobowski) - closed. - 0001445: [Plug-in > slicing] Crash when selecting the calls to an unterminating functions (patrick) - closed. - 0001448: [Plug-in > Eva] Interpretation of @ assigns \result; (yakobowski) - closed. - 0001480: [Kernel > ACSL implementation] assigns \result \from ...; in the AST should be pretty-printed as any other assigns clause (yakobowski) - closed. - 0001486: [Plug-in > Eva] validity of a field defined in an abstract struct typedef (yakobowski) - closed. - 0001549: [Plug-in > wp] Error message when a solver is not installed (correnson) - closed. - 0001559: [Plug-in > Eva] pointer comparable assert generated between void* and unsigned long (yakobowski) - closed. - 0001563: [Plug-in > obfuscator] Obfuscator for tags names in ACSL terms, properties, behaviors (signoles) - closed. - 0001573: [Kernel] Syntax error because of pause instruction in inline assebly (yakobowski) - closed. - 0001572: [Kernel] Multiple contracts merge twice resutling in Kernel error (yakobowski) - closed. - 0001601: [Plug-in > wp] WP Plugin with Alt-Ergo - unable to prove? (correnson) - closed. - 0001622: [Plug-in > wp] WP: This term has type real but is expected to have type int (correnson) - closed. - 0001603: [Plug-in > wp] Errors in coq files generated by WP (correnson) - closed. - 0001289: [Plug-in > aoraï] aorai causes failed assertion (virgile) - closed. - 0001439: [Kernel] Few fixes in libc/sys/socket.h (Matthieu Lemerre) - closed. - 0001477: [Plug-in > Eva] Value analysis: bad type conversion plus unassigned fields in a struct leads to crash (yakobowski) - closed. [64 issues]