Anonymous |
Login
|
Signup for a new account
2019-12-10 03:23 CET
Main
|
My View
|
View Issues
|
Change Log
|
Roadmap
|
Repositories
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]
Copyright © 2000 - 2019 MantisBT Team