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 / 229)  Print Reports ]  CSV Export ]  Excel Export ] [ First Prev 1 2 3 4 5 Next Last ]
    PID # Attachment count CategorySeverityStatusUpdatedSummary
  000213742 Plug-in > value analysisminorresolved (yakobowski)2017-03-31value analysis introduces weird pointer assert with variable length arrays
  000073351 Plug-in > inoutminorresolved (yakobowski)2017-03-31Invalid results in presence of pseudo-recursive calls in inout and from
  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?
  000227771 Plug-in > value analysismajorresolved (yakobowski)2017-03-08Operability depends on the order of options changes
  00022793   Plug-in > value analysistweakresolved (yakobowski)2017-03-07EVA analysis does not start with click on "Execution" button.
  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"
  0001740 1 Plug-in > E-ACSLmajorresolved (signoles)2017-03-02Incorrectness when early exiting a block
  0002284 1 Plug-in > E-ACSLcrashresolved (signoles)2017-03-01E-ACSL type system crash
  00022832   Plug-in > wpminorresolved (correnson)2017-03-01type of float parameter changed unexpectedly to double
  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
  0002285 1 Plug-in > wpfeatureassigned (correnson)2017-02-27suggest boolean expressions for "-wp-prop" arguments
  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
  0002252 1 Plug-in > E-ACSLminorresolved (signoles)2017-01-25GMP typing issue
  00022741   Kerneltweakconfirmed (maroneze)2017-01-24It is impossble to change log file without kinds of message changing.
   0002269    Plug-in > obfuscatortextresolved (signoles)2017-01-19There is a typo in description of plug-in: "objuscator" instead of "obfuscator".
  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?
  0002266    Plug-in > wpminorassigned (correnson)2017-01-02WP inserts unwanted new lines into Coq proofs
  0002265 1 Kernel > ACSL implementationminorassigned (virgile)2017-01-02label Pre in function contracts
  00022631   Plug-in > wpminorassigned (correnson)2016-12-16Why3 warning
  000226231 Plug-in > wpminorassigned (correnson)2016-12-16more prover processes run than expected
  00022618   Plug-in > wpminorassigned (virgile)2016-12-16wp: the example from Getting Started guide doesn't work (all goals are Unknown)
  00022353   Kernelcrashresolved (virgile)2016-12-12Functions that claim to return a struct but don't cause a crash
  000224821 Kerneltextassigned (virgile)2016-12-08option "-print" prints array upper bound in type before parameter name, rather than after it
  0002260    Plug-in > wpminorassigned (correnson)2016-12-03error in Coq file generation
  00022532   Kernel > libcminorassigned (maroneze)2016-11-21File frama-c/libc/features.h should include definition of the macro __GNUC_PREREQ from file /usr/include/features.h
  0002254 1 Plug-in > value analysisminorassigned (yakobowski)2016-11-07Option "-lib-entry" results misses possible values of function pointers
  0002194    Plug-in > E-ACSLminorassigned (signoles)2016-09-13Failure to record global variable with initialiser
  0002245 1 Plug-in > wpmajorassigned (correnson)2016-08-17Nested scopes may cause issues with the validity of created pointers
  0002244 1 Plug-in > wpmajorassigned (correnson)2016-08-08Logic with read clauses can have their values invalidated by writes to separated memory locations
  0002236    Documentation > manualstextassigned (patrick)2016-08-03tset issues in manual "acsl-implementation-Aluminium-20160501.pdf"
  0002241 1 Plug-in > wpmajorassigned (correnson)2016-07-29Implicit casting from integer to real causes failure in WP proof generation
  000220011 Documentation > ACSLtextacknowledged (patrick)2016-07-22explicitly mention operator precedences when referring to Fig.2.1 "Grammar of terms" in the acsl-implementation manual
  00021876   Documentation > ACSLtextassigned (patrick)2016-07-22Grammar omissions in 1.9
  00014672   Kernelfeatureconfirmed2016-07-05Parser does not handle mixed concatenations of wide and non-wide strings
  0002234    Plug-in > wpmajorassigned (correnson)2016-06-21Creating a pointer to a local causes valid pointers above it to lose thier valid status
  00012786   Kernel > Makefiletweakassigned (bobot)2016-06-21Path for 'make install-doc-code' for external plug-in
  [ First Prev 1 2 3 4 5 Next Last ]


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker