| | |  | 0002509 | 2 | |
Plug-in > wp | minor | closed (correnson) | 2020-10-15 | z3 ERROR: unknown parameter 'model_compress' |
| | | | 0002507 | 2 | |
Kernel | major | closed (AllanBlanchard) | 2020-10-06 | Frama-C reports “invalid ghost in extern linkage specification” while loading files |
| | |  | 0002508 | | 1 |
Kernel | minor | assigned (AllanBlanchard) | 2020-10-06 | cabs2cil fails with statements in expression in a question |
| | | | 0002420 | 1 | 1 |
Plug-in > wp | crash | resolved (correnson) | 2020-09-09 | Wp crashes on a recursive function |
| | | | 0002501 | 2 | 1 |
Plug-in > wp | major | closed (AllanBlanchard) | 2020-06-12 | error in generated proof obligation |
| | | | 0002417 | 4 | 1 |
Plug-in > E-ACSL | major | closed (bdesloges) | 2020-06-12 | Invalid label with spaghetti code and E-ACSL full mmodel |
| | | | 0002502 | 3 | 1 |
Plug-in > Eva | minor | closed (buhler) | 2020-06-12 | development version |
| | | | 0002489 | 3 | |
Kernel > libc | minor | closed (maroneze) | 2020-06-12 | unistd.h declares __fc_ttyname but it has no definition |
| | | | 0002506 | 5 | |
Graphical User Interface | major | closed (correnson) | 2020-06-04 | Unable to right-click on MacOS to drive GUI |
| | | | 0002505 | | |
Documentation > manuals | minor | acknowledged (maroneze) | 2020-05-07 | WP manual: hyperlink in table of contents sometimes one off |
| | | | 0002504 | | 1 |
Kernel | minor | acknowledged (virgile) | 2020-05-07 | more precise error message for missing closing } of axiomatic block |
| | |  | 0002500 | 3 | 1 |
Kernel > ACSL implementation | major | closed (signoles) | 2020-03-20 | unbound logic variable warning for local variable |
| | | | 0002498 | | 2 |
Plug-in > wp | minor | assigned (correnson) | 2020-02-24 | munmap() breaks WP analysis |
| | | | 0002418 | 2 | |
Documentation > manuals | trivial | closed (signoles) | 2020-02-17 | Outdated -rte-all option in RTE manual |
| | | | 0002468 | 12 | 3 |
Opam | major | closed (maroneze) | 2020-02-17 | opam fails to install frama-c |
| | | | 0002378 | 12 | 5 |
ptests | minor | closed (maroneze) | 2020-02-17 | Bytecode only compilation fails when linking to stdlib |
| | | | 0002389 | 18 | 2 |
Plug-in > wp | crash | closed (correnson) | 2020-02-17 | Failure to detect qed libraries when running wp |
| | | | 0002394 | 1 | 1 |
Plug-in > wp | major | closed (correnson) | 2020-02-17 | conditional input annotations result in why3 type errors |
| | | | 0002371 | 3 | 1 |
Plug-in > wp | feature | closed (correnson) | 2020-02-17 | suggest to provide results of commandl-line "-wp-prop" evaluation in a file in the wp-out directory |
| | | | 0001484 | 2 | 1 |
Plug-in > wp | minor | closed (correnson) | 2020-02-17 | ill-typed alt-ergo proof obligation |
| | | | 0002330 | 2 | 1 |
Plug-in > wp | minor | closed (correnson) | 2020-02-17 | known, but inferrable, yet not inferred, property not given as precodition to provers |
| | | | 0001806 | 2 | |
Plug-in > wp | minor | closed (correnson) | 2020-02-17 | Error in coq code generated by wp |
| | | | 0002338 | 10 | 3 |
Plug-in > wp | minor | closed (correnson) | 2020-02-17 | \false provable from recursive logic definition |
| | | | 0002469 | 2 | |
Documentation > website | minor | closed (virgile) | 2020-02-17 | wrong test path given in Compiling from source - Quick Start" |
| | | | 0002466 | 4 | |
Opam | block | closed (maroneze) | 2020-02-17 | Can't build from source using opam |
| | | | 0002464 | 7 | |
Opam | major | closed (correnson) | 2020-02-17 | Potassium does not install on the given Mac version from opam |
| | | | 0002482 | 3 | 1 |
Plug-in > wp | minor | closed (correnson) | 2020-02-17 | WP warning not clear |
| | | | 0002471 | 4 | 1 |
Plug-in > wp | major | closed (correnson) | 2020-02-17 | frama-c/wp generates invalid why3 |
| | | | 0002200 | 4 | 1 |
Documentation > ACSL | text | closed (patrick) | 2020-02-17 | explicitly mention operator precedences when referring to Fig.2.1 "Grammar of terms" in the acsl-implementation manual |
| | | | 0002450 | 3 | |
Documentation > manuals | minor | closed (patrick) | 2020-02-17 | formatting problem in acsl-implementation-18.0-Argon.pdf |
| | | | 0002497 | 2 | 1 |
Plug-in > wp | minor | assigned (correnson) | 2020-02-03 | quantifiers over logic types do not restrict to valid instances |
| | | | 0002491 | | 1 |
Plug-in > clang | minor | assigned (fvedrine) | 2020-01-23 | incompatibilité de libc/math.h ?? |
| | |  | 0002486 | 2 | 1 |
Graphical User Interface | major | assigned (correnson) | 2019-11-18 | Left pan (file tree and plugin views) inaccessible upon resize in frama-c-gui |
| | | | 0002485 | | 1 |
Plug-in > wp | minor | assigned (correnson) | 2019-11-08 | -wp-out missing output for Why3 provers in Frama-C 20 beta |
| | | | 0002484 | | |
Plug-in > wp | minor | assigned (correnson) | 2019-11-08 | alt-ergo support in Frama-C 20 beta |
| | | | 0002483 | | 1 |
Plug-in > wp | minor | assigned (correnson) | 2019-11-08 | Eprover in Frama-C 20 beta |
| | | | 0002100 | 6 | 1 |
Plug-in > wp | minor | closed (correnson) | 2019-10-17 | readability of coq(?) names |
| | | | 0002285 | 3 | 2 |
Plug-in > wp | feature | closed (correnson) | 2019-10-17 | suggest boolean expressions for "-wp-prop" arguments |
| | | | 0002329 | 2 | 2 |
Plug-in > wp | tweak | closed (correnson) | 2019-10-17 | suggest unique term normalization for lemmas and goals |
| | | | 0002332 | 3 | 2 |
Plug-in > wp | major | closed (correnson) | 2019-10-17 | Information on C type of array is not present (in Coq) |
| | | | 0002336 | 2 | 1 |
Plug-in > wp | tweak | closed (correnson) | 2019-10-17 | suggest to supply previous "ensures" as hypotheses in proof obligation of next "ensures" |
| | | | 0002180 | 1 | |
Plug-in > wp | crash | closed (correnson) | 2019-10-17 | Crash on loop with global assigns and per-behavior assigns |
| | | | 0002340 | 5 | 3 |
Plug-in > wp | minor | closed (correnson) | 2019-10-17 | Coq translation of predicate name changes when additional files are processed by Frama-C |
| | | | 0002353 | 2 | 5 |
Plug-in > wp | minor | closed (correnson) | 2019-10-17 | alt-ergo goals generated directly / via why3 differ in provability |
| | | | 0002385 | 1 | 1 |
Plug-in > wp | crash | closed (correnson) | 2019-10-17 | Auto-generated assigns clause for a void* argument crashes wp |
| | | | 0002401 | 4 | 2 |
Plug-in > wp | major | closed (correnson) | 2019-10-17 | Newer releases of FramaC produce apparent WP plug-in bug |
| | | | 0002390 | 8 | 1 |
Plug-in > wp | minor | closed (correnson) | 2019-10-17 | dubious discharge of postcondition |
| | | | 0002409 | 5 | 1 |
Plug-in > wp | crash | closed (correnson) | 2019-10-17 | crash |
| | | | 0002407 | 2 | 1 |
Plug-in > wp | major | closed (correnson) | 2019-10-17 | contracts about memory mapped I/O through volatile memory locations |
| | | | 0002414 | 1 | |
Plug-in > wp | major | closed (correnson) | 2019-10-17 | Mk_addr not defined in Memory.v (coqwp via why3ide) |
