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 (1 - 50 / 241)  Print Reports ]  CSV Export ]  Excel Export ] [ First Prev 1 2 3 4 5 Next Last ]
    PID # Attachment count CategorySeverityStatusUpdatedSummary
  000232912 Plug-in > wptweakassigned (correnson)2017-10-12suggest unique term normalization for lemmas and goals
  000228512 Plug-in > wpfeatureassigned (correnson)2017-10-09suggest boolean expressions for "-wp-prop" arguments
  000210051 Plug-in > wpminoracknowledged (correnson)2017-10-09readability of coq(?) names
  00023285   Plug-in > E-ACSLcrashacknowledged (kvorobyov)2017-09-15compilation fails on i386 with gcc-7
  000231422 Plug-in > RTEmajorassigned (signoles)2017-09-01Incorrect overflow and cast assertions for bitfields
  000232242 Kernelcrashresolved (virgile)2017-08-25repeated predicate definitions in separate file cause crash
  00023271   Plug-in > E-ACSLminorassigned (signoles)2017-08-25Failure to detect overflows into an allocated area within a struct
  000232111 Plug-in > slicingminorfeedback (Nikolai_Kosmatov)2017-08-02crash
  000230121 Plug-in > wpcrashassigned (correnson)2017-07-21statement contract apparently confuses parser
  0002317    Documentation > manualstextassigned (correnson)2017-07-19Statement contracts and WP
  0002316 1 Plug-in > PathCrawlerminorassigned (nicky)2017-07-07Instrumentation Failure Error in Online Pathcrawler
  000220021 Documentation > ACSLtextacknowledged (patrick)2017-06-28explicitly mention operator precedences when referring to Fig.2.1 "Grammar of terms" in the acsl-implementation manual
  00023131   Documentation > manualstextassigned (correnson)2017-06-23suggestions for improvement of Sect.3.6 and 3.7 of the wp manual
  000231211 Plug-in > wptweakassigned (correnson)2017-06-15false postcondition shouldn't be verified in default memory-model setting
  0002311 1 Plug-in > wptextassigned (correnson)2017-06-15poor errors message texts for Hoare memory model checks
  00022533   Kernel > libcminorresolved (maroneze)2017-06-14File frama-c/libc/features.h should include definition of the macro __GNUC_PREREQ from file /usr/include/features.h
  0002310 1 Plug-in > E-ACSLminorassigned (kvorobyov)2017-06-14Incorrect handling of \initialized when initialized struct is passed to a function by value
  00014673   Kernelfeatureresolved (valentin.perrelle)2017-06-09Parser does not handle mixed concatenations of wide and non-wide strings
  0002309 1 Plug-in > wpminorassigned (correnson)2017-06-01naming the default behavior influences proven obligations
  0002308 1 Plug-in > wpfeatureassigned (correnson)2017-06-01suggest to check (loop) assigns clauses by data flow analysis
  000229721 Kernelminorresolved (maroneze)2017-05-31syntax error before loop contract reported after loop contract
  000230621 Kernelminorassigned (yakobowski)2017-05-31Support for flexible array members
  000230752 Kernelminorassigned (virgile)2017-05-31preprocessor fail: unterminated comment
  0002305 2 Plug-in > E-ACSLminorassigned (kvorobyov)2017-05-31E-ACSL: proper bitfileds handling
  0002304 2 Plug-in > E-ACSLmajorassigned (kvorobyov)2017-05-29E-ACSL: compilation fail: generated functions doesn't have static inline attributes
  0002303 2 Plug-in > E-ACSLmajorassigned (kvorobyov)2017-05-29E-ACSL generates functions definitions without argument-names
  0002302 1 Plug-in > slicingmajorassigned (Nikolai_Kosmatov)2017-05-23the return statement of a called function was wrongly removed
  000229822 Plug-in > wpcrashassigned (correnson)2017-05-11"loop assigns" clause ignored in presence of "for"-prefixed clauses
  0002299 1 Plug-in > wpblockassigned (correnson)2017-05-10Some ACSL mathematical functions crash WP
  0002296 1 Plug-in > wpfeatureassigned (correnson)2017-05-08axiom about bounds of lsl result needed in the long run
  0002293 3 Plug-in > wpminorassigned (correnson)2017-03-16Frama-C gives succeeding lemma, rather than preceding lemmas, as hypothesis to e.g. Cvc4
  000229217 Plug-in > wpminorassigned (correnson)2017-03-16signature axiom omitted in Coq and Alt-ergo translation
  00017611   Kernel > ACSL implementationmajorassigned (virgile)2017-03-14Check that all occurrences of *p in assigns are guarded by a \valid(p) in requires
  000062811 Plug-in > jessieminorassigned (cmarche)2017-03-14Frama-C/Jessie does not recognize the length of array in struct
  000229113 Plug-in > wpminorassigned (correnson)2017-03-13suggestion: translate axioms and implication premises in forward order to coq
  000229011 Kernelminorassigned (correnson)2017-03-10incomplete loading of saved state when using WP?
  00022704   Graphical User Interfacemajorconfirmed (maroneze)2017-03-06Command "Show callgraph" fails.
  00022593   Plug-in > value analysistextassigned (yakobowski)2017-03-06suggest to provide and document a unique warning string to grep for in value-analysis output files
  000225631 Plug-in > value analysisminorassigned (yakobowski)2017-03-06"pointer comparison" warning emitted for "p==NULL"
  0002289    Plug-in > wpfeatureassigned (correnson)2017-03-01Why3ide cannot be opened in this version
  000228614 Plug-in > wpminorassigned (correnson)2017-02-27lemma tacitly omitted from prover assumptions
  0002282 2 Plug-in > wpminorassigned (correnson)2017-02-16applicability of Coq proof script depends on order of include files
  0002280 1 Plug-in > wptweakassigned (correnson)2017-02-14Frama-C sleeps too much when discharging trivial goals
  000227812 Plug-in > wpminoracknowledged (correnson)2017-02-06problem with Qed's simplification power
  00022762   Graphical User Interfacetweakfeedback (maroneze)2017-02-06Duplicates are created on the tab "Messages"
  000227556 Plug-in > wpminorconfirmed (correnson)2017-02-03translation to why3 of int* argument to logic function
  00022741   Kerneltweakconfirmed (maroneze)2017-01-24It is impossble to change log file without kinds of message changing.
  000227221 Kernelminorassigned (virgile)2017-01-16WP appears to assume left-to-right evaluation order for int addition
  00009453   Plug-in > value analysisminorassigned (maroneze)2017-01-12Should warn for overlapping lv=lv; assignments
  000226411 Kernel > ACSL implementationmajorassigned (virgile)2017-01-04structure in logic not supported?
  [ First Prev 1 2 3 4 5 Next Last ]


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker