2021-03-02 00:20 CET

Viewing Issues (101 - 150 / 269)  Print Reports ]  CSV Export ]  Excel Export ] [ First Prev 1 2 3 4 5 6 Next Last ]
    PID # Attachment count CategorySeverityStatusUpdatedSummary
  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