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 (101 - 150 / 294)  Print Reports ]  CSV Export ]  Excel Export ] [ First Prev 1 2 3 4 5 6 Next Last ]
    PID # Attachment count CategorySeverityStatusUpdatedSummary
  0002308 1 Plug-in > wpfeatureassigned (correnson)2017-06-01suggest to check (loop) assigns clauses by data flow analysis
  000230752 Kernelminorassigned (virgile)2017-05-31preprocessor fail: unterminated comment
  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
  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
  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
  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)
  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
  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
  0002241 1 Plug-in > wpmajorassigned (correnson)2016-07-29Implicit casting from integer to real causes failure in WP proof generation
  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
  00021621   Kernel > Makefileminorassigned (bobot)2016-06-21Compilation of kernel native cmx is messed up with plugin makefile
  00021632   Kernelfeatureassigned (bobot)2016-06-21Namespace through packs - packing frama-c cmx into a cmxa
  00021981   Documentationminorassigned (correnson)2016-06-21typo in output of 'frama-c -wp-help'
  0002232 1 Plug-in > wpcrashassigned (correnson)2016-06-14Use of very large real constants cause failures in proof generation in WP
  0002229 1 Plug-in > wpminorassigned (correnson)2016-05-31Validation fails when predicate is used with implicit type conversion.
  0002228    Plug-in > wpminorassigned (correnson)2016-05-16Oddities in the modeling of floats and doubles
  000222372 Kernel > Makefiletextassigned (virgile)2016-05-10Frama-C upgrade installation not foolproof
  000222641 Kernelminorassigned (correnson)2016-05-04insertion of "assert true" after a statement influences provability of the statement's contract
  0002222 1 Plug-in > wpminorassigned (correnson)2016-04-09Make find(1) command POSIX-compliant
  000221911 Plug-in > wpcrashassigned (correnson)2016-03-22Crash with large array initialisation
  000191131 Plug-in > wpminoracknowledged (correnson)2016-03-07WP detect a non-natural loop on a do-while(0) loop
  000220544 Plug-in > wpminorconfirmed (correnson)2016-02-04zombie processes (again)
  0002207 1 Plug-in > wpcrashassigned (correnson)2016-02-03WP crashes with \pointer_comparable
  0002197 1 Kernel > ACSL implementationfeatureassigned (virgile)2015-12-07expression "term!=term" is considered always a predicate, rather than (in some contexts) a term
  00021951   Kernel > ACSL implementationmajorassigned (virgile)2015-12-06ambiguity with consecutive comparison and ternary expressions
  0002196    Kernel > ACSL implementationfeatureassigned (virgile)2015-12-05No syntax to apply lambda expressions
  000218911 Plug-in > wptweakassigned (correnson)2015-12-03Frama-C runs out of memory on small C program (combinatorial explosion in analysis of "main"?)
  0002188 3 Plug-in > wpminorassigned (correnson)2015-11-30bit_test axiomatization doesn't imply == equality from bit-by-bit equality for e.g. uint32
  0001718    Kernelfeatureassigned (virgile)2015-11-04Nested VLA are not supported
  [ First Prev 1 2 3 4 5 6 Next Last ]


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker