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 (201 - 250 / 271)  Print Reports ]  CSV Export ]  Excel Export ] [ First Prev 1 2 3 4 5 6 Next Last ]
    PID # Attachment count CategorySeverityStatusUpdatedSummary
  00009672   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 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
  00005022   Plug-in > jessieminorassigned (cmarche)2010-06-13Unbound label in Jessie-generated Why file when using logic function in assigns clause
  000028921 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
  [ First Prev 1 2 3 4 5 6 Next Last ]


Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker