Issues · pub / frama-c

New issue

[wp] non-provable local typing constraints in lemmas

#2 · created May 06, 2020 by Jens Gerlach wp
- CLOSED
- 29
updated May 28, 2021
[wp] shall use per-behaviour assigns at call sites

#3 · created May 07, 2020 by Nikolai Kosmatov enhancement wp
- CLOSED
- 6
updated Aug 05, 2021
[wp] unsoundness for base-offset

#16 · created Jun 12, 2020 by Loïc Correnson wp
- CLOSED (MOVED)
- 0
updated Feb 22, 2021
WP: Incorrect assigns global/static handling

#18 · created Jun 15, 2020 by Alex Coffin wp
- CLOSED
- 1
- 1
updated Feb 22, 2021
Wanted features related to Why3-Coq

#30 · created Sep 28, 2020 by Allan Blanchard discussion enhancement wp
- 5
updated Oct 02, 2020
Z3 and CVC4 working for Frama-C 22 (Titanium) beta after some initial problems 3 of 3 tasks completed

#41 · created Nov 01, 2020 by Jens Gerlach wp
- CLOSED
- 1
- 28
updated Apr 13, 2021
Question: Dump why3 file generated by frama-c

#46 · created Dec 06, 2020 by Leo Viezens wp
- CLOSED
- 3
updated Aug 05, 2021
Why3 configuration for Frama-C

#47 · created Dec 11, 2020 by Allan Blanchard wp
- 0
updated Mar 31, 2021
An option to return error code if there are any problems with the analysis, so that frama-c is easier to be used in CI/CD workflows 3 of 3 tasks completed

#54 · created Jan 29, 2021 by varosi eva wp
- 3
updated Mar 29, 2021
z3 ERROR: unknown parameter 'model_compress'

#55 · created Oct 15, 2020 by rwmjones bug wp
- CLOSED
- 2
updated Feb 22, 2021
Wp crashes on a recursive function

#58 · created Dec 28, 2018 by Frédéric Loulergue critical wp
- CLOSED
- 1
updated Feb 22, 2021
error in generated proof obligation

#59 · created Mar 10, 2020 by Jens Gerlach bug wp
- CLOSED
- 2
updated Feb 22, 2021
munmap() breaks WP analysis

#70 · created Feb 10, 2020 by mantis-gitlab-migration bug wp
- 0
updated Feb 22, 2021
Failure to detect qed libraries when running wp

#75 · created Jul 17, 2018 by mantis-gitlab-migration critical wp
- CLOSED
- 18
updated Feb 22, 2021
conditional input annotations result in why3 type errors

#76 · created Aug 23, 2018 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Feb 22, 2021
suggest to provide results of commandl-line "-wp-prop" evaluation in a file in the wp-out directory

#77 · created Mar 22, 2018 by Jens Gerlach enhancement wp
- CLOSED
- 3
updated Feb 22, 2021
ill-typed alt-ergo proof obligation

#78 · created Sep 25, 2013 by Virgile Prevosto bug wp
- CLOSED
- 2
updated Feb 22, 2021
known, but inferrable, yet not inferred, property not given as precodition to provers

#80 · created Oct 26, 2017 by Jochen Burghardt bug wp
- CLOSED
- 2
updated Feb 22, 2021
Error in coq code generated by wp

#81 · created Jun 12, 2014 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Feb 22, 2021
\false provable from recursive logic definition

#82 · created Dec 18, 2017 by Jochen Burghardt bug wp
- CLOSED
- 10
updated Feb 22, 2021
WP warning not clear

#86 · created Oct 22, 2019 by Jens Gerlach bug wp
- CLOSED
- 3
updated Feb 22, 2021
frama-c/wp generates invalid why3

#87 · created Aug 13, 2019 by mantis-gitlab-migration bug wp
- CLOSED
- 4
updated Feb 22, 2021
quantifiers over logic types do not restrict to valid instances

#91 · created Jan 30, 2020 by mantis-gitlab-migration bug wp
- CLOSED
- 3
updated Apr 15, 2021
-wp-out missing output for Why3 provers in Frama-C 20 beta

