Frama-C Bug Tracking System

Reporter: Monitored By: Assigned To: Category: Severity: Resolution: Profile:
any any any any any any any
Status: Hide Status: Product Version: Fixed in Version: Target Version: Priority:
any none any any any any
Show: View Status: Show Sticky Issues: Changed(hrs): Use Date Filters: Relationships:
50 any No 6 No any
Platform: OS: OS Version: Tags:
any any any
Note By: any Sort by: Updated Descending  
Match Type: All Conditions  
- Search  Advanced Filters ]

Viewing Issues (351 - 400 / 1220)  Print Reports ]  CSV Export ]  Excel Export ] [ First Prev  ... 3 4 5 6 7 8 9 10 11 12 13 ...  Next Last ]
    PID # Attachment count CategorySeverityStatusUpdatedSummary
  00021901   Plug-in > wpminorclosed (correnson)2016-01-26WP output of loop variant's goal doesn't have location of loop variant
  000212711 Plug-in > wpminorclosed (correnson)2016-01-26Unprovable inequality involving (unsigned) -1
  00021261   Plug-in > wpmajorclosed (correnson)2016-01-26WP crashes on generation of PO for assigns clause (assertion failure in MemVar.ml)
  000087551 Plug-in > Evafeatureclosed (yakobowski)2016-01-26suggest to issue a warning on (<)-comparisons between pointers, unless both are non-null
  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
  00021851   Plug-in > Evaminorclosed (yakobowski)2015-12-04Recursive calls in value analysis
  000218911 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
  00005754   Kernel > ACSL implementationminorclosed (virgile)2015-09-24set of set
  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
  0002165    Kernel > Makefilefeatureclosed (signoles)2015-09-16Relocable buckx
  00021601   Plug-in > wpminoracknowledged (correnson)2015-09-15assertion failure using memset on a char
  00017841   Documentation > ACSLminorclosed (patrick)2015-09-09typo in grammar
  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
  000101741 Kernel > ACSL implementationfeatureclosed (virgile)2015-08-03suggest to warn about ensures clauses containing only \old variables
  000069011   Plug-in > slicingfeatureclosed (yakobowski)2015-08-03Slicing does not preserve some ACSL constructs
  000199211 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
  00021381   Plug-in > wpmajorclosed (correnson)2015-06-29deficient axioms
  00020442   Plug-in > wpminorclosed (correnson)2015-06-29Sessions and WP do not interact properly
  00020411   Plug-in > wpminoracknowledged (correnson)2015-06-29unable to use lemma separated_region
  0002099141 Graphical User Interfacecrashclosed (correnson)2015-06-29Frama-C GUI crashes under OS X
  00021181   Plug-in > wpminorclosed (correnson)2015-06-29do ... while{ } loop and -wp-invariants option
  000212323 Plug-in > wpminoracknowledged (correnson)2015-06-29validity of obligation from statement contract depends on whether the statement is enclosed in block {}
  00021332   Plug-in > wpmajorclosed (correnson)2015-06-29requires in beahviors do not behave as expected
  000212921 Plug-in > wpmajorclosed (correnson)2015-06-29Range of remainder of two positive integers, wrong and missing assertions.
  000213021 Plug-in > wpmajorclosed (correnson)2015-06-29*off == off_cpy cannot be proven just after the assignment *off = off_cpy
  0002134    Kernel > ACSL implementationminorassigned (virgile)2015-06-12Weak and Strong Invariants are not supported
  000212811 Plug-in > wpminorclosed (virgile)2015-06-08*i == *j cannot be proven from i == j
  00016363   Plug-in > E-ACSLmajorclosed (signoles)2015-06-08E-ACSL: executes "__store_block()" but never "__delete_block()"!
  000183751 Plug-in > E-ACSLminorclosed (signoles)2015-06-08Literal strings can be added multiple times in memory
  00021251   Kernel > ACSL implementationminorconfirmed (virgile)2015-06-02Redefintion of variables in same scope is allowed in annotations
  00015033   Kernelminorclosed (virgile)2015-05-10failure: invalid implicit conversion from void to int
  000168832 Plug-in > wpminorclosed (correnson)2015-03-17CVC4 results are not displayed in the GUI
  00017881   Documentation > ACSLminorclosed (virgile)2015-03-17predicate-def and logic-predicate-def
  000190741 Plug-in > Evaminorclosed (yakobowski)2015-03-17Value abort because of Zero-sized location
  00019195   Graphical User Interfacecrashclosed (yakobowski)2015-03-17Segmentation fault when launching frama-c-gui with OCaml 4.02.0
  000192221 Plug-in > wpcrashclosed (correnson)2015-03-17WP-Plugin crashes due to an internal error
  00020671   Plug-in > wpminorclosed (bobot)2015-03-17Frama-C does not work with versions of Why3 newer than 0.83
  [ First Prev  ... 3 4 5 6 7 8 9 10 11 12 13 ...  Next Last ]

newfeedbackacknowledgedconfirmedassignedresolvedclosed


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker