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


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker