2021-01-27 10:26 CET

Frama-C Bug Tracking System - All Projects

Word 2000 Word View

Viewing Issues ( 1 - 269 )

  PID # Attachment count CategorySeverityStatusUpdatedSummary
 0002508 1 Kernelminorassigned (AllanBlanchard)2020-10-06cabs2cil fails with statements in expression in a question
 000242011 Plug-in > wpcrashresolved (correnson)2020-09-09Wp crashes on a recursive function
 0002505    Documentation > manualsminoracknowledged (maroneze)2020-05-07WP manual: hyperlink in table of contents sometimes one off
 0002504 1 Kernelminoracknowledged (virgile)2020-05-07more precise error message for missing closing } of axiomatic block
 0002498 2 Plug-in > wpminorassigned (correnson)2020-02-24munmap() breaks WP analysis
 000249721 Plug-in > wpminorassigned (correnson)2020-02-03quantifiers over logic types do not restrict to valid instances
 0002491 1 Plug-in > clangminorassigned (fvedrine)2020-01-23incompatibilité de libc/math.h ??
 000248621 Graphical User Interfacemajorassigned (correnson)2019-11-18Left pan (file tree and plugin views) inaccessible upon resize in frama-c-gui
 0002485 1 Plug-in > wpminorassigned (correnson)2019-11-08-wp-out missing output for Why3 provers in Frama-C 20 beta
 0002484    Plug-in > wpminorassigned (correnson)2019-11-08alt-ergo support in Frama-C 20 beta
 0002483 1 Plug-in > wpminorassigned (correnson)2019-11-08Eprover in Frama-C 20 beta
 000240431 Plug-in > wpminoracknowledged (correnson)2019-10-17Shape of VC depends on selection of properties
 000242751 Plug-in > wpminoracknowledged (correnson)2019-10-17Prove of \false
 00024802   Plug-in > clangblockconfirmed (virgile)2019-10-06Syntax error in reorder_defs.ml after running make
 00024743   Documentation > websiteminorassigned (bobot)2019-09-18Can't view publications on the wiki
 00024631   Plug-in > clangmajorassigned (virgile)2019-07-08Error in frama-clang make file
 00024622   Plug-in > clangmajorassigned (virgile)2019-07-05frama-clang failed to install
 00024573   Kernel > configureminorassigned (virgile)2019-06-20configure does not detect gtksourceview due to wrong path
 00024581   Kernel > configureminorassigned (virgile)2019-06-20build failure due to mangled variable assignment in Makefile
 00024561   Kernel > Makefileminorassigned (bobot)2019-06-18Does not build with OCaml 4.08.0
 00024491   Documentation > websitetrivialconfirmed (virgile)2019-06-10invalid links to "ACSL by Example"
 00024481   Documentation > websiteminorassigned (bobot)2019-06-04frama-c installation needs dune > 1.5 package installed
 0002435 1 Kernelmajorassigned (virgile)2019-05-08kernel generates UnspecifiedSequence when 2 following ternary operators
 0002327    Plug-in > E-ACSLminorassigned (signoles)2019-01-25Failure to detect overflows into an allocated area within a struct
 0002194    Plug-in > E-ACSLminorassigned (signoles)2019-01-25Failure to record global variable with initialiser
 0002310 1 Plug-in > E-ACSLminorassigned (signoles)2019-01-25Incorrect handling of \initialized when initialized struct is passed to a function by value
 000242221 Plug-in > E-ACSLcrashconfirmed (signoles)2019-01-23Can't use e-acsl on a dynamic library containing all the instrumentations
 000241291 Plug-in > E-ACSLcrashconfirmed (signoles)2018-12-17E-ACSL crash with RTE generated assertion with booleans
 0002419    Plug-in > RTEminorconfirmed (signoles)2018-12-17Missing cast in code generated by RTE
 00024163   Plug-in > E-ACSLminoracknowledged (signoles)2018-12-11missing E-ACSL code, control flow graph, function pointer
 000241321 Plug-in > E-ACSLmajorconfirmed (signoles)2018-12-06missing E-ACSL code when ignoring asm annotation
 0001648    Kernelmajorassigned (maroneze)2018-11-30Wrong specification for standard library function memmove
 00024023   Plug-in > clangblockassigned (virgile)2018-10-03frama-clang fails to compile
 00023952   Plug-in > clangminorassigned (virgile)2018-09-07const fields in constructors
 00023971   Kernel > ACSL implementationfeatureassigned (virgile)2018-08-27Model Variables in Frama C
 0002396    Plug-in > clangminorassigned (virgile)2018-08-24cast error with reference fields
 0002376 1 Plug-in > jessiecrashassigned (cmarche)2018-05-29frama-c/jessie crashes with Unexpected error (Cil.SizeOfError("Undefined sizeof on a function.", _)).
 0002370    Kernel > ACSL implementationfeatureassigned (virgile)2018-03-08Expose ACSL annotations through host language pragmas
 00023698   Plug-in > E-ACSLminoracknowledged (signoles)2018-02-23e-acsl-gcc failes on macOS
 000236711 Plug-in > clangminorassigned (virgile)2018-02-12C-function returning a struct causes warning on missing Ctor code/spec when inside 'extern "C" {...}'
 0002366 1 Plug-in > clangminorassigned (virgile)2018-02-12loop assigns clause ginored under strange circumstances
 0002365 1 Plug-in > clangminorassigned (virgile)2018-02-12user-defined type not accepted after builtin type in quantifier chain
  0002364 1 Plug-in > clangfeatureassigned (virgile)2018-02-12Frama-clang reports overloading ambiguity where Frama-C doesn't
 0002363 1 Plug-in > clangminorassigned (virgile)2018-02-12variable declared in "for" init-part unrecognized in loop body assigns clause; 100% verification degree reported nevertheless
 0002362 1 Plug-in > clangminorassigned (virgile)2018-02-12"let" in predicate body unrecognized
 0002361 1 Plug-in > clangcrashassigned (virgile)2018-02-12"assigns" in statement contract causes abort or crash
 0002360 1 Plug-in > clangcrashassigned (virgile)2018-02-12"Here" as predicate label in statement contract causes Segmentation fault
 0002359 1 Plug-in > clangfeatureassigned (virgile)2018-02-12Frama-clang complains when reserved keywords are used as property labels, while Frama-C doesn't
 000235621 Plug-in > clangfeatureconfirmed (virgile)2018-02-09insufficient contracts for generated constructors and assignment operator(s)
 000235721 Plug-in > clangminorassigned (virgile)2018-02-08can't handle lemma with 3 labels
 0002358 1 Plug-in > clangfeatureassigned (virgile)2018-02-08predicate argument type "struct S" accepted by Frama-C, but not by Frama-clang
 000235022 Plug-in > clangminoracknowledged (virgile)2018-02-08kernel warns about invalid implicit conversion
 000235511 Plug-in > clangminorassigned (virgile)2018-02-05Alt-Ergo reports about " bool and int cannot be unified"
 0002352 1 Plug-in > clangcrashassigned (virgile)2018-01-31Frama-Clang crashes on error in contract
 000235111 Plug-in > clangminorassigned (virgile)2018-01-31no diagnostics on wrong keyword
 000234912 Plug-in > clangfeatureconfirmed (virgile)2018-01-31warning from kernel about exceptions
 000234812 Plug-in > clangminorassigned (virgile)2018-01-30unknown variable in contract is not treated as an error
 000234713 Plug-in > clangcrashassigned (virgile)2018-01-23direct initialisation of bool by nullptr
 0002346 2 Plug-in > clangminorassigned (virgile)2018-01-19C++11 delegating constructor not supported
 0002345 1 Plug-in > clangminorassigned (virgile)2018-01-19range based for loop from C++11 not supported
 000234221 Plug-in > clangminorconfirmed (virgile)2018-01-18std::bad_alloc not supported
 00014311   Graphical User Interfacefeatureconfirmed (maroneze)2018-01-12How to use the "Callers ..." context menu item
 00009453   Plug-in > Evaminorassigned (maroneze)2017-12-17Should warn for overlapping lv=lv; assignments
 000225411 Plug-in > Evaminorassigned (maroneze)2017-12-17Option "-lib-entry" results misses possible values of function pointers
 000225621 Plug-in > Evaminorassigned (maroneze)2017-12-17"pointer comparison" warning emitted for "p==NULL"
 00021668   Plug-in > Evaminorassigned (buhler)2017-12-17Substraction results in unknown values
 000230621 Kernelminorassigned (maroneze)2017-12-17Support for flexible array members
 00022763   Graphical User Interfacetweakacknowledged (maroneze)2017-11-27Duplicates are created on the tab "Messages"
 000230121 Plug-in > wpcrashassigned (correnson)2017-07-21statement contract apparently confuses parser
 0002317    Documentation > manualstextassigned (correnson)2017-07-19Statement contracts and WP
 0002316 1 Plug-in > pathcrawlerminorassigned (nicky)2017-07-07Instrumentation Failure Error in Online Pathcrawler
 00023131   Documentation > manualstextassigned (correnson)2017-06-23suggestions for improvement of Sect.3.6 and 3.7 of the wp manual
 000231211 Plug-in > wptweakassigned (correnson)2017-06-15false postcondition shouldn't be verified in default memory-model setting
 0002311 1 Plug-in > wptextassigned (correnson)2017-06-15poor errors message texts for Hoare memory model checks
 0002309 1 Plug-in > wpminorassigned (correnson)2017-06-01naming the default behavior influences proven obligations
 0002308 1 Plug-in > wpfeatureassigned (correnson)2017-06-01suggest to check (loop) assigns clauses by data flow analysis
 000230732 Kernelminorassigned (virgile)2017-05-31preprocessor fail: unterminated comment
 000229822 Plug-in > wpcrashassigned (correnson)2017-05-11"loop assigns" clause ignored in presence of "for"-prefixed clauses
 0002299 1 Plug-in > wpblockassigned (correnson)2017-05-10Some ACSL mathematical functions crash WP
 0002296 1 Plug-in > wpfeatureassigned (correnson)2017-05-08axiom about bounds of lsl result needed in the long run
 0002293 3 Plug-in > wpminorassigned (correnson)2017-03-16Frama-C gives succeeding lemma, rather than preceding lemmas, as hypothesis to e.g. Cvc4
 000229217 Plug-in > wpminorassigned (correnson)2017-03-16signature axiom omitted in Coq and Alt-ergo translation
 00017611   Kernel > ACSL implementationmajorassigned (virgile)2017-03-14Check that all occurrences of *p in assigns are guarded by a \valid(p) in requires
 000062811 Plug-in > jessieminorassigned (cmarche)2017-03-14Frama-C/Jessie does not recognize the length of array in struct
 000229113 Plug-in > wpminorassigned (correnson)2017-03-13suggestion: translate axioms and implication premises in forward order to coq
 0002289    Plug-in > wpfeatureassigned (correnson)2017-03-01Why3ide cannot be opened in this version
 000228614 Plug-in > wpminorassigned (correnson)2017-02-27lemma tacitly omitted from prover assumptions
 0002282 2 Plug-in > wpminorassigned (correnson)2017-02-16applicability of Coq proof script depends on order of include files
 0002280 1 Plug-in > wptweakassigned (correnson)2017-02-14Frama-C sleeps too much when discharging trivial goals
 000227812 Plug-in > wpminoracknowledged (correnson)2017-02-06problem with Qed's simplification power
 000227556 Plug-in > wpminorconfirmed (correnson)2017-02-03translation to why3 of int* argument to logic function
 00022741   Kerneltweakconfirmed (maroneze)2017-01-24It is impossble to change log file without kinds of message changing.
 000227221 Kernelminorassigned (virgile)2017-01-16WP appears to assume left-to-right evaluation order for int addition
 000226411 Kernel > ACSL implementationmajorassigned (virgile)2017-01-04structure in logic not supported?
 0002266    Plug-in > wpminorassigned (correnson)2017-01-02WP inserts unwanted new lines into Coq proofs
 0002265 1 Kernel > ACSL implementationminorassigned (virgile)2017-01-02label Pre in function contracts
 00022631   Plug-in > wpminorassigned (correnson)2016-12-16Why3 warning
 000226231 Plug-in > wpminorassigned (correnson)2016-12-16more prover processes run than expected
 00022618   Plug-in > wpminorassigned (virgile)2016-12-16wp: the example from Getting Started guide doesn't work (all goals are Unknown)
 000224821 Kerneltextassigned (virgile)2016-12-08option "-print" prints array upper bound in type before parameter name, rather than after it
 0002260    Plug-in > wpminorassigned (correnson)2016-12-03error in Coq file generation
 0002245 1 Plug-in > wpmajorassigned (correnson)2016-08-17Nested scopes may cause issues with the validity of created pointers
 0002244 1 Plug-in > wpmajorassigned (correnson)2016-08-08Logic with read clauses can have their values invalidated by writes to separated memory locations
 0002241 1 Plug-in > wpmajorassigned (correnson)2016-07-29Implicit casting from integer to real causes failure in WP proof generation
 0002234    Plug-in > wpmajorassigned (correnson)2016-06-21Creating a pointer to a local causes valid pointers above it to lose thier valid status
 00012781   Kernel > Makefiletweakassigned (bobot)2016-06-21Path for 'make install-doc-code' for external plug-in
 0002162    Kernel > Makefileminorassigned (bobot)2016-06-21Compilation of kernel native cmx is messed up with plugin makefile
 00021631   Kernelfeatureassigned (bobot)2016-06-21Namespace through packs - packing frama-c cmx into a cmxa
 00021981   Documentationminorassigned (correnson)2016-06-21typo in output of 'frama-c -wp-help'
 0002232 1 Plug-in > wpcrashassigned (correnson)2016-06-14Use of very large real constants cause failures in proof generation in WP
 0002229 1 Plug-in > wpminorassigned (correnson)2016-05-31Validation fails when predicate is used with implicit type conversion.
 0002228    Plug-in > wpminorassigned (correnson)2016-05-16Oddities in the modeling of floats and doubles
 000222372 Kernel > Makefiletextassigned (virgile)2016-05-10Frama-C upgrade installation not foolproof
 000222631 Kernelminorassigned (correnson)2016-05-04insertion of "assert true" after a statement influences provability of the statement's contract
 0002222 1 Plug-in > wpminorassigned (correnson)2016-04-09Make find(1) command POSIX-compliant
 0002219 1 Plug-in > wpcrashassigned (correnson)2016-03-22Crash with large array initialisation
 000191131 Plug-in > wpminoracknowledged (correnson)2016-03-07WP detect a non-natural loop on a do-while(0) loop
 000220544 Plug-in > wpminorconfirmed (correnson)2016-02-04zombie processes (again)
 0002207 1 Plug-in > wpcrashassigned (correnson)2016-02-03WP crashes with \pointer_comparable
 0002197 1 Kernel > ACSL implementationfeatureassigned (virgile)2015-12-07expression "term!=term" is considered always a predicate, rather than (in some contexts) a term
 00021951   Kernel > ACSL implementationmajorassigned (virgile)2015-12-06ambiguity with consecutive comparison and ternary expressions
 0002196    Kernel > ACSL implementationfeatureassigned (virgile)2015-12-05No syntax to apply lambda expressions
 0002189 1 Plug-in > wptweakassigned (correnson)2015-12-03Frama-C runs out of memory on small C program (combinatorial explosion in analysis of "main"?)
 0002188 3 Plug-in > wpminorassigned (correnson)2015-11-30bit_test axiomatization doesn't imply == equality from bit-by-bit equality for e.g. uint32
 0001718    Kernelfeatureassigned (virgile)2015-11-04Nested VLA are not supported
 0002182 1 Plug-in > wpcrashassigned (correnson)2015-10-27Plug-in wp aborted: internal error, Raised at file "src/wp/register.ml", line 579
 000217911 Plug-in > wpminorassigned (correnson)2015-10-18Unable to prove things that are provable, gets confused
 0002170    Kernel > ACSL implementationminorassigned (virgile)2015-09-24ACSL typing fails when performing unification of type variables
 0002169 1 Plug-in > wpminorassigned (correnson)2015-09-21incomplete Alt-Ergo obligation files generated in presence of lemma "forall int x; ..." with "x" not occurring in "..."
 0002168 1 Plug-in > wpfeatureassigned (correnson)2015-09-21suggest command-line option to avoid sophisticated expression transformations, in particular for Coq obligations
 00021601   Plug-in > wpminoracknowledged (correnson)2015-09-15assertion failure using memset on a char
 000215611 Plug-in > wpminorassigned (correnson)2015-09-07Slow in proof obligation generation
 000215343 Plug-in > wpminoracknowledged (correnson)2015-09-03bound variable names in Coq file depend on unrelated function later in C source code
 0002152    Kernelminorassigned (virgile)2015-08-21With struct containing arrays, option -unspecified-access is too strict
 0001992 1 Plug-in > pdgminorassigned (maroneze)2015-08-03Control dependencies between labelled instructuctions and the corresponding goto statement
 0002148    Kernel > ACSL implementationmajorassigned (virgile)2015-07-17implicit conversion of terms to predicates
 000214533 Plug-in > wpminorassigned (correnson)2015-07-17Error when struct has no members
 0002147    Kernel > ACSL implementationminorassigned (virgile)2015-07-16Frama-C problem with macro substitution in annotations
 00020411   Plug-in > wpminoracknowledged (correnson)2015-06-29unable to use lemma separated_region
 000212323 Plug-in > wpminoracknowledged (correnson)2015-06-29validity of obligation from statement contract depends on whether the statement is enclosed in block {}
 0002134    Kernel > ACSL implementationminorassigned (virgile)2015-06-12Weak and Strong Invariants are not supported
 00021251   Kernel > ACSL implementationminorconfirmed (virgile)2015-06-02Redefintion of variables in same scope is allowed in annotations
 000208712 Plug-in > wpminoracknowledged (correnson)2015-03-09Able to assert a false statement
 0002054    ptestsminorassigned (virgile)2015-01-22ptest doesn't abort tests for which the command is incorrect
 0002039 1 Plug-in > wpcrashassigned (correnson)2014-12-22WP-Plugin crashes due to an internal error when terms of sets during union have different types
 0002011    Plug-in > wpmajorassigned (correnson)2014-12-02Unsoundness bug using native alt-ergo and Why3 due to reordering of lemmas
 0001632    Kernel > ACSL implementationminorassigned (virgile)2014-10-29Translation of abrupt clause into assert do not take 'for :' clause into account
 0001943 1 Plug-in > jessiemajorassigned (cmarche)2014-10-29Jessie crashes with "Assertion failed"
 0001936 1 Plug-in > wpcrashassigned (correnson)2014-10-14WP crashes on \floor builtin
 000191312 Plug-in > jessiecrashassigned (cmarche)2014-08-26Jessie crashes on incorrectly declared malloc
 0001847    Plug-in > wpminorassigned (correnson)2014-07-21Problem with _Bool(when casting to int or with ?:)
 0001844 1 Plug-in > wpcrashassigned (correnson)2014-07-17assigns crash on incorrect locations
 000163842 Plug-in > wpmajoracknowledged (correnson)2014-07-17assigns clause appears unprovable
 00011032   Kernelfeatureassigned (virgile)2014-07-11Default @requires property for the [main] function
 00014613   Plug-in > wpminoracknowledged (correnson)2014-06-17assigns, loop assigns and loop invariant
 000181212 Plug-in > wpminoracknowledged (correnson)2014-06-17Assigns not respected in behaviors when using pointers to pointers
 0001804    Plug-in > wpcrashassigned (correnson)2014-06-06WP crash when type casting in lemma
 0001801    Plug-in > wpmajorassigned (correnson)2014-06-06WP doesn't warn about volatile variables
 0001800    Kernelminorassigned (virgile)2014-06-06Cannot use quotes in comments in annotations
 00015377   Plug-in > wpfeatureacknowledged (correnson)2014-06-02Frama-C should warn about inconsistent specification of declared functions
 0001645    Kernelminorassigned (virgile)2014-03-24Initializer of static variable refers to size of type of local variable
 0001712    Kernelminorassigned (virgile)2014-03-24Statically reject programs that jump over VLA declaration.
 00014541   Kernel > configureminorassigned (virgile)2014-03-14Configure script's autolocation of local OcamlGraph breaks out of tree builds
 0001699    Plug-in > wpfeatureassigned (correnson)2014-03-14Develop strategies to efficiently run WP with different ATP and Coq
 0001693    Plug-in > wpfeatureassigned (correnson)2014-03-14Generate footprint from reads clauses of logic declarations
 0001694    Plug-in > wpfeatureassigned (correnson)2014-03-13Generate proof obligation for drivers when driver instantiate a logic acsl declaration
 0001687    Plug-in > wpmajorassigned (correnson)2014-03-12Frama-C GUI discards candidate coq proof
 00007503   Kernel > ACSL implementationfeatureacknowledged (virgile)2014-02-12Several [invariant] at a program point
 00012811   Plug-in > wpminoracknowledged (correnson)2014-02-05do { ... } while (0) pattern causes wp to fail
 00014951   Kernel > ACSL implementationminorassigned (virgile)2014-02-05crash
 000155631 Plug-in > wpminoracknowledged (correnson)2014-02-05unprovable PO in function manipulating structs - issue with Qed's simplifications
 00016212   Plug-in > wpminoracknowledged (correnson)2014-01-24loop invariant as hypothesis
 0001577 1 Kernelfeatureassigned (virgile)2013-12-17suggest to insert implicit cast of logic function's expression to return type
 0001582    Kernel > ACSL implementationtweakassigned (virgile)2013-12-03r24600: confusing error message when t[] is used where t* is expected
 0001576 1 Kernelfeatureassigned (virgile)2013-11-28declaration of variable of type void accepted
 00014501   Kernelminorconfirmed (signoles)2013-09-26journalization of -print option
 00014303   Plug-in > reportminorassigned (correnson)2013-05-31RTE are not in 'report'
 00014281   Plug-in > wpminorassigned (correnson)2013-05-24Range verification in 2D-array fails
 0001418    Kernel > configuremajorassigned (virgile)2013-05-09Fatal error: exception Env.Error("C:\Frama-C\lib/pervasives.cmi")
 0001417    Plug-in > jessieminorassigned (cmarche)2013-05-08Config file 'C:\cygwin\home\xiewenlong\.gwhyrc' does not exists,
 0001389    Plug-in > wpfeatureassigned (correnson)2013-04-16Translation of tsets
 000076541 Plug-in > wpminorassigned (correnson)2013-03-09Post-state of statement spec
 000085241 Kernelminorassigned (virgile)2013-01-25non-constant size of 2-dim array causes error in recursive procedure
 0001332    Plug-in > wpcrashassigned (correnson)2012-12-15[wp] failure: not an integer (Blob)
 0001327    Kernelminorassigned (virgile)2012-12-12Code annotation in the middle of labels
 0001291    Kernel > ACSL implementationminoracknowledged (virgile)2012-10-31Typing rejects polymorphic logic constants
 0001288 2 Plug-in > aoraïtrivialacknowledged (virgile)2012-10-26.ya filename missing in error report
 0001280    Plug-in > wpminorassigned (correnson)2012-10-13Printing of function types causes a stack overflow
 0001279 1 Plug-in > wpcrashassigned (correnson)2012-10-13Multiple branches to a label/loop entries crashes wp
 000037921 Plug-in > jessiecrashassigned (cmarche)2012-09-21\separated
 000118641 Plug-in > wpminorassigned (correnson)2012-06-15ltl does not accept state charts with transitions invoking dynamic function pointers
 000065811 Plug-in > jessiefeatureassigned (cmarche)2012-06-10loop assigns crash
 000065311 Plug-in > jessieminorassigned (cmarche)2012-06-10jessie's Unexpected failure
 0001010    Plug-in > wpfeatureassigned (correnson)2012-06-09warn on stderr about current restrictions, and list them in WP manual
 00011901   Kernelminorassigned (virgile)2012-06-09__builtin_alloca
 000116111 Plug-in > jessiefeatureassigned (cmarche)2012-04-17error in wp_behav.c
 000115441 Plug-in > jessieminorassigned (cmarche)2012-04-17erroneous left value (structure field)
 0001093 1 Plug-in > jessiecrashassigned (cmarche)2012-02-14Passing multi-dimensional arrays via reference fails
 0000967    Kernel > ACSL implementationminorassigned (virgile)2012-02-09unbound function \length in annotation
 0000252    Plug-in > jessiefeatureassigned (virgile)2012-01-21type invariants
 0001062    Plug-in > jessiemajorassigned (cmarche)2012-01-12Jessie incorrectly handles initialization of static array with {} initialization
 0001058    Plug-in > jessieminorassigned (cmarche)2012-01-04Jessie incorrectly handles labels
 000105112 Plug-in > wptextassigned (correnson)2011-12-16suspicious axiomatization of included,zrange,zunion in .sx file
 0001047 1 Plug-in > jessiemajorassigned (cmarche)2011-12-12labels defined before loops and used after loops are not correctly translated in jessie
 0001033    Plug-in > jessiefeatureassigned (cmarche)2011-11-29Feature request (Jessie): \fresh (and \separated)
 0001032 2 Plug-in > jessiefeatureassigned (cmarche)2011-11-29assigns nothing is not possible to proof, if malloc is not in a same function
 000100822 Plug-in > jessiefeatureassigned (cmarche)2011-11-16suggest to supply lower-bound for constant_too_large_2147483647 to Simplify
 000100741 Kernel > ACSL implementationmajorassigned (virgile)2011-11-10wrong proof obligation generated for loop initialization [under why-2.30]
 0001011    Plug-in > wpfeatureassigned (correnson)2011-11-04suggest to provide FILE,LINE references for proof obligations in WP cmd-line output
 0000980    Kernel > ACSL implementationfeatureassigned (virgile)2011-10-06Functional expression in assigns properties
 0000923 1 Plug-in > jessiemajorassigned (cmarche)2011-08-12Jessie Plugin returns an error. Code with struct-statement, cannot be compiled.
 000092211 Plug-in > jessiemajorassigned (cmarche)2011-08-12Jessie Plugin returns an error. Code with struct-statement, cannot be compiled in a function by call by value.
 0000846 1 Plug-in > jessieminorassigned (cmarche)2011-05-30array access in "decreases"-clause causes "Unexpected internal region in logic"
 0000834    Plug-in > jessieminorassigned (cmarche)2011-05-24Computation of regions for axioms in axiomatics
 000082931 Plug-in > jessieminorassigned (cmarche)2011-05-24alias between int* and uint* handled incorrectly
 0000813 1 Plug-in > jessieminorassigned (cmarche)2011-05-09struct dereferencing causes uncaught exception
 000081121 Plug-in > jessieminorassigned (cmarche)2011-05-06double struct dereferencing causes unbound variable error
 0000734    Kerneltweakassigned (correnson)2011-02-21Command.command_generic may raise Sys_error
 0000713    Kernel > ACSL implementationfeatureassigned (virgile)2011-02-10Any number of ";" should be allowed in specifications
 0000712    Plug-in > jessiemajorassigned (cmarche)2011-02-10Validity of valid pointer to struct member cannot be verified
 000066732 Plug-in > jessiecrashassigned (cmarche)2011-01-25/usr/share/frama-c/libc/stdio.h:107:[jessie] failure: Unexpected exception.
 0000676    Kernelminorassigned (virgile)2011-01-18Strange AST produced with unspecified side-effects involve function calls in expressions
 0000670 1 Plug-in > jessieminorassigned (cmarche)2011-01-12In certain circumstances Jessie cannot analyse files that it generates
 0000654    Plug-in > jessieminorassigned (cmarche)2010-12-25Incorrect translation (Unbound variable)
 0000652 1 Plug-in > jessieminorassigned (cmarche)2010-12-24pointer arithmetic
 0000651 1 Plug-in > jessieminorassigned (cmarche)2010-12-24array id "shift"
 000064321 Kernel > ACSL implementationminorassigned (virgile)2010-12-18Incorrect parsing of complex lemma
 0000601 1 Kernel > ACSL implementationfeatureassigned (virgile)2010-12-16no multiple assert-clauses accepted in /*@...*/-style comment
 00006051   Kernel > ACSL implementationminorassigned (virgile)2010-12-16Empty specification causes syntax error
 0000632 1 Plug-in > jessiefeatureassigned (cmarche)2010-11-29Suggest to rename user identifiers to avoid name clashes in ..._why.sx files
 00006172   Plug-in > jessieminorconfirmed (cmarche)2010-11-17assigns nothing ?
 00006291   Plug-in > jessieminorassigned (cmarche)2010-11-17Incorrect processing of "type var[]" constructions
 000061511 Plug-in > jessiemajorassigned (cmarche)2010-10-22separately verified files show code-bug when linked together
 0000614 1 Plug-in > jessieminorassigned (cmarche)2010-10-22"\valid(&aaa)" unprovable for global variable aaa - missing antecedens in proof obligation?
 000059341 Kernelminorconfirmed (virgile)2010-10-01Parse error when using a wide string literal to initialize uint16 array
 0000590 1 Plug-in > jessieminorassigned (cmarche)2010-09-22Jessie plugin does not support logic label Post in ensures clause
 0000544    Plug-in > jessiefeatureassigned (cmarche)2010-07-17Enhancement on assigns annotation and the name of proof obligation
 00001021   Plug-in > jessiemajorconfirmed (cmarche)2010-07-13Jessie: struct field's validity
 0000518 1 Plug-in > jessieminorassigned (cmarche)2010-06-22Loop assigns are not taken into account when proving a safety PO
 0000502    Plug-in > jessieminorassigned (cmarche)2010-06-13Unbound label in Jessie-generated Why file when using logic function in assigns clause
 000028911 Plug-in > jessiemajoracknowledged (virgile)2010-06-09unsoundness of Jessie with respect to expression evaluation of ANSI-C
 0000485    Plug-in > jessiefeatureassigned (cmarche)2010-05-18Code containing consts should be verifiable
 0000480    Plug-in > jessiecrashassigned (cmarche)2010-05-12volatile annotation breaks type checker
 0000456 1 Plug-in > jessieminorassigned (cmarche)2010-04-23Lack of parameter generation
 0000433 1 Plug-in > jessietweakassigned (virgile)2010-03-23different translation of casted constants in program-code and in assertion
 000042431 Plug-in > jessieminorassigned (cmarche)2010-03-22Uncaught exception: Failure("Unexpected internal region in logic")
 0000416 1 Plug-in > jessieminorassigned (cmarche)2010-02-22local array decl with non-constant size causes Why error
 00000721   Plug-in > jessieminorassigned (cmarche)2010-02-12The specifications of statements are not translated
 00000792   Kernel > ACSL implementationfeatureassigned (virgile)2010-02-05Better support of //@ style
 0000387    Kernel > ACSL implementationfeatureassigned (virgile)2010-02-05ghost integer ?
 00003361   Plug-in > jessiemajorassigned (cmarche)2010-01-22cast between homogenous struct and array
 0000373    Plug-in > jessiemajorassigned (cmarche)2010-01-14Global invariants are not verified
 00003481   Plug-in > jessiemajorassigned (cmarche)2009-12-03Arithmetic safety of bitwise operators cannot be verified
 00000391   Plug-in > jessieminorconfirmed (cmarche)2009-11-24Frama-C/Jessie: memory set problem
 0000335 1 Plug-in > jessieminorassigned (cmarche)2009-11-20Unbound reference raised by Why
 0000328 1 Plug-in > jessiemajorassigned (cmarche)2009-11-13assertion failed in Jessie with bitfields inside union
 0000291 1 Plug-in > jessieminorassigned (cmarche)2009-10-20Unbound variable raised by why in presence of an unsafe cast
 0000040    Plug-in > jessieminorconfirmed (cmarche)2009-10-15Frama-C/Jessie: typing error
 000026121 Kernelminoracknowledged (virgile)2009-10-01Frama-C fails to parse a file
 0000256    Plug-in > jessieminorassigned (cmarche)2009-09-25array range in requires predicate
 0000025    Plug-in > jessieminoracknowledged (virgile)2009-09-21type invariants
 0000215 1 Plug-in > jessieminorassigned (cmarche)2009-08-25Mise en hypothèse de la précondition d'une opération appelée
 00001851   Plug-in > jessiemajorassigned (cmarche)2009-07-17Frama-C cannot process properly arrays of structures
 00001781   Plug-in > jessieminorconfirmed (cmarche)2009-07-09type error in generated why file
 00000921   Plug-in > jessieminorassigned (cmarche)2009-06-19Why error with logic functions returning a pointer
 00000421   Plug-in > jessiefeatureassigned (cmarche)2009-06-17Default invariant should be inferred for loops
 0000031    Plug-in > jessieminoracknowledged (cmarche)2009-06-17Why- error :-jessie-no-regions and assigns does not work
 0000032    Plug-in > jessieminorassigned (cmarche)2009-04-10Internal error with assign specification on bi-dimensional arrays
 0000038    Plug-in > jessieminorassigned (cmarche)2009-04-10Jessie crashes on simple program without annotations