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 none any any any any
Show: View Status: Show Sticky Issues: Changed(hrs): Use Date Filters: Relationships:
50 any No 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 / 1234)  Print Reports ]  CSV Export ]  Excel Export ] [ First Prev 1 2 3 4 5 6 7 8 9 10 11 ...  Next Last ]
    PID # Attachment count CategorySeverityStatusUpdatedSummary
  00025092   Plug-in > wpminorclosed (correnson)2020-10-15z3 ERROR: unknown parameter 'model_compress'
  00025072   Kernelmajorclosed (AllanBlanchard)2020-10-06Frama-C reports “invalid ghost in extern linkage specification” while loading files
  0002508 1 Kernelminorassigned (AllanBlanchard)2020-10-06cabs2cil fails with statements in expression in a question
  000242011 Plug-in > wpcrashresolved (correnson)2020-09-09Wp crashes on a recursive function
  000250121 Plug-in > wpmajorclosed (AllanBlanchard)2020-06-12error in generated proof obligation
  000241741 Plug-in > E-ACSLmajorclosed (bdesloges)2020-06-12Invalid label with spaghetti code and E-ACSL full mmodel
  000250231 Plug-in > Evaminorclosed (buhler)2020-06-12development version
  00024893   Kernel > libcminorclosed (maroneze)2020-06-12unistd.h declares __fc_ttyname but it has no definition
  00025065   Graphical User Interfacemajorclosed (correnson)2020-06-04Unable to right-click on MacOS to drive GUI
  0002505    Documentation > manualsminoracknowledged (maroneze)2020-05-07WP manual: hyperlink in table of contents sometimes one off
  0002504 1 Kernelminoracknowledged (virgile)2020-05-07more precise error message for missing closing } of axiomatic block
  000250031 Kernel > ACSL implementationmajorclosed (signoles)2020-03-20unbound logic variable warning for local variable
  0002498 2 Plug-in > wpminorassigned (correnson)2020-02-24munmap() breaks WP analysis
  00024182   Documentation > manualstrivialclosed (signoles)2020-02-17Outdated -rte-all option in RTE manual
  0002468123 Opammajorclosed (maroneze)2020-02-17opam fails to install frama-c
  0002378125 ptestsminorclosed (maroneze)2020-02-17Bytecode only compilation fails when linking to stdlib
  0002389182 Plug-in > wpcrashclosed (correnson)2020-02-17Failure to detect qed libraries when running wp
  000239411 Plug-in > wpmajorclosed (correnson)2020-02-17conditional input annotations result in why3 type errors
   000237131 Plug-in > wpfeatureclosed (correnson)2020-02-17suggest to provide results of commandl-line "-wp-prop" evaluation in a file in the wp-out directory
  000148421 Plug-in > wpminorclosed (correnson)2020-02-17ill-typed alt-ergo proof obligation
  000233021 Plug-in > wpminorclosed (correnson)2020-02-17known, but inferrable, yet not inferred, property not given as precodition to provers
  00018062   Plug-in > wpminorclosed (correnson)2020-02-17Error in coq code generated by wp
  0002338103 Plug-in > wpminorclosed (correnson)2020-02-17\false provable from recursive logic definition
  00024692   Documentation > websiteminorclosed (virgile)2020-02-17wrong test path given in Compiling from source - Quick Start"
  00024664   Opamblockclosed (maroneze)2020-02-17Can't build from source using opam
  00024648   Opammajorclosed (correnson)2020-02-17Potassium does not install on the given Mac version from opam
  000248231 Plug-in > wpminorclosed (correnson)2020-02-17WP warning not clear
  000247141 Plug-in > wpmajorclosed (correnson)2020-02-17frama-c/wp generates invalid why3
  000220041 Documentation > ACSLtextclosed (patrick)2020-02-17explicitly mention operator precedences when referring to Fig.2.1 "Grammar of terms" in the acsl-implementation manual
  00024503   Documentation > manualsminorclosed (patrick)2020-02-17formatting problem in acsl-implementation-18.0-Argon.pdf
  000249721 Plug-in > wpminorassigned (correnson)2020-02-03quantifiers over logic types do not restrict to valid instances
  000249111 Plug-in > clangminorassigned (fvedrine)2020-01-23incompatibilité de libc/math.h ??
  000248621 Graphical User Interfacemajorassigned (correnson)2019-11-18Left pan (file tree and plugin views) inaccessible upon resize in frama-c-gui
  0002485 1 Plug-in > wpminorassigned (correnson)2019-11-08-wp-out missing output for Why3 provers in Frama-C 20 beta
  0002484    Plug-in > wpminorassigned (correnson)2019-11-08alt-ergo support in Frama-C 20 beta
  0002483 1 Plug-in > wpminorassigned (correnson)2019-11-08Eprover in Frama-C 20 beta
  000210061 Plug-in > wpminorclosed (correnson)2019-10-17readability of coq(?) names
  000228532 Plug-in > wpfeatureclosed (correnson)2019-10-17suggest boolean expressions for "-wp-prop" arguments
  000232922 Plug-in > wptweakclosed (correnson)2019-10-17suggest unique term normalization for lemmas and goals
  000233232 Plug-in > wpmajorclosed (correnson)2019-10-17Information on C type of array is not present (in Coq)
  000233621 Plug-in > wptweakclosed (correnson)2019-10-17suggest to supply previous "ensures" as hypotheses in proof obligation of next "ensures"
  00021802   Plug-in > wpcrashclosed (correnson)2019-10-17Crash on loop with global assigns and per-behavior assigns
  000234053 Plug-in > wpminorclosed (correnson)2019-10-17Coq translation of predicate name changes when additional files are processed by Frama-C
  000235325 Plug-in > wpminorclosed (correnson)2019-10-17alt-ergo goals generated directly / via why3 differ in provability
  000238511 Plug-in > wpcrashclosed (correnson)2019-10-17Auto-generated assigns clause for a void* argument crashes wp
  000240142 Plug-in > wpmajorclosed (correnson)2019-10-17Newer releases of FramaC produce apparent WP plug-in bug
  000239081 Plug-in > wpminorclosed (correnson)2019-10-17dubious discharge of postcondition
  000240961 Plug-in > wpcrashclosed (correnson)2019-10-17crash
  000240721 Plug-in > wpmajorclosed (correnson)2019-10-17contracts about memory mapped I/O through volatile memory locations
  00024141   Plug-in > wpmajorclosed (correnson)2019-10-17Mk_addr not defined in Memory.v (coqwp via why3ide)
  [ First Prev 1 2 3 4 5 6 7 8 9 10 11 ...  Next Last ]

newfeedbackacknowledgedconfirmedassignedresolvedclosed


Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker