Frama-C Bug Tracking System

Frama-C - Change Log

Frama-C - Frama-C 16 Sulfur (Not Yet Released) View Issues ]
==============================================
- 0002303: [Plug-in > E-ACSL] E-ACSL generates functions definitions without argument-names (signoles) - resolved.
- 0002304: [Plug-in > E-ACSL] E-ACSL: compilation fail: generated functions doesn't have static inline attributes (signoles) - resolved.
- 0002297: [Kernel] syntax error before loop contract reported after loop contract (maroneze) - resolved.

[3 issues]

Frama-C - Frama-C 15 Phosphorus (Released 2017-05-31) View Issues ]
=====================================================
- 0002253: [Kernel > libc] File frama-c/libc/features.h should include definition of the macro __GNUC_PREREQ from file /usr/include/features.h (maroneze) - resolved.
- 0002137: [Plug-in > value analysis] value analysis introduces weird pointer assert with variable length arrays (yakobowski) - closed.
- 0000733: [Plug-in > inout] Invalid results in presence of pseudo-recursive calls in inout and from (yakobowski) - closed.
- 0001740: [Plug-in > E-ACSL] Incorrectness when early exiting a block (signoles) - closed.
- 0002269: [Plug-in > obfuscator] There is a typo in description of plug-in: "objuscator" instead of "obfuscator". (signoles) - closed.
- 0002277: [Plug-in > value analysis] Operability depends on the order of options changes (yakobowski) - closed.
- 0002252: [Plug-in > E-ACSL] GMP typing issue (signoles) - closed.
- 0002235: [Kernel] Functions that claim to return a struct but don't cause a crash (virgile) - closed.
- 0002279: [Plug-in > value analysis] EVA analysis does not start with click on "Execution" button. (yakobowski) - closed.
- 0002283: [Plug-in > wp] type of float parameter changed unexpectedly to double (correnson) - closed.
- 0002284: [Plug-in > E-ACSL] E-ACSL type system crash (signoles) - closed.

[11 issues]

Frama-C - Frama-C 14 Silicon (Released 2016-11-30) View Issues ]
==================================================
- 0001817: [Plug-in > E-ACSL] Literal strings in global arrays with compound initializers are not correctly initialized (kvorobyov) - closed.
- 0002213: [Plug-in > E-ACSL] Can't install E-ACSL plugin (signoles) - closed.

[2 issues]

Frama-C - Frama-C Aluminium (Released 2016-05-31) View Issues ]
=================================================
- 0002135: [Kernel > libc] sigsetjmp and siglongjmp in setjmp.h (maroneze) - closed.
- 0002146: [Kernel] Frama-C does not support standard C digraphs (maroneze) - closed.
- 0001368: [Kernel] suggest to suppress "Neither code nor specification" warning for __builtin_va_start (valentin.perrelle) - closed.
- 0001367: [Documentation > ACSL] suggest to mention in acsl manual that \valid shouldn't be applied to function pointers (yakobowski) - closed.
- 0002183: [Documentation > ACSL] doubling of a word (maroneze) - closed.
- 0002159: [Plug-in > wp] alt-ergo: undefined symbol andb (correnson) - closed.
- 0002164: [Kernel > Makefile] Relocable buckx (yakobowski) - closed.
- 0002158: [Kernel > ACSL implementation] WP crashes on the given function (virgile) - closed.
- 0002132: [Plug-in > wp] Under windows, many times, Frama-c wp process doesn't kill alt-ergo process before finishing (correnson) - closed.
- 0002154: [Plug-in > wp] Zombie processes (correnson) - closed.
- 0002217: [Kernel] Frama-c accepts assigning formal parameters when a range is used (virgile) - closed.
- 0002218: [Kernel > ACSL implementation] Specification for sigsetjmp is invalid (virgile) - closed.
- 0001790: [Plug-in > jessie] Crash when running "frama-c -jessie -jessie-atp=gui reduce.c" (yakobowski) - closed.
- 0001179: [Plug-in > wp] Suggest to supply values of global consts to provers (correnson) - closed.
- 0002201: [Plug-in > wp] Unexpected error (Invalid_argument("Z.shift_left: count argument must be positive")) (correnson) - closed.
- 0001968: [Plug-in > value analysis] Values inferred for 32-bit variable do not fit in 32-bit type (valentin.perrelle) - closed.
- 0002155: [Plug-in > wp] coq fails to compile Cint because Zbits is not found (patrick) - closed.
- 0002214: [Plug-in > wp] Reals are bad encoded for coq (correnson) - closed.
- 0002203: [Documentation > ACSL] LoopEntry vs LoopInit (virgile) - closed.

[19 issues]

Frama-C - Frama-C Magnesium (Released 2016-01-18) View Issues ]
=================================================
- 0001771: [Documentation] quality of pdf files (correnson) - closed.
- 0002204: [Documentation] provide "Magnesium" product version in the BTS (signoles) - closed.
- 0002161: [Kernel] redefinition of __STDC_VERSION__ (yakobowski) - closed.
- 0002098: [Kernel > ACSL implementation] overloading of predicate fails (virgile) - closed.
- 0002119: [Kernel] "If" statement with only one successor (yakobowski) - closed.
- 0002184: [Plug-in > wp] memory leak (endless recursion?) caused by erroneous c program (signoles) - closed.
- 0002171: [Kernel > libc] redefinition of size_t, time_t, FILE (maroneze) - closed.
- 0002131: [Kernel] Error with casted ternary statements (yakobowski) - closed.
- 0001939: [Kernel > libc] Specification of the read function (maroneze) - closed.
- 0002144: [Plug-in > wp] crash in presence of \result in assigns (correnson) - closed.
- 0000876: [Plug-in > value analysis] Widen hints for a variable should not influence the values for other variables (yakobowski) - closed.
- 0001022: [Documentation > ACSL] suggest to explain semantics of missing loop assigns clause in Acsl manual (patrick) - closed.
- 0002021: [Documentation > ACSL] Incorrect grammar for loop-behavior in document (patrick) - closed.
- 0002040: [Plug-in > wp] assumes clause and labels (correnson) - closed.
- 0001553: [Kernel > ACSL implementation] Fails to cope with multiple non-contiguous constant array instantiations (yakobowski) - closed.
- 0002141: [Plug-in > wp] Incorrect result with X modulo 1 (correnson) - closed.
- 0002082: [Plug-in > wp] Crash with \is_infinite (correnson) - closed.
- 0002115: [Documentation > ACSL] Typos and Grammatical corrections for the ACSL 1.9 manual (patrick) - closed.
- 0002114: [Documentation > ACSL] ACSL manual:issues affecting technical correctness or understanding (patrick) - closed.
- 0002143: [Documentation > ACSL] Incorrect grammar of Predicate Application and Function Application (patrick) - closed.
- 0001683: [Plug-in > wp] Number of discharged Qed goals counted multiple times (correnson) - closed.
- 0002090: [Kernel] unary negation of enum constant always yield 0 (yakobowski) - closed.
- 0002117: [Kernel] frama-c gets confused by comma operator inside ternary operator: cannot cast from void to char (yakobowski) - closed.
- 0002121: [Kernel] Symbolic links in tar ball (bobot) - closed.
- 0002126: [Plug-in > wp] WP crashes on generation of PO for assigns clause (assertion failure in MemVar.ml) (correnson) - closed.
- 0002127: [Plug-in > wp] Unprovable inequality involving (unsigned) -1 (correnson) - closed.
- 0000875: [Plug-in > value analysis] suggest to issue a warning on (<)-comparisons between pointers, unless both are non-null (yakobowski) - closed.

[27 issues]

Frama-C - Frama-C Sodium (Released 2015-03-17) View Issues ]
==============================================
- 0001098: [Documentation] Non working example in the documentation (virgile) - closed.
- 0001732: [Documentation > manuals] Erreur dans la documentation pour plugin erreur de type (signoles) - closed.
- 0001731: [Documentation] Erreur dans la documentation pour plugin contradiction sur nom de fichiers (signoles) - closed.
- 0001822: [Documentation > manuals] Manuals are not in the distribution (bobot) - closed.
- 0001979: [Documentation > manuals] Bug in example - plugin documentation (Matthieu Lemerre) - closed.
- 0001782: [Documentation > manuals] wrong link in e-acsl documentation (signoles) - closed.
- 0001784: [Documentation > ACSL] typo in grammar (patrick) - closed.
- 0001636: [Plug-in > E-ACSL] E-ACSL: executes "__store_block()" but never "__delete_block()"! (signoles) - closed.
- 0001837: [Plug-in > E-ACSL] Literal strings can be added multiple times in memory (signoles) - closed.
- 0001688: [Plug-in > wp] CVC4 results are not displayed in the GUI (correnson) - closed.
- 0001788: [Documentation > ACSL] predicate-def and logic-predicate-def (virgile) - closed.
- 0001907: [Plug-in > value analysis] Value abort because of Zero-sized location (yakobowski) - closed.
- 0001919: [Graphical User Interface] Segmentation fault when launching frama-c-gui with OCaml 4.02.0 (yakobowski) - closed.
- 0001922: [Plug-in > wp] WP-Plugin crashes due to an internal error (correnson) - closed.
- 0002067: [Plug-in > wp] Frama-C does not work with versions of Why3 newer than 0.83 (bobot) - closed.
- 0001485: [Graphical User Interface] Bullet colors are unreadable for color blind people (guillaume-petiot) - closed.
- 0002020: [Plug-in > PathCrawler] body of atomic cond belonging to an assume reproduced in sequence containing the assume (muriel) - closed.
- 0001276: [Kernel] Capitalized filename in Dynamic.load_module (virgile) - closed.
- 0001768: [Plug-in > slicing] Crah with the option -ulevel (patrick) - closed.
- 0001751: [Plug-in > wp] Frama-C/WP "forgets" a proven assertion (patrick) - closed.
- 0001828: [Plug-in > wp] Frame Validity (patrick) - closed.
- 0001832: [Plug-in > wp] typo in wp output: "interruped"-->"interrupted" (correnson) - closed.
- 0001853: [Kernel] bogus syntax error with doxygen (yakobowski) - closed.
- 0001857: [Plug-in > value analysis] Crash on invalid -val-split-return-function option (yakobowski) - closed.
- 0001901: [Kernel] Crash when merging contracts for duplicated functions with different formal parameters names (virgile) - closed.
- 0001908: [Plug-in > value analysis] Non terminating call to stncpy (yakobowski) - closed.
- 0001930: [Plug-in > wp] Status of POs: the word "interruped" should be "interrupted" (correnson) - closed.
- 0001670: [Plug-in > wp] WP ignores some goals when 'initialized' is used in hypotheses (correnson) - closed.
- 0001630: [Plug-in > wp] Make identifiers in Coq proofs more similar to those from C code (correnson) - closed.
- 0001647: [Plug-in > wp] compatibility between \null in ACSL and NULL in C in wp (correnson) - closed.
- 0001729: [Kernel] "char const * const *" causes syntax error (virgile) - closed.
- 0001764: [Kernel] Port to OCamlgraph 1.8.5 (bobot) - closed.
- 0001765: [Kernel] Spelling errors in binary (signoles) - closed.
- 0001750: [Plug-in > wp] Frama-C/WP fails to discharge simple bit operation for small integer types (patrick) - closed.
- 0001767: [Plug-in > wp] Problem when arguments are not used in predicates (correnson) - closed.
- 0001776: [Plug-in > wp] Assert erroneously proved valid (correnson) - closed.
- 0001770: [Kernel > configure] Cannot switch to local version if OCamlgraph is already installed (virgile) - closed.
- 0001779: [Plug-in > wp] Crash when using wpo api get_result (virgile) - closed.
- 0001789: [Kernel > ACSL implementation] Crashes when using logic in assigns statement (correnson) - closed.

[39 issues]

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 > value analysis] 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 > value analysis] 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 > value analysis] Logging just enough information for failed pre-conditions (yakobowski) - closed.
- 0001435: [Plug-in > value analysis] 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 > value analysis] 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 > value analysis] 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 > value analysis] 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 > value analysis] 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 > value analysis] 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 > value analysis] 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 > value analysis] Value analysis: bad type conversion plus unassigned fields in a struct leads to crash (yakobowski) - closed.

[64 issues]

Frama-C - Frama-C Fluorine-20130601 (Released 2013-06-19) View Issues ]
=========================================================
- 0001478: [Plug-in > E-ACSL] E-ACSL reports use of invalid pointer while in fact the pointer is valid (signoles) - closed.
- 0001437: [Kernel] Cannot use Frama_C_interval on Fluorine (signoles) - closed.

[2 issues]

Frama-C - Frama-C Fluorine-20130501 (Released 2013-05-23) View Issues ]
=========================================================
- 0001424: [Plug-in > value analysis] Different signed_overflow assert with rte + val (yakobowski) - closed.

[1 issue]

Frama-C - Frama-C Fluorine-20130401 (Released 2013-04-19) View Issues ]
=========================================================
- 0001335: [Documentation] new link to ACSL by Example (patrick) - closed.
- 0001334: [Documentation] Fraunhofer FIRST -> Fraunhofer FOKUS (patrick) - closed.
- 0001284: [Kernel] Copy visitor builds an inconsistent AST on clause 'frees' (virgile) - closed.
- 0001277: [Kernel] Datatype.triple is missing (signoles) - closed.
- 0001282: [Kernel] [Visitor] Cil.JustCopy does not work on functions with contracts (virgile) - closed.
- 0001287: [Kernel] no hook table for parameter -plevel (signoles) - closed.
- 0001290: [Plug-in > aoraï] aorai doesn't enrich user's "loop assigns" by generated internal variables (virgile) - closed.
- 0001295: [Kernel] bad help printing for option when invisible and has negative option (signoles) - closed.
- 0001309: [Kernel > ACSL implementation] Incorrect typing of term conditional over floats (virgile) - closed.
- 0001316: [Plug-in > wp] false property proved intTyped (if confirmed) (correnson) - closed.
- 0001343: [Kernel > Makefile] "make clean" does not work when upgrading OCaml (signoles) - closed.
- 0001360: [Plug-in > wp] \valid_read and assigns (correnson) - closed.
- 0000856: [Plug-in > value analysis] non-constant size of 2-dim array leads to crash (some similarities to issue 0000852) (yakobowski) - closed.
- 0001355: [Plug-in > wp] WP computation is looping during variable analysis (yakobowski) - closed.
- 0001359: [Documentation > ACSL] duplicate entries in index of acsl documentation (virgile) - closed.
- 0001385: [Kernel] Compilation crash if ocamllex.opt not installed (signoles) - closed.
- 0000722: [Kernel > ACSL implementation] bitwise operator (virgile) - closed.
- 0000915: [Plug-in > value analysis] interest for a built-in memset function (yakobowski) - closed.
- 0001127: [Kernel] Error in Type.pp_ml_name with Datatype.String.Set.ty (signoles) - closed.
- 0000090: [Plug-in > slicing] Remove generated annotations from slicing results (yakobowski) - closed.
- 0001364: [Plug-in > value analysis] strange warning "extracting bits of a pointer" (yakobowski) - closed.
- 0000862: [Kernel > ACSL implementation] ACSL parser + pretty-printer (virgile) - closed.
- 0001213: [Kernel] suggest to forbid unknown functions by default (virgile) - closed.
- 0001119: [Plug-in > wp] couldn't verify series of struct member initializations (correnson) - closed.
- 0000794: [Plug-in > wp] initial value of strings (correnson) - closed.
- 0000793: [Plug-in > wp] time too long even with -wp-timeout 1 (dargaye) - closed.
- 0000992: [Plug-in > wp] Wrong WP computation when calling a function with behaviors (assigns problem ?) (correnson) - closed.
- 0001038: [Plug-in > wp] lemma tacitly ignored in absense of C code (correnson) - closed.
- 0001264: [Plug-in > value analysis] Locations.valid_enumerate_bits enumerate invalid bits (yakobowski) - closed.
- 0001299: [Plug-in > wp] unproven property used in a behavior in Typed model (correnson) - closed.
- 0001293: [Plug-in > wp] proc name in assigns clause causes crash (correnson) - closed.
- 0001302: [Plug-in > value analysis] Crash with Invalid argument for Frama_C_alloc_size function (yakobowski) - closed.
- 0001328: [Kernel > ACSL implementation] Incorrect AST in presence of local ghost variables (virgile) - closed.
- 0001348: [Plug-in > wp] performance problem about number of fields in structure for struct equality properties (correnson) - closed.
- 0001372: [Plug-in > value analysis] Extern function vs extern variable to get a random value (yakobowski) - closed.

[35 issues]

Frama-C - Frama-C Oxygen-20120901 (Released 2012-09-19) View Issues ]
=======================================================
- 0001085: [Documentation] Cute boolean options too cute for their own good (signoles) - closed.
- 0001014: [Documentation] gui and doc (signoles) - closed.
- 0001092: [Documentation > manuals] some typos etc. in the value-analysis manual (pascal) - closed.
- 0000991: [Documentation > manuals] outdated manual titles (virgile) - closed.
- 0001089: [Documentation > manuals] Updated example in plugin-development-guide (signoles) - closed.
- 0000419: [Documentation > manuals] Plug-in dev guide: tutorial for kernel integrated plug-in is out-of-date (signoles) - closed.
- 0001067: [Documentation > manuals] suggest to mention option "-value-help" in value analysis manual (pascal) - closed.
- 0001036: [Documentation > manuals] In section 5.11.5 of the Plugin developper manual : Reference to modules that neither appear in the API nor in Frama-c source. (signoles) - closed.
- 0001088: [Documentation > manuals] Plugin-development-guide section 2.1.2 (signoles) - closed.
- 0000745: [Kernel > ACSL implementation] Very big integer constants (virgile) - closed.
- 0001072: [Plug-in > value analysis] evaluation of && and || in term position (yakobowski) - closed.
- 0000759: [Plug-in > value analysis] wrong treatment for const arrays in lib-entry mode (pascal) - closed.
- 0001073: [Kernel] Some functions lose their formals after File.create_project_from_visitor (virgile) - closed.
- 0001100: [Kernel] Loop unrolling sub-optimal in presence of some labels (yakobowski) - closed.
- 0001099: [Kernel] Crash when parsing an incorrect program with pointer to arrays (virgile) - closed.
- 0000990: [Kernel] Crash with multiple incompatible declarations (virgile) - closed.
- 0000986: [Plug-in > wp] Wrong [\valid(p)] outside the pointed variable scope (correnson) - closed.
- 0001069: [Kernel > configure] Handling error in external plug-in through --enable-external (virgile) - closed.
- 0001023: [Documentation > ACSL] \valid_range not mentioned in Acsl manual (virgile) - closed.
- 0000999: [Kernel] Missing or misleading warnings when merging two functions (virgile) - closed.
- 0000993: [Plug-in > from] Incorrect dependencies in presence of declared functions (yakobowski) - closed.
- 0001009: [Kernel > ACSL implementation] code annotation placed above a local declaration are not correctly handled (virgile) - closed.
- 0001006: [Kernel] Kernel should desugar "complete behaviors" (virgile) - closed.
- 0001132: [Kernel] -cpp-extra-args option should be a list (signoles) - closed.
- 0001114: [Kernel] 17514, -unspecified-access and if (*p = (*p < 3)) (csmith) (virgile) - closed.
- 0001135: [Kernel] unrolling loop statements with labels into there annotations are not handled correctly (in conjunction with -ulevel) (patrick) - closed.
- 0001113: [Kernel] Preprocessing code may yield expanded code with undeclared variables (virgile) - closed.
- 0001126: [Kernel] AST check failure : problem with generated block-local variables (virgile) - closed.
- 0001136: [Kernel] [Globals.Vars.get_astinfo] doesn't work (virgile) - closed.
- 0001139: [Kernel] unrolling labeled loops (patrick) - closed.
- 0001116: [Kernel] axiom outside axiomatic tacitly ignored in presence of struct (virgile) - closed.
- 0001142: [Plug-in > value analysis] Bad AST generation ? (yakobowski) - closed.
- 0001144: [Kernel] 17944 using option -unspecified-access, no alarm for x + (x=0) (virgile) - closed.
- 0001145: [Kernel > Makefile] PLUGIN_LINK_GUI_OFLAGS not used ? (signoles) - closed.
- 0001024: [Plug-in > value analysis] Emitted assertion wrongly reduces to bottom (apparently) (csmith) (yakobowski) - closed.
- 0001110: [Kernel] Using Filter without Value (yakobowski) - closed.
- 0001165: [Kernel] [libc] erreur: #endif sans #if (virgile) - closed.
- 0001050: [Plug-in > aoraï] Sequence number generated by aorai is incorrect (virgile) - closed.
- 0001027: [Kernel > ACSL implementation] incompatible types for a correct spec (virgile) - closed.
- 0001056: [Kernel > ACSL implementation] Frama-c fails when Starting Jessie Translation (virgile) - closed.
- 0001066: [Plug-in > value analysis] suggest to use "NULL" rather than "&NULL" for null pointer (pascal) - closed.
- 0001082: [Kernel > Makefile] Bad links in generated documentation modules.svg (signoles) - closed.
- 0001079: [Plug-in > scope] Imprecision of 'Defs' when querying precise location (yakobowski) - closed.
- 0001071: [Plug-in > value analysis] relation chains exploited incompletely (pascal) - closed.
- 0001025: [Kernel] Cil.prepareCfg (or -simplify-cfg option) insert dummy locations in the ast (yakobowski) - closed.
- 0000107: [Plug-in > slicing] Slicer: slicing preserving some undesired function calls (yakobowski) - closed.
- 0000251: [Plug-in > value analysis] wrong origin displayed in the GUI (yakobowski) - closed.
- 0000728: [Kernel] Arguments are not checked when function call precedes function declaration (yakobowski) - closed.
- 0001214: [Plug-in > value analysis] FRAMA_C_MALLOC_INFINITE not used in stdlib.c (yakobowski) - closed.
- 0000840: [Kernel] syntax error message refers to (true error line + 5 lines) (virgile) - closed.
- 0001226: [Kernel] error with -pp-annot : eof while parsing C comment (virgile) - closed.
- 0001122: [Graphical User Interface] Opening consolidation graph crashes when 'dot' is missing (signoles) - closed.
- 0000932: [Kernel] Journalisation of dynamic functions using abstract types does not work (signoles) - closed.
- 0001254: [Kernel] Documentation for Cil.d_plaininit (signoles) - closed.
- 0001059: [Kernel] Undefined behavior with embedded assignment goes undetected (virgile) - closed.
- 0001104: [Graphical User Interface] value analysis warning disappears from 'Messages' window in gui after 'Reparse' button clicked (yakobowski) - closed.
- 0001070: [Kernel > configure] Getting frama-c version through --enable-external (virgile) - closed.
- 0001000: [Plug-in > value analysis] Evaluation in the logic can cause crashes (yakobowski) - closed.
- 0000679: [Plug-in > slicing] untypable ACSL in a sliced program containing \at(p,label) when the label was removed (Anne) - closed.
- 0000888: [Kernel] 14292: warn for unspecified side-effect that are separated by a function call (csmith) (virgile) - closed.
- 0001140: [Kernel] Strange declaration mismatch (monate) - closed.
- 0001261: [Plug-in > wp] Modules defined twice during WP compilation. (correnson) - closed.
- 0001128: [Kernel > Makefile] Install frama-c.top (signoles) - closed.
- 0001274: [Kernel] Things get mixed-up between project (yakobowski) - closed.
- 0000239: [Plug-in > jessie] internal error when analyzing max.h (correnson) - closed.
- 0001004: [Plug-in > jessie] Jessie reports syntax error in .mlw file (cmarche) - closed.
- 0001158: [Plug-in > jessie] inlining of assembleur is not supported (cmarche) - closed.
- 0001149: [Plug-in > jessie] function names are restricted due to exclusion of ACSL keywords (virgile) - closed.
- 0001251: [Plug-in > jessie] Binary search doesn't verify anymore after upgrade (cmarche) - closed.
- 0001265: [Plug-in > jessie] Function with name shift produces error (virgile) - closed.
- 0001003: [Plug-in > jessie] conditional expression (?:) raises uncaught exception under why-2.30 (cmarche) - closed.
- 0001182: [Graphical User Interface] Project menu is empty when Ubuntu/Unity is enabled (monate) - closed.
- 0001117: [Plug-in > wp] addr_eq versus = and <> in generated axioms access_update, access_update_neq (pherrmann) - closed.
- 0000384: [Kernel] Labels in loops are not unrolled (virgile) - closed.
- 0000594: [Kernel] Kernel error with RTE generated annotations: invalid operands (bitwise) (virgile) - closed.
- 0000672: [Kernel] Incorrect cil merging in presence of ACSL annotations (virgile) - closed.
- 0000685: [Kernel] CIL's added return masks issues (virgile) - closed.
- 0000895: [Plug-in > wp] Proof obligations of lemma properties (correnson) - closed.
- 0000764: [Kernel] Specifying several directories in environment variables FRAMAC_* (signoles) - closed.
- 0000989: [Plug-in > syntactic callgraph] Strange dot callgraphs (signoles) - closed.
- 0001001: [Plug-in > value analysis] Invalid handling of shift of pointer address (pascal) - closed.
- 0000997: [Plug-in > value analysis] Warnings in presence of Top floats (yakobowski) - closed.
- 0001005: [Kernel] defining two axioms with same name causes kernel crash (virgile) - closed.
- 0001013: [Kernel] Crash when casting something to type void (yakobowski) - closed.
- 0001021: [Graphical User Interface] request for pretty printing only one property by lines (yakobowski) - closed.
- 0001028: [Plug-in > wp] unable to prove that comparison-result is 0 or 1: insufficient axiomatization of eq_int_bool? (correnson) - closed.
- 0001026: [Plug-in > value analysis] value analysis memory consumption problem when using -lib-entry option (yakobowski) - closed.
- 0001074: [Plug-in > value analysis] Imprecise result on almost deterministic program (pascal) - closed.
- 0001081: [Kernel] foo ? (void)x : (signed char)y (csmithreduction) (virgile) - closed.
- 0001076: [Plug-in > value analysis] "volatile" ignored (pascal) - closed.
- 0001083: [Plug-in > RTE] RTE does not check for downcast of unsigned integer (pherrmann) - closed.
- 0001108: [Plug-in > wp] Bitwise Operators (correnson) - closed.
- 0001102: [Graphical User Interface] Rename frama-c-gui.config (monate) - closed.
- 0001141: [Kernel] incorrect UINT8_MAX (and others) (monate) - closed.
- 0001162: [Kernel > ACSL implementation] "for" clause is refused (virgile) - closed.
- 0001180: [Kernel] Port to OCamlgraph 1.8.2 (signoles) - closed.
- 0001194: [Plug-in > scope] imprecision in PDG when unreachable statements (yakobowski) - closed.
- 0001225: [Plug-in > wp] Upgrading WP causes crash in Jessie (signoles) - closed.
- 0001243: [Kernel] two axioms with same name cause crash (yakobowski) - closed.
- 0001263: [Kernel] Identical lvals not equal in Cil_datatype.Lval.Hashtbl (virgile) - closed.
- 0001273: [Kernel] Parser does not complain about superfluous } (virgile) - closed.

[101 issues]

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 > value analysis] possible unsoundness bug (pascal) - closed.
- 0000718: [Plug-in > value analysis] 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 > value analysis] 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 > 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.
- 0000754: [Kernel > Makefile] Dynamic plugin doc (virgile) - closed.
- 0000774: [Plug-in > slicing] Slicing is sometimes not journalisable anymore (signoles) - closed.
- 0000689: [Plug-in > value analysis] 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 > value analysis] 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 > value analysis] 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 > value analysis] 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 > value analysis] 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 > value analysis] 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 > value analysis] 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 > value analysis] 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 > value analysis] 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 > 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.
- 0000949: [Plug-in > value analysis] 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 > value analysis] Use of Cabs2cil.fresh_global (pascal) - closed.
- 0000715: [Plug-in > value analysis] 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 > value analysis] 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 > value analysis] 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]

Frama-C - Frama-C Carbon-20110201 (Released 2011-08-02) View Issues ]
=======================================================
- 0000645: [Kernel] lose of location displayed by Cil.warning (monate) - closed.
- 0000637: [Kernel > Makefile] actions done with make install -n (svn 10897) (signoles) - closed.
- 0000635: [Kernel] losing messages doing save/load (signoles) - closed.
- 0000666: [Graphical User Interface] Wrong evaluation of expression in the GUI (pascal) - closed.
- 0000673: [Plug-in > slicing] untypable ACSL in a sliced program containing \result (patrick) - closed.
- 0000677: [Kernel] Help options are wrongly described as "aliases" when they have the same description. (signoles) - closed.
- 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.
- 0000646: [Plug-in > wp] [wp] warning: Stronger goal store_AppelerVerifier_post_6 (1 warning) (dargaye) - closed.
- 0000662: [Plug-in > wp] warning: Degenerated goal (dargaye) - closed.
- 0000665: [Plug-in > wp] Unexpected error (Stack overflow) during WP (correnson) - closed.
- 0000701: [Plug-in > wp] Unexpected error (Failure("int_of_string")). (correnson) - closed.
- 0000710: [Plug-in > slicing] Crash during slicing (Anne) - closed.
- 0000630: [Kernel] bad location with tmp CIL variable (virgile) - closed.
- 0000647: [Kernel > configure] lib apron not found in configure (signoles) - closed.

[15 issues]

Frama-C - Frama-C Carbon-20101202-beta2 (Released 2010-12-17) View Issues ]
=============================================================
- 0000299: [Plug-in > jessie] Frama-C stops with unexpected failure (Ref. "norm.ml:1105:8") (cmarche) - closed.
- 0000404: [Plug-in > jessie] Jessie translation unexpected failure (cmarche) - closed.
- 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.
- 0000363: [Plug-in > jessie] Plugin jessie aborted because of an internal error. (cmarche) - closed.
- 0000427: [Plug-in > jessie] Jessie crashes on \old(*ptr) (cmarche) - closed.
- 0000434: [Plug-in > jessie] assertion at line 2772 of jc/jc_typing.ml fails (cmarche) - closed.
- 0000426: [Plug-in > jessie] Jessie internal error (cmarche) - closed.
- 0000509: [Plug-in > jessie] Unexpected exception if no input file (cmarche) - closed.
- 0000537: [Plug-in > jessie] Predicate Sorted causes crash (norm.ml:1524:10) (cmarche) - closed.
- 0000476: [Plug-in > jessie] Partial support of tset leads to assert failure (cmarche) - closed.
- 0000500: [Plug-in > jessie] Uncaught exception in jc/jc_effect.ml caused by union type (cmarche) - closed.
- 0000523: [Plug-in > jessie] struct-type expression in loop-assigns causes crash (cmarche) - closed.
- 0000530: [Plug-in > jessie] crash (cmarche) - closed.

[16 issues]