#101 · created Nov 08, 2019 by Jens Gerlach bug wp
- 0
updated Aug 05, 2021
alt-ergo support in Frama-C 20 beta

#102 · created Nov 08, 2019 by Jens Gerlach bug wp
- CLOSED
- 0
updated Apr 14, 2021
Eprover in Frama-C 20 beta

#103 · created Nov 08, 2019 by Jens Gerlach bug wp
- CLOSED
- 1
updated Apr 15, 2021
readability of coq(?) names

#104 · created Mar 31, 2015 by Jens Gerlach bug wp
- CLOSED
- 6
updated Feb 22, 2021
suggest boolean expressions for "-wp-prop" arguments

#105 · created Feb 27, 2017 by Jochen Burghardt enhancement wp
- CLOSED
- 3
updated Feb 22, 2021
suggest unique term normalization for lemmas and goals

#106 · created Oct 09, 2017 by Jochen Burghardt enhancement wp
- CLOSED
- 2
updated Feb 22, 2021
Information on C type of array is not present (in Coq)

#107 · created Nov 22, 2017 by Jens Gerlach bug wp
- CLOSED
- 3
updated Feb 22, 2021
suggest to supply previous "ensures" as hypotheses in proof obligation of next "ensures"

#108 · created Dec 08, 2017 by Jochen Burghardt enhancement wp
- CLOSED
- 2
updated Feb 22, 2021
Crash on loop with global assigns and per-behavior assigns

#109 · created Oct 19, 2015 by Boris Yakobowski critical wp
- CLOSED
- 2
updated Feb 22, 2021
Coq translation of predicate name changes when additional files are processed by Frama-C

#111 · created Jan 04, 2018 by Jochen Burghardt bug wp
- CLOSED
- 5
updated Feb 22, 2021
alt-ergo goals generated directly / via why3 differ in provability

#112 · created Feb 01, 2018 by Jochen Burghardt bug wp
- CLOSED
- 2
updated Feb 22, 2021
Auto-generated assigns clause for a void* argument crashes wp

#113 · created Jul 05, 2018 by mantis-gitlab-migration critical wp
- CLOSED
- 1
updated Feb 22, 2021
Newer releases of FramaC produce apparent WP plug-in bug

#114 · created Oct 01, 2018 by mantis-gitlab-migration bug wp
- CLOSED
- 4
updated Feb 22, 2021
dubious discharge of postcondition

#115 · created Jul 24, 2018 by Jens Gerlach bug wp
- CLOSED
- 8
updated Feb 22, 2021
crash

#116 · created Nov 13, 2018 by mantis-gitlab-migration critical wp
- CLOSED
- 6
updated Feb 22, 2021
contracts about memory mapped I/O through volatile memory locations

#117 · created Oct 31, 2018 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Feb 22, 2021
Mk_addr not defined in Memory.v (coqwp via why3ide)

#118 · created Dec 07, 2018 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Feb 22, 2021
floating-point support is somwhat incomplete

#121 · created Jul 02, 2019 by mantis-gitlab-migration critical wp
- CLOSED
- 4
updated Feb 22, 2021
malloc breaks reasoning about assigns

#122 · created Jun 17, 2019 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Feb 22, 2021
incomplete loading of saved state when using WP?

#124 · created Mar 09, 2017 by Jens Gerlach bug wp
- CLOSED
- 2
updated Feb 22, 2021
Shape of VC depends on selection of properties

#125 · created Oct 08, 2018 by Jens Gerlach bug wp
- CLOSED
- 4
updated Sep 21, 2021
Prove of \false

#126 · created Feb 16, 2019 by Jens Gerlach bug wp
- CLOSED
- 6
updated Apr 15, 2021
number of generated files in Frama-C 18 vs 19. beta(2)

#151 · created Jun 14, 2019 by Jens Gerlach bug wp
- CLOSED
- 7
updated Feb 22, 2021
Ambiguous path error using why3

#159 · created Jun 17, 2019 by mantis-gitlab-migration bug wp
- CLOSED
- 8
updated Feb 22, 2021
Division by zero doesn't increase the number of VC in console output

#168 · created Feb 17, 2019 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Feb 22, 2021
One \valid seems sufficient to write in a whole array.

#169 · created Feb 12, 2019 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Feb 22, 2021
`strlen` used from code makes it no longer possible to prove `assigns \nothing`.

#224 · created Jun 23, 2018 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Feb 22, 2021
Some issues related to Frama-C 18.0 (beta) "Argon"

#225 · created Nov 03, 2018 by Jens Gerlach bug wp
- CLOSED
- 1
updated Feb 22, 2021
Newer releases of FramaC produce apparent WP plug-in bug

#241 · created Oct 01, 2018 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Feb 22, 2021
WP is not able to validate a statically declared structure followed by a memset

#246 · created Jul 11, 2018 by Patricia Mouy bug wp
- CLOSED
- 3
updated Feb 22, 2021
Invalid sizeof(struct) calculation in Sulfur

#259 · created Jan 19, 2018 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Feb 22, 2021
WP: internal error: only the kernel should set the status of property assumes

#261 · created Jul 04, 2018 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Feb 22, 2021
Strange difference in generated Coq code between Chlorine and Sulfur

#262 · created May 09, 2018 by Jens Gerlach critical wp
- CLOSED
- 9
updated Feb 22, 2021
statement contract apparently confuses parser

#324 · created May 11, 2017 by Jochen Burghardt critical wp
- CLOSED
- 3
updated Apr 15, 2021
false postcondition shouldn't be verified in default memory-model setting

#333 · created Jun 15, 2017 by Jochen Burghardt enhancement wp
- CLOSED
- 2
updated Apr 15, 2021
poor errors message texts for Hoare memory model checks

#334 · created Jun 15, 2017 by Jochen Burghardt wp
- CLOSED
- 1
updated Sep 21, 2021
naming the default behavior influences proven obligations

#336 · created Jun 01, 2017 by Jochen Burghardt bug wp
- CLOSED
- 1
updated Apr 15, 2021
suggest to check (loop) assigns clauses by data flow analysis

#337 · created Jun 01, 2017 by Jochen Burghardt enhancement wp
- CLOSED
- 1
updated Aug 05, 2021
type of float parameter changed unexpectedly to double

#347 · created Feb 24, 2017 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Feb 22, 2021
"loop assigns" clause ignored in presence of "for"-prefixed clauses

#350 · created May 08, 2017 by Jochen Burghardt critical wp
- CLOSED
- 3
updated Apr 15, 2021
Some ACSL mathematical functions crash WP

#351 · created May 10, 2017 by mantis-gitlab-migration critical wp
- CLOSED
- 1
updated Apr 15, 2021
axiom about bounds of lsl result needed in the long run

#352 · created May 08, 2017 by Jochen Burghardt enhancement wp
- CLOSED
- 1
updated Apr 15, 2021
Frama-C gives succeeding lemma, rather than preceding lemmas, as hypothesis to e.g. Cvc4

#353 · created Mar 16, 2017 by Jochen Burghardt bug wp
- CLOSED
- 1
updated Apr 15, 2021
signature axiom omitted in Coq and Alt-ergo translation

#354 · created Mar 13, 2017 by Jochen Burghardt bug wp
- CLOSED
- 2
updated Apr 15, 2021
Axiomatic is recompiled when using severalprocesses

#356 · created Mar 12, 2014 by Jens Gerlach bug wp
- CLOSED
- 1
updated Feb 22, 2021
Provide an option to run Coq from Frama-C

#359 · created Mar 12, 2014 by Jens Gerlach enhancement wp
- CLOSED
- 1
updated Feb 22, 2021
suggestion: translate axioms and implication premises in forward order to coq

#360 · created Mar 13, 2017 by Jochen Burghardt bug wp
- CLOSED
- 2
updated Apr 15, 2021
Why3ide cannot be opened in this version

#365 · created Mar 01, 2017 by Pierre Yves Piriou enhancement wp
- 0
updated Feb 22, 2021
lemma tacitly omitted from prover assumptions

#367 · created Feb 27, 2017 by Jochen Burghardt bug wp
- CLOSED
- 2
updated Aug 05, 2021
applicability of Coq proof script depends on order of include files

#368 · created Feb 16, 2017 by Jochen Burghardt bug wp
- CLOSED
- 1
updated Apr 15, 2021
Frama-C sleeps too much when discharging trivial goals

#369 · created Feb 13, 2017 by mantis-gitlab-migration enhancement wp
- CLOSED
- 1
updated Apr 15, 2021
problem with Qed's simplification power

#370 · created Feb 06, 2017 by Jochen Burghardt bug wp
- 1
updated Feb 22, 2021
translation to why3 of int* argument to logic function

#371 · created Feb 02, 2017 by Jochen Burghardt bug confirmed wp
- CLOSED
- 6
updated Apr 15, 2021
coq 8.5: cannot find Memory.v

#384 · created Feb 11, 2016 by Jens Gerlach bug wp
- CLOSED
- 7
updated Feb 22, 2021
WP inserts unwanted new lines into Coq proofs

#385 · created Jan 02, 2017 by Jens Gerlach bug wp
- CLOSED
- 1
updated Apr 15, 2021
Why3 warning

#387 · created Dec 16, 2016 by Jens Gerlach bug wp
- CLOSED
- 2
updated Apr 15, 2021
more prover processes run than expected

#388 · created Dec 15, 2016 by Jens Gerlach bug wp
- CLOSED
- 4
updated Apr 15, 2021
Frama-C is unsound when employing both alt-ergo and cvc4

#394 · created Jun 30, 2016 by Jochen Burghardt bug wp
- CLOSED
- 5
updated Feb 22, 2021
Switch statements seem to be unsound

#397 · created Aug 19, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 3
updated Feb 22, 2021
"Builtin already registered" after Reparse

#398 · created Jul 30, 2016 by mantis-gitlab-migration critical wp
- CLOSED
- 2
updated Feb 22, 2021
workaround for coq-8.5.1 issue?

#403 · created Jun 16, 2016 by Jochen Burghardt enhancement wp
- CLOSED
- 7
updated Feb 22, 2021
error in Coq file generation

#405 · created Dec 03, 2016 by Alain Giorgetti bug wp
- CLOSED
- 1
updated Apr 15, 2021
Nested scopes may cause issues with the validity of created pointers

#409 · created Aug 17, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Apr 15, 2021
Logic with read clauses can have their values invalidated by writes to separated memory locations

#410 · created Aug 08, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Aug 05, 2021
Implicit casting from integer to real causes failure in WP proof generation

#413 · created Jul 29, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Apr 15, 2021
Creating a pointer to a local causes valid pointers above it to lose thier valid status

#425 · created Jun 21, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Apr 15, 2021
alt-ergo: undefined symbol andb

#489 · created Sep 14, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Feb 22, 2021
Zombie processes

#491 · created Sep 01, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 3
updated Feb 22, 2021
Under windows, many times, Frama-c wp process doesn't kill alt-ergo process before finishing

#492 · created Jun 11, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 0
updated Feb 22, 2021
missing lower bound of ACSL operator ".." not detected by Magnesium

#494 · created Jun 13, 2016 by Jochen Burghardt enhancement wp
- CLOSED
- 6
updated Feb 22, 2021
Suggest to supply values of global consts to provers

#498 · created May 10, 2012 by Jochen Burghardt enhancement wp
- CLOSED
- 13
updated Feb 22, 2021
Unexpected error (Invalid_argument("Z.shift_left: count argument must be positive"))

#499 · created Jan 22, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated May 18, 2021
coq fails to compile Cint because Zbits is not found

#501 · created Sep 02, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 3
updated Feb 22, 2021
Reals are bad encoded for coq

#504 · created Mar 03, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 0
updated Feb 22, 2021
Use of very large real constants cause failures in proof generation in WP

#507 · created Jun 14, 2016 by mantis-gitlab-migration critical wp
- CLOSED
- 1
updated Apr 14, 2021
Validation fails when predicate is used with implicit type conversion.

#508 · created May 31, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Apr 15, 2021
Oddities in the modeling of floats and doubles

#509 · created May 16, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Apr 15, 2021