Frama-C Bug Tracking System - All Projects

Word 2000 Word View

Viewing Issues( 1 - 275 )
  PID # Attachment count CategorySeverityStatusUpdatedSummary
 0002414    [Frama-C]
Plug-in > wp
majorassigned (correnson)2018-12-07Mk_addr not defined in Memory.v (coqwp via why3ide)
 000241321 [Frama-C]
Plug-in > E-ACSL
majorconfirmed (signoles)2018-12-06missing E-ACSL code when ignoring asm annotation
 0002389162 [Frama-C]
Plug-in > wp
crashassigned (correnson)2018-12-06Failure to detect qed libraries when running wp
 000241221 [Frama-C]
Plug-in > RTE
crashconfirmed (signoles)2018-12-03E-ACSL crash with RTE generated assertion with booleans
 0001648    [Frama-C]
Kernel
majorassigned (maroneze)2018-11-30Wrong specification for standard library function memmove
 0001809    [Frama-C]
Kernel
tweakassigned (maroneze)2018-11-30Frama-C should not have unimplemented headers
 0002378    [Frama-C]
ptests
minorassigned (bobot)2018-11-30Bytecode only compilation fails when linking to stdlib
 000240941 [Frama-C]
Plug-in > wp
crashconfirmed (correnson)2018-11-30crash
 000240711 [Frama-C]
Plug-in > wp
majorassigned (correnson)2018-10-31contracts about memory mapped I/O through volatile memory locations
 000240431 [Frama-C]
Plug-in > wp
minorassigned (correnson)2018-10-09Shape of VC depends on selection of properties
 00024023   [Frama-C]
Plug-in > clang
blockassigned (virgile)2018-10-03frama-clang fails to compile
 0002310 1 [Frama-C]
Plug-in > E-ACSL
minorassigned (fmaurica)2018-10-02Incorrect handling of \initialized when initialized struct is passed to a function by value
 000240142 [Frama-C]
Plug-in > wp
majoracknowledged (correnson)2018-10-02Newer releases of FramaC produce apparent WP plug-in bug
 00023952   [Frama-C]
Plug-in > clang
minorassigned (virgile)2018-09-07const fields in constructors
 000229021 [Frama-C]
Plug-in > wp
minorassigned (correnson)2018-09-06incomplete loading of saved state when using WP?
 00023971   [Frama-C]
Kernel > ACSL implementation
featureassigned (virgile)2018-08-27Model Variables in Frama C
 0002396    [Frama-C]
Plug-in > clang
minorassigned (virgile)2018-08-24cast error with reference fields
 0002394 1 [Frama-C]
Plug-in > wp
majorassigned (correnson)2018-08-23conditional input annotations result in why3 type errors
 000239081 [Frama-C]
Plug-in > wp
minorfeedback (correnson)2018-07-25dubious discharge of postcondition
 000238231 [Frama-C]
Kernel
minorassigned (virgile)2018-07-10handling of escape sequences
 000238511 [Frama-C]
Plug-in > wp
crashassigned (correnson)2018-07-06Auto-generated assigns clause for a void* argument crashes wp
 0002376 1 [Frama-C]
Plug-in > jessie
crashassigned (cmarche)2018-05-29frama-c/jessie crashes with Unexpected error (Cil.SizeOfError("Undefined sizeof on a function.", _)).
 000237221 [Frama-C]
Kernel > configure
majorassigned (virgile)2018-03-28coq and ocaml conflict
  000237111 [Frama-C]
Plug-in > wp
featureassigned (correnson)2018-03-26suggest to provide results of commandl-line "-wp-prop" evaluation in a file in the wp-out directory
 0002370    [Frama-C]
Kernel > ACSL implementation
featureassigned (virgile)2018-03-08Expose ACSL annotations through host language pragmas
 00023698   [Frama-C]
Plug-in > E-ACSL
minoracknowledged (signoles)2018-02-23e-acsl-gcc failes on macOS
 0002194    [Frama-C]
Plug-in > E-ACSL
minorassigned (fmaurica)2018-02-22Failure to record global variable with initialiser
 00023271   [Frama-C]
Plug-in > E-ACSL
minorassigned (fmaurica)2018-02-22Failure to detect overflows into an allocated area within a struct
 000236711 [Frama-C]
Plug-in > clang
minorassigned (virgile)2018-02-12C-function returning a struct causes warning on missing Ctor code/spec when inside 'extern "C" {...}'
 0002366 1 [Frama-C]
Plug-in > clang
minorassigned (virgile)2018-02-12loop assigns clause ginored under strange circumstances
 0002365 1 [Frama-C]
Plug-in > clang
minorassigned (virgile)2018-02-12user-defined type not accepted after builtin type in quantifier chain
  0002364 1 [Frama-C]
Plug-in > clang
featureassigned (virgile)2018-02-12Frama-clang reports overloading ambiguity where Frama-C doesn't
 0002363 1 [Frama-C]
Plug-in > clang
minorassigned (virgile)2018-02-12variable declared in "for" init-part unrecognized in loop body assigns clause; 100% verification degree reported nevertheless
 0002362 1 [Frama-C]
Plug-in > clang
minorassigned (virgile)2018-02-12"let" in predicate body unrecognized
 0002361 1 [Frama-C]
Plug-in > clang
crashassigned (virgile)2018-02-12"assigns" in statement contract causes abort or crash
 0002360 1 [Frama-C]
Plug-in > clang
crashassigned (virgile)2018-02-12"Here" as predicate label in statement contract causes Segmentation fault
 0002359 1 [Frama-C]
Plug-in > clang
featureassigned (virgile)2018-02-12Frama-clang complains when reserved keywords are used as property labels, while Frama-C doesn't
 000235621 [Frama-C]
Plug-in > clang
featureconfirmed (virgile)2018-02-09insufficient contracts for generated constructors and assignment operator(s)
 000235721 [Frama-C]
Plug-in > clang
minorassigned (virgile)2018-02-08can't handle lemma with 3 labels
 0002358 1 [Frama-C]
Plug-in > clang
featureassigned (virgile)2018-02-08predicate argument type "struct S" accepted by Frama-C, but not by Frama-clang
 000235022 [Frama-C]
Plug-in > clang
minoracknowledged (virgile)2018-02-08kernel warns about invalid implicit conversion
 000235511 [Frama-C]
Plug-in > clang
minorassigned (virgile)2018-02-05Alt-Ergo reports about " bool and int cannot be unified"
 000148411 [Frama-C]
Plug-in > wp
minorassigned (correnson)2018-02-05ill-typed alt-ergo proof obligation
 000234043 [Frama-C]
Plug-in > wp
minoracknowledged (correnson)2018-02-02Coq translation of predicate name changes when additional files are processed by Frama-C
 000235315 [Frama-C]
Plug-in > wp
minorassigned (correnson)2018-02-01alt-ergo goals generated directly / via why3 differ in provability
 0002352 1 [Frama-C]
Plug-in > clang
crashassigned (virgile)2018-01-31Frama-Clang crashes on error in contract
 000235111 [Frama-C]
Plug-in > clang
minorassigned (virgile)2018-01-31no diagnostics on wrong keyword
 000234912 [Frama-C]
Plug-in > clang
featureconfirmed (virgile)2018-01-31warning from kernel about exceptions
 000234812 [Frama-C]
Plug-in > clang
minorassigned (virgile)2018-01-30unknown variable in contract is not treated as an error
 000234713 [Frama-C]
Plug-in > clang
crashassigned (virgile)2018-01-23direct initialisation of bool by nullptr
 0002346 2 [Frama-C]
Plug-in > clang
minorassigned (virgile)2018-01-19C++11 delegating constructor not supported
 0002345 1 [Frama-C]
Plug-in > clang
minorassigned (virgile)2018-01-19range based for loop from C++11 not supported
 000234221 [Frama-C]
Plug-in > clang
minorconfirmed (virgile)2018-01-18std::bad_alloc not supported
 00014312   [Frama-C]
Graphical User Interface
featureconfirmed (maroneze)2018-01-12How to use the "Callers ..." context menu item
 00023371   [Frama-C]
Documentation
textassigned (correnson)2017-12-29explain wp's syntactic restrictions on "inductive" definitions
 000233843 [Frama-C]
Plug-in > wp
minorassigned (correnson)2017-12-18\false provable from recursive logic definition
 00009454   [Frama-C]
Plug-in > Eva
minorassigned (maroneze)2017-12-17Should warn for overlapping lv=lv; assignments
 000225411 [Frama-C]
Plug-in > Eva
minorassigned (maroneze)2017-12-17Option "-lib-entry" results misses possible values of function pointers
 000225641 [Frama-C]
Plug-in > Eva
minorassigned (maroneze)2017-12-17"pointer comparison" warning emitted for "p==NULL"
 00021801   [Frama-C]
Plug-in > wp
crashassigned (correnson)2017-12-17Crash on loop with global assigns and per-behavior assigns
 00021668   [Frama-C]
Plug-in > Eva
minorassigned (buhler)2017-12-17Substraction results in unknown values
 000230621 [Frama-C]
Kernel
minorassigned (maroneze)2017-12-17Support for flexible array members
 000233611 [Frama-C]
Plug-in > wp
tweakassigned (correnson)2017-12-08suggest to supply previous "ensures" as hypotheses in proof obligation of next "ensures"
 00022763   [Frama-C]
Graphical User Interface
tweakacknowledged (maroneze)2017-11-27Duplicates are created on the tab "Messages"
 000233232 [Frama-C]
Plug-in > wp
majoracknowledged (correnson)2017-11-22Information on C type of array is not present (in Coq)
 0002330 1 [Frama-C]
Plug-in > wp
minorassigned (correnson)2017-10-26known, but inferrable, yet not inferred, property not given as precodition to provers
 000232912 [Frama-C]
Plug-in > wp
tweakassigned (correnson)2017-10-12suggest unique term normalization for lemmas and goals
 000228512 [Frama-C]
Plug-in > wp
featureassigned (correnson)2017-10-09suggest boolean expressions for "-wp-prop" arguments
 000210051 [Frama-C]
Plug-in > wp
minoracknowledged (correnson)2017-10-09readability of coq(?) names
 000230121 [Frama-C]
Plug-in > wp
crashassigned (correnson)2017-07-21statement contract apparently confuses parser
 0002317    [Frama-C]
Documentation > manuals
textassigned (correnson)2017-07-19Statement contracts and WP
 0002316 1 [Frama-C]
Plug-in > pathcrawler
minorassigned (nicky)2017-07-07Instrumentation Failure Error in Online Pathcrawler
 000220021 [Frama-C]
Documentation > ACSL
textacknowledged (patrick)2017-06-28explicitly mention operator precedences when referring to Fig.2.1 "Grammar of terms" in the acsl-implementation manual
 00023131   [Frama-C]
Documentation > manuals
textassigned (correnson)2017-06-23suggestions for improvement of Sect.3.6 and 3.7 of the wp manual
 000231211 [Frama-C]
Plug-in > wp
tweakassigned (correnson)2017-06-15false postcondition shouldn't be verified in default memory-model setting
 0002311 1 [Frama-C]
Plug-in > wp
textassigned (correnson)2017-06-15poor errors message texts for Hoare memory model checks
 0002309 1 [Frama-C]
Plug-in > wp
minorassigned (correnson)2017-06-01naming the default behavior influences proven obligations
 0002308 1 [Frama-C]
Plug-in > wp
featureassigned (correnson)2017-06-01suggest to check (loop) assigns clauses by data flow analysis
 000230752 [Frama-C]
Kernel
minorassigned (virgile)2017-05-31preprocessor fail: unterminated comment
 000229822 [Frama-C]
Plug-in > wp
crashassigned (correnson)2017-05-11"loop assigns" clause ignored in presence of "for"-prefixed clauses
 0002299 1 [Frama-C]
Plug-in > wp
blockassigned (correnson)2017-05-10Some ACSL mathematical functions crash WP
 0002296 1 [Frama-C]
Plug-in > wp
featureassigned (correnson)2017-05-08axiom about bounds of lsl result needed in the long run
 0002293 3 [Frama-C]
Plug-in > wp
minorassigned (correnson)2017-03-16Frama-C gives succeeding lemma, rather than preceding lemmas, as hypothesis to e.g. Cvc4
 000229217 [Frama-C]
Plug-in > wp
minorassigned (correnson)2017-03-16signature axiom omitted in Coq and Alt-ergo translation
 00017611   [Frama-C]
Kernel > ACSL implementation
majorassigned (virgile)2017-03-14Check that all occurrences of *p in assigns are guarded by a \valid(p) in requires
 000062811 [Frama-C]
Plug-in > jessie
minorassigned (cmarche)2017-03-14Frama-C/Jessie does not recognize the length of array in struct
 000229113 [Frama-C]
Plug-in > wp
minorassigned (correnson)2017-03-13suggestion: translate axioms and implication premises in forward order to coq
 0002289    [Frama-C]
Plug-in > wp
featureassigned (correnson)2017-03-01Why3ide cannot be opened in this version
 000228614 [Frama-C]
Plug-in > wp
minorassigned (correnson)2017-02-27lemma tacitly omitted from prover assumptions
 0002282 2 [Frama-C]
Plug-in > wp
minorassigned (correnson)2017-02-16applicability of Coq proof script depends on order of include files
 0002280 1 [Frama-C]
Plug-in > wp
tweakassigned (correnson)2017-02-14Frama-C sleeps too much when discharging trivial goals
 000227812 [Frama-C]
Plug-in > wp
minoracknowledged (correnson)2017-02-06problem with Qed's simplification power
 000227556 [Frama-C]
Plug-in > wp
minorconfirmed (correnson)2017-02-03translation to why3 of int* argument to logic function
 00022741   [Frama-C]
Kernel
tweakconfirmed (maroneze)2017-01-24It is impossble to change log file without kinds of message changing.
 000227221 [Frama-C]
Kernel
minorassigned (virgile)2017-01-16WP appears to assume left-to-right evaluation order for int addition
 000226411 [Frama-C]
Kernel > ACSL implementation
majorassigned (virgile)2017-01-04structure in logic not supported?
 0002266    [Frama-C]
Plug-in > wp
minorassigned (correnson)2017-01-02WP inserts unwanted new lines into Coq proofs
 0002265 1 [Frama-C]
Kernel > ACSL implementation
minorassigned (virgile)2017-01-02label Pre in function contracts
 00022631   [Frama-C]
Plug-in > wp
minorassigned (correnson)2016-12-16Why3 warning
 000226231 [Frama-C]
Plug-in > wp
minorassigned (correnson)2016-12-16more prover processes run than expected
 00022618   [Frama-C]
Plug-in > wp
minorassigned (virgile)2016-12-16wp: the example from Getting Started guide doesn't work (all goals are Unknown)
 000224821 [Frama-C]
Kernel
textassigned (virgile)2016-12-08option "-print" prints array upper bound in type before parameter name, rather than after it
 0002260    [Frama-C]
Plug-in > wp
minorassigned (correnson)2016-12-03error in Coq file generation
 0002245 1 [Frama-C]
Plug-in > wp
majorassigned (correnson)2016-08-17Nested scopes may cause issues with the validity of created pointers
 0002244 1 [Frama-C]
Plug-in > wp
majorassigned (correnson)2016-08-08Logic with read clauses can have their values invalidated by writes to separated memory locations
 0002236    [Frama-C]
Documentation > manuals
textassigned (patrick)2016-08-03tset issues in manual "acsl-implementation-Aluminium-20160501.pdf"
 0002241 1 [Frama-C]
Plug-in > wp
majorassigned (correnson)2016-07-29Implicit casting from integer to real causes failure in WP proof generation
 00021876   [Frama-C]
Documentation > ACSL
textassigned (patrick)2016-07-22Grammar omissions in 1.9
 0002234    [Frama-C]
Plug-in > wp
majorassigned (correnson)2016-06-21Creating a pointer to a local causes valid pointers above it to lose thier valid status
 00012786   [Frama-C]
Kernel > Makefile
tweakassigned (bobot)2016-06-21Path for 'make install-doc-code' for external plug-in
 00021621   [Frama-C]
Kernel > Makefile
minorassigned (bobot)2016-06-21Compilation of kernel native cmx is messed up with plugin makefile
 00021632   [Frama-C]
Kernel
featureassigned (bobot)2016-06-21Namespace through packs - packing frama-c cmx into a cmxa
 00021981   [Frama-C]
Documentation
minorassigned (correnson)2016-06-21typo in output of 'frama-c -wp-help'
 0002232 1 [Frama-C]
Plug-in > wp
crashassigned (correnson)2016-06-14Use of very large real constants cause failures in proof generation in WP
 0002229 1 [Frama-C]
Plug-in > wp
minorassigned (correnson)2016-05-31Validation fails when predicate is used with implicit type conversion.
 0002228    [Frama-C]
Plug-in > wp
minorassigned (correnson)2016-05-16Oddities in the modeling of floats and doubles
 000222372 [Frama-C]
Kernel > Makefile
textassigned (virgile)2016-05-10Frama-C upgrade installation not foolproof
 000222641 [Frama-C]
Kernel
minorassigned (correnson)2016-05-04insertion of "assert true" after a statement influences provability of the statement's contract
 0002222 1 [Frama-C]
Plug-in > wp
minorassigned (correnson)2016-04-09Make find(1) command POSIX-compliant
 000221911 [Frama-C]
Plug-in > wp
crashassigned (correnson)2016-03-22Crash with large array initialisation
 000191131 [Frama-C]
Plug-in > wp
minoracknowledged (correnson)2016-03-07WP detect a non-natural loop on a do-while(0) loop
 000220544 [Frama-C]
Plug-in > wp
minorconfirmed (correnson)2016-02-04zombie processes (again)
 0002207 1 [Frama-C]
Plug-in > wp
crashassigned (correnson)2016-02-03WP crashes with \pointer_comparable
 0002197 1 [Frama-C]
Kernel > ACSL implementation
featureassigned (virgile)2015-12-07expression "term!=term" is considered always a predicate, rather than (in some contexts) a term
 00021951   [Frama-C]
Kernel > ACSL implementation
majorassigned (virgile)2015-12-06ambiguity with consecutive comparison and ternary expressions
 0002196    [Frama-C]
Kernel > ACSL implementation
featureassigned (virgile)2015-12-05No syntax to apply lambda expressions
 000218911 [Frama-C]
Plug-in > wp
tweakassigned (correnson)2015-12-03Frama-C runs out of memory on small C program (combinatorial explosion in analysis of "main"?)
 0002188 3 [Frama-C]
Plug-in > wp
minorassigned (correnson)2015-11-30bit_test axiomatization doesn't imply == equality from bit-by-bit equality for e.g. uint32
 0001718    [Frama-C]
Kernel
featureassigned (virgile)2015-11-04Nested VLA are not supported
 0002182 1 [Frama-C]
Plug-in > wp
crashassigned (correnson)2015-10-27Plug-in wp aborted: internal error, Raised at file "src/wp/register.ml", line 579
 000217911 [Frama-C]
Plug-in > wp
minorassigned (correnson)2015-10-18Unable to prove things that are provable, gets confused
 0002170    [Frama-C]
Kernel > ACSL implementation
minorassigned (virgile)2015-09-24ACSL typing fails when performing unification of type variables
 0002169 1 [Frama-C]
Plug-in > wp
minorassigned (correnson)2015-09-21incomplete Alt-Ergo obligation files generated in presence of lemma "forall int x; ..." with "x" not occurring in "..."
 0002168 1 [Frama-C]
Plug-in > wp
featureassigned (correnson)2015-09-21suggest command-line option to avoid sophisticated expression transformations, in particular for Coq obligations
 00021601   [Frama-C]
Plug-in > wp
minoracknowledged (correnson)2015-09-15assertion failure using memset on a char
 000215611 [Frama-C]
Plug-in > wp
minorassigned (correnson)2015-09-07Slow in proof obligation generation
 000215343 [Frama-C]
Plug-in > wp
minoracknowledged (correnson)2015-09-03bound variable names in Coq file depend on unrelated function later in C source code
 0002152    [Frama-C]
Kernel
minorassigned (virgile)2015-08-21With struct containing arrays, option -unspecified-access is too strict
 000199211 [Frama-C]
Plug-in > pdg
minorassigned (maroneze)2015-08-03Control dependencies between labelled instructuctions and the corresponding goto statement
 0002148    [Frama-C]
Kernel > ACSL implementation
majorassigned (virgile)2015-07-17implicit conversion of terms to predicates
 000214533 [Frama-C]
Plug-in > wp
minorassigned (correnson)2015-07-17Error when struct has no members
 0002147    [Frama-C]
Kernel > ACSL implementation
minorassigned (virgile)2015-07-16Frama-C problem with macro substitution in annotations
 00020411   [Frama-C]
Plug-in > wp
minoracknowledged (correnson)2015-06-29unable to use lemma separated_region
 000212323 [Frama-C]
Plug-in > wp
minoracknowledged (correnson)2015-06-29validity of obligation from statement contract depends on whether the statement is enclosed in block {}
 0002134    [Frama-C]
Kernel > ACSL implementation
minorassigned (virgile)2015-06-12Weak and Strong Invariants are not supported
 00021251   [Frama-C]
Kernel > ACSL implementation
minorconfirmed (virgile)2015-06-02Redefintion of variables in same scope is allowed in annotations
 000208712 [Frama-C]
Plug-in > wp
minoracknowledged (correnson)2015-03-09Able to assert a false statement
 0002054    [Frama-C]
ptests
minorassigned (virgile)2015-01-22ptest doesn't abort tests for which the command is incorrect
 0002039 1 [Frama-C]
Plug-in > wp
crashassigned (correnson)2014-12-22WP-Plugin crashes due to an internal error when terms of sets during union have different types
 0002011    [Frama-C]
Plug-in > wp
majorassigned (correnson)2014-12-02Unsoundness bug using native alt-ergo and Why3 due to reordering of lemmas
 0001632    [Frama-C]
Kernel > ACSL implementation
minorassigned (virgile)2014-10-29Translation of abrupt clause into assert do not take 'for :' clause into account
 0001943 1 [Frama-C]
Plug-in > jessie
majorassigned (cmarche)2014-10-29Jessie crashes with "Assertion failed"
 0001936 1 [Frama-C]
Plug-in > wp
crashassigned (correnson)2014-10-14WP crashes on \floor builtin
 000191312 [Frama-C]
Plug-in > jessie
crashassigned (cmarche)2014-08-26Jessie crashes on incorrectly declared malloc
 0001847    [Frama-C]
Plug-in > wp
minorassigned (correnson)2014-07-21Problem with _Bool(when casting to int or with ?:)
 0001844 1 [Frama-C]
Plug-in > wp
crashassigned (correnson)2014-07-17assigns crash on incorrect locations
 000163842 [Frama-C]
Plug-in > wp
majoracknowledged (correnson)2014-07-17assigns clause appears unprovable
 00011032   [Frama-C]
Kernel
featureassigned (virgile)2014-07-11Default @requires property for the [main] function
 00014613   [Frama-C]
Plug-in > wp
minoracknowledged (correnson)2014-06-17assigns, loop assigns and loop invariant
 000181212 [Frama-C]
Plug-in > wp
minoracknowledged (correnson)2014-06-17Assigns not respected in behaviors when using pointers to pointers
 0001806    [Frama-C]
Plug-in > wp
minorassigned (correnson)2014-06-13Error in coq code generated by wp
 0001804    [Frama-C]
Plug-in > wp
crashassigned (correnson)2014-06-06WP crash when type casting in lemma
 0001801    [Frama-C]
Plug-in > wp
majorassigned (correnson)2014-06-06WP doesn't warn about volatile variables
 0001800    [Frama-C]
Kernel
minorassigned (virgile)2014-06-06Cannot use quotes in comments in annotations
 00015377   [Frama-C]
Plug-in > wp
featureacknowledged (correnson)2014-06-02Frama-C should warn about inconsistent specification of declared functions
 0001645    [Frama-C]
Kernel
minorassigned (virgile)2014-03-24Initializer of static variable refers to size of type of local variable
 0001712    [Frama-C]
Kernel
minorassigned (virgile)2014-03-24Statically reject programs that jump over VLA declaration.
 00014542   [Frama-C]
Kernel > configure
minorassigned (virgile)2014-03-14Configure script's autolocation of local OcamlGraph breaks out of tree builds
 0001699    [Frama-C]
Plug-in > wp
featureassigned (correnson)2014-03-14Develop strategies to efficiently run WP with different ATP and Coq
 0001693    [Frama-C]
Plug-in > wp
featureassigned (correnson)2014-03-14Generate footprint from reads clauses of logic declarations
 0001694    [Frama-C]
Plug-in > wp
featureassigned (correnson)2014-03-13Generate proof obligation for drivers when driver instantiate a logic acsl declaration
 0001687    [Frama-C]
Plug-in > wp
majorassigned (correnson)2014-03-12Frama-C GUI discards candidate coq proof
 00007504   [Frama-C]
Kernel > ACSL implementation
featureacknowledged (virgile)2014-02-12Several [invariant] at a program point
 00012812   [Frama-C]
Plug-in > wp
minoracknowledged (correnson)2014-02-05do { ... } while (0) pattern causes wp to fail
 00014951   [Frama-C]
Kernel > ACSL implementation
minorassigned (virgile)2014-02-05crash
 000155641 [Frama-C]
Plug-in > wp
minoracknowledged (correnson)2014-02-05unprovable PO in function manipulating structs - issue with Qed's simplifications
 00016212   [Frama-C]
Plug-in > wp
minoracknowledged (correnson)2014-01-24loop invariant as hypothesis
 0001577 1 [Frama-C]
Kernel
featureassigned (virgile)2013-12-17suggest to insert implicit cast of logic function's expression to return type
 0001582    [Frama-C]
Kernel > ACSL implementation
tweakassigned (virgile)2013-12-03r24600: confusing error message when t[] is used where t* is expected
 0001576 1 [Frama-C]
Kernel
featureassigned (virgile)2013-11-28declaration of variable of type void accepted
 00014501   [Frama-C]
Kernel
minorconfirmed (signoles)2013-09-26journalization of -print option
 000147161 [Frama-C]
Kernel
minoracknowledged (signoles)2013-09-26r23410: unsound reporting of pre-condition status
 00014303   [Frama-C]
Plug-in > report
minorassigned (correnson)2013-05-31RTE are not in 'report'
 00014281   [Frama-C]
Plug-in > wp
minorassigned (correnson)2013-05-24Range verification in 2D-array fails
 0001418    [Frama-C]
Kernel > configure
majorassigned (virgile)2013-05-09Fatal error: exception Env.Error("C:\Frama-C\lib/pervasives.cmi")
 0001417    [Frama-C]
Plug-in > jessie
minorassigned (cmarche)2013-05-08Config file 'C:\cygwin\home\xiewenlong\.gwhyrc' does not exists,
 0001389    [Frama-C]
Plug-in > wp
featureassigned (correnson)2013-04-16Translation of tsets
 000076551 [Frama-C]
Plug-in > wp
minorassigned (correnson)2013-03-09Post-state of statement spec
 000085241 [Frama-C]
Kernel
minorassigned (virgile)2013-01-25non-constant size of 2-dim array causes error in recursive procedure
 0001332    [Frama-C]
Plug-in > wp
crashassigned (correnson)2012-12-15[wp] failure: not an integer (Blob)
 0001327    [Frama-C]
Kernel
minorassigned (virgile)2012-12-12Code annotation in the middle of labels
 0001291    [Frama-C]
Kernel > ACSL implementation
minoracknowledged (virgile)2012-10-31Typing rejects polymorphic logic constants
 0001288 2 [Frama-C]
Plug-in > aoraï
trivialacknowledged (virgile)2012-10-26.ya filename missing in error report
 0001280    [Frama-C]
Plug-in > wp
minorassigned (correnson)2012-10-13Printing of function types causes a stack overflow
 0001279 1 [Frama-C]
Plug-in > wp
crashassigned (correnson)2012-10-13Multiple branches to a label/loop entries crashes wp
 000037921 [Frama-C]
Plug-in > jessie
crashassigned (cmarche)2012-09-21\separated
 000118641 [Frama-C]
Plug-in > wp
minorassigned (correnson)2012-06-15ltl does not accept state charts with transitions invoking dynamic function pointers
 000065811 [Frama-C]
Plug-in > jessie
featureassigned (cmarche)2012-06-10loop assigns crash
 000065311 [Frama-C]
Plug-in > jessie
minorassigned (cmarche)2012-06-10jessie's Unexpected failure
 0001010    [Frama-C]
Plug-in > wp
featureassigned (correnson)2012-06-09warn on stderr about current restrictions, and list them in WP manual
 00011901   [Frama-C]
Kernel
minorassigned (virgile)2012-06-09__builtin_alloca
 000116111 [Frama-C]
Plug-in > jessie
featureassigned (cmarche)2012-04-17error in wp_behav.c
 000115441 [Frama-C]
Plug-in > jessie
minorassigned (cmarche)2012-04-17erroneous left value (structure field)
 0001093 1 [Frama-C]
Plug-in > jessie
crashassigned (cmarche)2012-02-14Passing multi-dimensional arrays via reference fails
 00009672   [Frama-C]
Kernel > ACSL implementation
minorassigned (virgile)2012-02-09unbound function \length in annotation
 0000252    [Frama-C]
Plug-in > jessie
featureassigned (virgile)2012-01-21type invariants
 0001062    [Frama-C]
Plug-in > jessie
majorassigned (cmarche)2012-01-12Jessie incorrectly handles initialization of static array with {} initialization
 0001058    [Frama-C]
Plug-in > jessie
minorassigned (cmarche)2012-01-04Jessie incorrectly handles labels
 000105112 [Frama-C]
Plug-in > wp
textassigned (correnson)2011-12-16suspicious axiomatization of included,zrange,zunion in .sx file
 0001047 1 [Frama-C]
Plug-in > jessie
majorassigned (cmarche)2011-12-12labels defined before loops and used after loops are not correctly translated in jessie
 0001033    [Frama-C]
Plug-in > jessie
featureassigned (cmarche)2011-11-29Feature request (Jessie): \fresh (and \separated)
 0001032 2 [Frama-C]
Plug-in > jessie
featureassigned (cmarche)2011-11-29assigns nothing is not possible to proof, if malloc is not in a same function
 000100822 [Frama-C]
Plug-in > jessie
featureassigned (cmarche)2011-11-16suggest to supply lower-bound for constant_too_large_2147483647 to Simplify
 000100741 [Frama-C]
Kernel > ACSL implementation
majorassigned (virgile)2011-11-10wrong proof obligation generated for loop initialization [under why-2.30]
 0001011    [Frama-C]
Plug-in > wp
featureassigned (correnson)2011-11-04suggest to provide FILE,LINE references for proof obligations in WP cmd-line output
 0000980    [Frama-C]
Kernel > ACSL implementation
featureassigned (virgile)2011-10-06Functional expression in assigns properties
 0000923 1 [Frama-C]
Plug-in > jessie
majorassigned (cmarche)2011-08-12Jessie Plugin returns an error. Code with struct-statement, cannot be compiled.
 000092211 [Frama-C]
Plug-in > jessie
majorassigned (cmarche)2011-08-12Jessie Plugin returns an error. Code with struct-statement, cannot be compiled in a function by call by value.
 0000846 1 [Frama-C]
Plug-in > jessie
minorassigned (cmarche)2011-05-30array access in "decreases"-clause causes "Unexpected internal region in logic"
 0000834    [Frama-C]
Plug-in > jessie
minorassigned (cmarche)2011-05-24Computation of regions for axioms in axiomatics
 000082931 [Frama-C]
Plug-in > jessie
minorassigned (cmarche)2011-05-24alias between int* and uint* handled incorrectly
 0000813 1 [Frama-C]
Plug-in > jessie
minorassigned (cmarche)2011-05-09struct dereferencing causes uncaught exception
 000081121 [Frama-C]
Plug-in > jessie
minorassigned (cmarche)2011-05-06double struct dereferencing causes unbound variable error
 0000734    [Frama-C]
Kernel
tweakassigned (correnson)2011-02-21Command.command_generic may raise Sys_error
 0000713    [Frama-C]
Kernel > ACSL implementation
featureassigned (virgile)2011-02-10Any number of ";" should be allowed in specifications
 0000712    [Frama-C]
Plug-in > jessie
majorassigned (cmarche)2011-02-10Validity of valid pointer to struct member cannot be verified
 000066732 [Frama-C]
Plug-in > jessie
crashassigned (cmarche)2011-01-25/usr/share/frama-c/libc/stdio.h:107:[jessie] failure: Unexpected exception.
 0000676    [Frama-C]
Kernel
minorassigned (virgile)2011-01-18Strange AST produced with unspecified side-effects involve function calls in expressions
 0000670 1 [Frama-C]
Plug-in > jessie
minorassigned (cmarche)2011-01-12In certain circumstances Jessie cannot analyse files that it generates
 0000654    [Frama-C]
Plug-in > jessie
minorassigned (cmarche)2010-12-25Incorrect translation (Unbound variable)
 0000652 1 [Frama-C]
Plug-in > jessie
minorassigned (cmarche)2010-12-24pointer arithmetic
 0000651 1 [Frama-C]
Plug-in > jessie
minorassigned (cmarche)2010-12-24array id "shift"
 000064321 [Frama-C]
Kernel > ACSL implementation
minorassigned (virgile)2010-12-18Incorrect parsing of complex lemma
 0000601 1 [Frama-C]
Kernel > ACSL implementation
featureassigned (virgile)2010-12-16no multiple assert-clauses accepted in /*@...*/-style comment
 00006051   [Frama-C]
Kernel > ACSL implementation
minorassigned (virgile)2010-12-16Empty specification causes syntax error
 0000632 1 [Frama-C]
Plug-in > jessie
featureassigned (cmarche)2010-11-29Suggest to rename user identifiers to avoid name clashes in ..._why.sx files
 00006172   [Frama-C]
Plug-in > jessie
minorconfirmed (cmarche)2010-11-17assigns nothing ?
 00006291   [Frama-C]
Plug-in > jessie
minorassigned (cmarche)2010-11-17Incorrect processing of "type var[]" constructions
 000061511 [Frama-C]
Plug-in > jessie
majorassigned (cmarche)2010-10-22separately verified files show code-bug when linked together
 0000614 1 [Frama-C]
Plug-in > jessie
minorassigned (cmarche)2010-10-22"\valid(&aaa)" unprovable for global variable aaa - missing antecedens in proof obligation?
 000059341 [Frama-C]
Kernel
minorconfirmed (virgile)2010-10-01Parse error when using a wide string literal to initialize uint16 array
 0000590 1 [Frama-C]
Plug-in > jessie
minorassigned (cmarche)2010-09-22Jessie plugin does not support logic label Post in ensures clause
 0000544    [Frama-C]
Plug-in > jessie
featureassigned (cmarche)2010-07-17Enhancement on assigns annotation and the name of proof obligation
 00001021   [Frama-C]
Plug-in > jessie
majorconfirmed (cmarche)2010-07-13Jessie: struct field's validity
 0000518 1 [Frama-C]
Plug-in > jessie
minorassigned (cmarche)2010-06-22Loop assigns are not taken into account when proving a safety PO
 00005022   [Frama-C]
Plug-in > jessie
minorassigned (cmarche)2010-06-13Unbound label in Jessie-generated Why file when using logic function in assigns clause
 000028921 [Frama-C]
Plug-in > jessie
majoracknowledged (virgile)2010-06-09unsoundness of Jessie with respect to expression evaluation of ANSI-C
 0000485    [Frama-C]
Plug-in > jessie
featureassigned (cmarche)2010-05-18Code containing consts should be verifiable
 0000480    [Frama-C]
Plug-in > jessie
crashassigned (cmarche)2010-05-12volatile annotation breaks type checker
 0000456 1 [Frama-C]
Plug-in > jessie
minorassigned (cmarche)2010-04-23Lack of parameter generation
 0000433 1 [Frama-C]
Plug-in > jessie
tweakassigned (virgile)2010-03-23different translation of casted constants in program-code and in assertion
 000042431 [Frama-C]
Plug-in > jessie
minorassigned (cmarche)2010-03-22Uncaught exception: Failure("Unexpected internal region in logic")
 0000416 1 [Frama-C]
Plug-in > jessie
minorassigned (cmarche)2010-02-22local array decl with non-constant size causes Why error
 00000721   [Frama-C]
Plug-in > jessie
minorassigned (cmarche)2010-02-12The specifications of statements are not translated
 00000792   [Frama-C]
Kernel > ACSL implementation
featureassigned (virgile)2010-02-05Better support of //@ style
 0000387    [Frama-C]
Kernel > ACSL implementation
featureassigned (virgile)2010-02-05ghost integer ?
 00003361   [Frama-C]
Plug-in > jessie
majorassigned (cmarche)2010-01-22cast between homogenous struct and array
 0000373    [Frama-C]
Plug-in > jessie
majorassigned (cmarche)2010-01-14Global invariants are not verified
 00003481   [Frama-C]
Plug-in > jessie
majorassigned (cmarche)2009-12-03Arithmetic safety of bitwise operators cannot be verified
 00000391   [Frama-C]
Plug-in > jessie
minorconfirmed (cmarche)2009-11-24Frama-C/Jessie: memory set problem
 0000335 1 [Frama-C]
Plug-in > jessie
minorassigned (cmarche)2009-11-20Unbound reference raised by Why
 0000328 1 [Frama-C]
Plug-in > jessie
majorassigned (cmarche)2009-11-13assertion failed in Jessie with bitfields inside union
 0000291 1 [Frama-C]
Plug-in > jessie
minorassigned (cmarche)2009-10-20Unbound variable raised by why in presence of an unsafe cast
 0000040    [Frama-C]
Plug-in > jessie
minorconfirmed (cmarche)2009-10-15Frama-C/Jessie: typing error
 000026121 [Frama-C]
Kernel
minoracknowledged (virgile)2009-10-01Frama-C fails to parse a file
 0000256    [Frama-C]
Plug-in > jessie
minorassigned (cmarche)2009-09-25array range in requires predicate
 0000025    [Frama-C]
Plug-in > jessie
minoracknowledged (virgile)2009-09-21type invariants
 0000215 1 [Frama-C]
Plug-in > jessie
minorassigned (cmarche)2009-08-25Mise en hypothèse de la précondition d'une opération appelée
 00001851   [Frama-C]
Plug-in > jessie
majorassigned (cmarche)2009-07-17Frama-C cannot process properly arrays of structures
 00001781   [Frama-C]
Plug-in > jessie
minorconfirmed (cmarche)2009-07-09type error in generated why file
 00000921   [Frama-C]
Plug-in > jessie
minorassigned (cmarche)2009-06-19Why error with logic functions returning a pointer
 00000422   [Frama-C]
Plug-in > jessie
featureassigned (cmarche)2009-06-17Default invariant should be inferred for loops
 0000031    [Frama-C]
Plug-in > jessie
minoracknowledged (cmarche)2009-06-17Why- error :-jessie-no-regions and assigns does not work
 0000032    [Frama-C]
Plug-in > jessie
minorassigned (cmarche)2009-04-10Internal error with assign specification on bi-dimensional arrays
 0000038    [Frama-C]
Plug-in > jessie
minorassigned (cmarche)2009-04-10Jessie crashes on simple program without annotations