Frama-C - Frama-C Carbon-20101201-beta1 (Released 2010-12-14) View Issues ]
=============================================================
- 0000554: [Documentation] Logic_utils and Logic_const documentation ... (signoles) - closed.
- 0000595: [Documentation] Implementation <-> Documentation Inconsistency (virgile) - closed.
- 0000474: [Documentation] Multiple definition of function iter_stmt (signoles) - closed.
- 0000339: [Documentation] wrong option name in Jessie Plugin Tutorial (signoles) - closed.
- 0000365: [Documentation > manuals] Jessie tutorial binary_search examples fail with Why 2.23 - loop variant must be added (cmarche) - 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.
- 0000448: [Plug-in > slicing] invariant with quantifier not kept in computed slice (Anne) - 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.
- 0000470: [Graphical User Interface] In the GUI, it is impossible to talk about variables generated by Value's -lib-entry (pascal) - closed.
- 0000484: [Kernel > ACSL implementation] function and statement behaviors (patrick) - closed.
- 0000489: [Kernel] Cint64 user constants have no textual representation (virgile) - closed.
- 0000451: [Kernel] Crash when a 'break' occurs outside a proper statement (virgile) - closed.
- 0000440: [Plug-in > jessie] Pb with annot.c in (virgile) - closed.
- 0000452: [Kernel] "Body of function main falls-through" warning could be improved (virgile) - closed.
- 0000472: [Plug-in > value analysis] Comparing a function pointer will NULL might raise incorrect warning (pascal) - closed.
- 0000505: [Kernel > ACSL implementation] Predicate/Functions depending only on a state are not handled correctly (virgile) - closed.
- 0000510: [Plug-in > jessie] Jessie generates error when called to be executed. (signoles) - closed.
- 0000524: [Kernel] Missing declared inline functions in Globals (monate) - closed.
- 0000519: [Kernel] int t[static 2] is not supported as function argument (virgile) - closed.
- 0000528: [Kernel > Makefile] Makefile.dynamic should always write to $(DESTDIR) (signoles) - closed.
- 0000550: [Plug-in > occurrence] Selecting "occurrence" crashes Frama-C (signoles) - closed.
- 0000541: [Kernel > ACSL implementation] When using -pp-annot and including stdbool.h, can't parse \false in annotations (virgile) - closed.
- 0000512: [Kernel] suggest to refer to fct-contract's clauses-order in error message (virgile) - closed.
- 0000506: [Kernel] line command option for doCollapseCallCast configuration (virgile) - closed.
- 0000549: [Kernel > ACSL implementation] Typing problem into the logic about C variable of an array type. (virgile) - closed.
- 0000568: [Kernel > ACSL implementation] cast to const type not handled in acsl annotations (virgile) - closed.
- 0000570: [Kernel > ACSL implementation] Incorrect typing of annotations (virgile) - closed.
- 0000588: [Kernel] Error when function contract defined after function definition and with different parameter names (virgile) - closed.
- 0000612: [Documentation > ACSL] Mention that invariant does not hold after for-loop (virgile) - closed.
- 0000634: [Plug-in > value analysis] Superfluous ';' in value analysis output (pascal) - closed.
- 0000548: [Kernel] Header limit.h is nonsense (pascal) - closed.
- 0000482: [Kernel > ACSL implementation] for behav : invariant INV ; (patrick) - closed.
- 0000569: [Graphical User Interface] Stoping external process (why) (monate) - closed.
- 0000462: [Kernel > Makefile] Makefile.dynamic should not change known_plugins.ac (virgile) - closed.
- 0000525: [Kernel] inchoherence of types between enumitems and enum type with multi-files (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.
- 0000552: [Kernel] Checking number of arguments passed to C functions (virgile) - closed.
- 0000584: [Plug-in > jessie] incorrect(?) jessie code generated from strcpy (cmarche) - closed.
- 0000620: [Kernel] Default assigns generation (patrick) - closed.

[42 issues]

Frama-C - Frama-C Boron-20100401 (Released 2010-04-13) View Issues ]
======================================================
- 0000314: [Plug-in > value analysis] 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 > value analysis] Incorrect 'assert false' in value analysis (monate) - closed.
- 0000406: [Plug-in > jessie] assert false (* TODO *) (cmarche) - closed.
- 0000381: [Plug-in > value analysis] propagation of \result clauses (pascal) - 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.
- 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 > value analysis] 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.
- 0000370: [Plug-in > jessie] pragma JessieIntegerModel (cmarche) - closed.
- 0000361: [Plug-in > jessie] "why" reports "unbound label" (cmarche) - closed.
- 0000367: [Plug-in > jessie] bug with constants like 1E-6 (cmarche) - closed.
- 0000420: [Plug-in > jessie] same formula translated differently as axiom/lemma (cmarche) - closed.
- 0000391: [Plug-in > jessie] Why keywords as ACSL identifiers (cmarche) - closed.
- 0000386: [Plug-in > jessie] int32 and real can't be unified (cmarche) - closed.
- 0000399: [Plug-in > jessie] Statement contract and "hiding" of statement (cmarche) - closed.
- 0000443: [Plug-in > jessie] assigns clause unchecked on arrays (cmarche) - 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 > value analysis] imprecision in widening/narrowing for char and short index (pascal) - closed.
- 0000358: [Kernel > ACSL implementation] redeclaration as different kind of symbol (yakobowski) - closed.
- 0000435: [Plug-in > syntactic callgraph] Too many edges in call graph (signoles) - closed.
- 0000385: [Kernel] File "src/kernel/cilE.ml", line 372, characters 13-19: Assertion failed (virgile) - closed.
- 0000393: [Plug-in > slicing] assigns clauses are missing from the sliced program (Anne) - closed.
- 0000392: [Plug-in > value analysis] Failure("Function 'From.find_deps_no_transitivity' not registered yet") (pascal) - closed.
- 0000376: [Plug-in > jessie] unsigned long long constant becomes signed (cmarche) - closed.
- 0000332: [Kernel] goto generated by Frama-C and not supported by Jessie (virgile) - closed.
- 0000309: [Kernel > ACSL implementation] After ./confugure with --disable-all-staff options and make static, frama-c-Myplugin.byte crashes (virgile) - closed.
- 0000364: [Plug-in > jessie] complete/disjoint behaviors shouldn't accept undefined behaviors (virgile) - closed.
- 0000372: [Plug-in > value analysis] Wrong postconditions are "valid according to value analysis" (virgile) - closed.

[42 issues]

Frama-C - Frama-C Beryllium-20090902 (Released 2009-09-23) View Issues ]
==========================================================
- 0000170: [Documentation > manuals] Impossible to pass option to jessie or why through jessie plugin (correnson) - closed.
- 0000285: [Plug-in > jessie] jessie problem - closed.
- 0000242: [Graphical User Interface] 'Go to definition' and 'Go to caller' do not update main view of GUI (monate) - closed.
- 0000068: [Plug-in > value analysis] Plug-in inout fails to parse clause /*@ assigns s[..]; */ (pascal) - closed.
 - 0000230: [Kernel] Missing functions to convert logic terms directly to abstract values (pascal) - closed.
- 0000234: [Kernel] Wrong display of call stacks in value analysis (correnson) - closed.
- 0000238: [Graphical User Interface] Files of a project state not displayed on reload in GUI (monate) - closed.
- 0000236: [Graphical User Interface] Error when linking the viewer (signoles) - closed.
- 0000223: [Kernel] -warn-unspecified-order false positive (virgile) - closed.
- 0000250: [Plug-in > obfuscator] obfuscator loses link between logic and C variables (monate) - closed.
- 0000253: [Kernel] Extlib.deprecated does not use Log.* to print messages (correnson) - closed.
- 0000237: [Graphical User Interface] Warning repetition in Messages window (correnson) - closed.
- 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.
- 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.
- 0000224: [Kernel] Non-exhaustive pattern matching leads to compilation error (signoles) - closed.

[19 issues]

Frama-C - Frama-C Beryllium-20090901 (Released 2009-09-02) View Issues ]
==========================================================
- 0000180: [Kernel] Save/Load elapsed time (pascal) - closed.
- 0000184: [Plug-in > slicing] slicing crashes when there is no entry point to the function (Anne) - closed.
- 0000193: [Plug-in > slicing] crash with information [kernel] error: unexpected error Extlib.NotYetImplemented("[logic_interp] not a lvalue") (correnson) - closed.
- 0000189: [Kernel] the configure script does not work properly with libocamlgraph-ocaml-dev 1.1-1 (signoles) - closed.
- 0000169: [Kernel] Build fails due to Printexc.record_backtrace (signoles) - closed.
- 0000200: [Kernel] Error while linking lib/plugins/Jessie.cmo (signoles) - closed.
- 0000216: [Plug-in > scope] Uncaught exception in scope (pascal) - closed.
- 0000192: [Kernel] -ocode causes crach (pascal) - closed.
- 0000198: [Kernel] Packing for dynamic plug-in is not done in current directory (signoles) - closed.
- 0000195: [Plug-in > value analysis] wrongly synthesized assert (pascal) - closed.
- 0000197: [Kernel] Options <plug-in>-debug and <plug-in>-verbose for dynamic plug-ins do not work (signoles) - closed.
- 0000211: [Kernel] "make doc" error (signoles) - closed.
- 0000182: [Kernel] The file `share/configure.ac' is missing (virgile) - closed.
- 0000225: [Graphical User Interface] Incorrect linking order for the viewer (signoles) - closed.
- 0000190: [Plug-in > slicing] crash when unbound variable (patrick) - closed.
- 0000163: [Kernel] crash for untyped_metrics example plugin (monate) - closed.
- 0000183: [Kernel] 'make top' fails (virgile) - closed.

[17 issues]

Frama-C - Frama-C Beryllium-20090601-beta1 (Released 2009-06-23) View Issues ]
================================================================
- 0000059: [Kernel] code normalisation issue when return variable is named __retres (monate) - closed.
- 0000060: [Kernel] Conversion from integer to real (virgile) - closed.
- 0000062: [Kernel] integer is not well-casted in real (virgile) - closed.
- 0000076: [Plug-in > value analysis] int a; main(){ return 100 / (int)(&a + 2); } fails to report a division by zero (pascal) - closed.
- 0000077: [Plug-in > value analysis] if((int)(&a+2)) fails to warn about being unspecified (pascal) - closed.
- 0000115: [Plug-in > aoraï] problem for making dynamic plugin (signoles) - closed.
- 0000148: [Kernel] cmdline.ml assertion error at line 88 (signoles) - closed.
- 0000088: [Kernel] Frama-C should stop on error in annotations instead of issuing a warning (virgile) - closed.
- 0000160: [Plug-in > jessie] \at(...,Post) in assigns clause (cmarche) - closed.
- 0000096: [Kernel] "logic set<struct something *> f(...)" throw a syntax error (virgile) - closed.
- 0000111: [Kernel] Compilation error if options --with-jessie-static --with-ltl_to_acsl-static are present. (signoles) - closed.
- 0000046: [Plug-in > jessie] Jessie/GWhy/Gappa: format file and invalid POs proved valid (cmarche) - closed.
- 0000073: [Plug-in > jessie] A pure predicate in an axiomatic with some "unpure" axioms have some strange results (cmarche) - closed.
- 0000028: [Plug-in > jessie] Jessie-gui : call of coqide and --project option (cmarche) - closed.
- 0000094: [Plug-in > jessie] "assert i >= 0;" not proven for unsigned char (cmarche) - closed.
- 0000095: [Plug-in > jessie] "//@ assert i >= CHAR_MIN;" not proven for char (cmarche) - closed.
- 0000117: [Kernel] int -> integer -> real (virgile) - closed.
- 0000029: [Plug-in > jessie] Lithium fool the tool (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.
- 0000061: [Kernel] frama-c --help (signoles) - closed.
- 0000049: [Plug-in > jessie] Jessie/Gwhy: cpulimit-win.c (cmarche) - closed.

[22 issues]

Frama-C - Frama-C GIT, precise the release id (Released 2005-12-09) View Issues ]
===================================================================
- 0002322: [Kernel] repeated predicate definitions in separate file cause crash (virgile) - resolved.
- 0001467: [Kernel] Parser does not handle mixed concatenations of wide and non-wide strings (valentin.perrelle) - resolved.
- 0002325: [Graphical User Interface] Make it build on bytecode architectures (maroneze) - closed.
- 0002323: [Documentation] Spelling errors (virgile) - closed.
- 0002249: [Kernel] __attribute__((aligned(0))) tacitly causes sizeof computation to fail (maroneze) - closed.

[5 issues]


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker