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 closed (And Above) any any any any
Show: View Status: Show Sticky Issues: Changed(hrs): Use Date Filters: Relationships:
50 any Yes 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 (151 - 200 / 282)  Print Reports ]  CSV Export ]  Excel Export ] [ First Prev 1 2 3 4 5 6 Next Last ]
    PID # Attachment count CategorySeverityStatusUpdatedSummary
  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.
  00014542   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
  00007504   Kernel > ACSL implementationfeatureacknowledged (virgile)2014-02-12Several [invariant] at a program point
  00012812   Plug-in > wpminoracknowledged (correnson)2014-02-05do { ... } while (0) pattern causes wp to fail
  00014951   Kernel > ACSL implementationminorassigned (virgile)2014-02-05crash
  000155641 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
  000076551 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
  [ First Prev 1 2 3 4 5 6 Next Last ]


Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker