Unassigned [ ^ ] (0 - 0 / 0)

Resolved [ ^ ] (1 - 10 / 17) 0002482 WP warning not clear Plug-in > wp - 2019-10-22 23:35 0002330 known, but inferrable, yet not inferred, property not given as precodition to provers Plug-in > wp - 2019-10-17 17:30 0001484 ill-typed alt-ergo proof obligation Plug-in > wp - 2019-10-17 17:11 0002371   suggest to provide results of commandl-line "-wp-prop" evaluation in a file in the wp-out directory Plug-in > wp - 2019-10-17 17:11 0002394 conditional input annotations result in why3 type errors Plug-in > wp - 2019-10-17 17:05 0002389 Failure to detect qed libraries when running wp Plug-in > wp - 2019-10-17 16:30 0002338 \false provable from recursive logic definition Plug-in > wp - 2019-10-17 15:30 0002464 Potassium does not install on the given Mac version from opam Opam - 2019-10-17 14:50 0001806 Error in coq code generated by wp Plug-in > wp - 2019-10-17 14:35 0002471 frama-c/wp generates invalid why3 Plug-in > wp - 2019-10-17 14:29

Recently Modified [ ^ ] (1 - 10 / 1220) 0002485 -wp-out missing output for Why3 provers in Frama-C 20 beta Plug-in > wp - 2019-11-08 13:19 0002484 alt-ergo support in Frama-C 20 beta Plug-in > wp - 2019-11-08 13:03 0002483 Eprover in Frama-C 20 beta Plug-in > wp - 2019-11-08 12:53 0002482 WP warning not clear Plug-in > wp - 2019-10-22 23:35 0002100 readability of coq(?) names Plug-in > wp - 2019-10-17 18:03 0002285 suggest boolean expressions for "-wp-prop" arguments Plug-in > wp - 2019-10-17 18:03 0002329 suggest unique term normalization for lemmas and goals Plug-in > wp - 2019-10-17 18:02 0002332 Information on C type of array is not present (in Coq) Plug-in > wp - 2019-10-17 18:02 0002336 suggest to supply previous "ensures" as hypotheses in proof obligation of next "ensures" Plug-in > wp - 2019-10-17 18:02 0002180 Crash on loop with global assigns and per-behavior assigns Plug-in > wp - 2019-10-17 18:01

new

feedback

acknowledged

confirmed

assigned

resolved

closed