Issues · pub / frama-c

New issue

[wp] shall use per-behaviour assigns at call sites

#3 · created May 07, 2020 by Nikolai Kosmatov enhancement wp
- 5
updated Feb 22, 2021
suspicious Coq code for ACSL lemma in Frama-C 21 3 of 3 tasks completed

#19 · created Jun 17, 2020 by Jens Gerlach
- 9
updated Feb 22, 2021
No Why3 libraries compiled for PVS

#21 · created Jul 27, 2020 by Mariano Moscato
- 7
updated Feb 22, 2021
[Frama-Clang] Cannot refer to variables declared within a block in assertions placed just before the closing brace. 3 of 3 tasks completed

#22 · created Aug 02, 2020 by Jakub Szabelewski
- 0
updated Feb 22, 2021
[wp] Infinite loop related to WP cache. 3 of 3 tasks completed

#28 · created Sep 09, 2020 by Veenstra
- 0
updated Oct 22, 2020
Wanted features related to Why3-Coq

#30 · created Sep 28, 2020 by Allan Blanchard discussion enhancement wp
- 5
updated Oct 02, 2020
Unexpected incompatible pointers types

#32 · created Oct 07, 2020 by Bob Rubbens
- 3
updated Oct 28, 2020
Frama-C --version lacks \n

#35 · created Oct 15, 2020 by libguestfs
- 1
updated Oct 15, 2020
non-compilable slice produced by frama-c

#36 · created Oct 23, 2020 by Ivan Postolski bug confirmed slicing
- 2
updated Nov 18, 2020
Question: Dump why3 file generated by frama-c

#46 · created Dec 06, 2020 by Leo Viezens wp
- 2
updated Mar 29, 2021
Why3 configuration for Frama-C

#47 · created Dec 11, 2020 by Allan Blanchard wp
- 0
updated Mar 31, 2021
Documentation for Report plug-in is not correct 3 of 3 tasks completed

#53 · created Jan 29, 2021 by varosi documentation report
- 2
updated Mar 29, 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
cabs2cil fails with statements in expression in a question

#57 · created Jun 10, 2020 by mantis-gitlab-migration bug kernel
- 0
updated Feb 22, 2021
WP manual: hyperlink in table of contents sometimes one off

#65 · created Apr 16, 2020 by Jens Gerlach bug documentation
- 0
updated Feb 22, 2021
more precise error message for missing closing } of axiomatic block

#66 · created Mar 26, 2020 by Jens Gerlach bug kernel
- 0
updated Feb 22, 2021
munmap() breaks WP analysis

#70 · created Feb 10, 2020 by mantis-gitlab-migration bug wp
- 0
updated Feb 22, 2021
incompatibilité de libc/math.h ??

#97 · created Jan 22, 2020 by Nicky Williams bug frama-clang
- 1
updated Feb 22, 2021
Left pan (file tree and plugin views) inaccessible upon resize in frama-c-gui

#100 · created Nov 16, 2019 by mantis-gitlab-migration bug gui
- 2
updated Feb 22, 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 Feb 22, 2021
Shape of VC depends on selection of properties

#125 · created Oct 08, 2018 by Jens Gerlach bug wp
- 3
updated Feb 22, 2021
Syntax error in reorder_defs.ml after running make

#128 · created Oct 03, 2019 by mantis-gitlab-migration confirmed critical frama-clang
- 2
updated Feb 22, 2021
Can't view publications on the wiki

#131 · created Sep 10, 2019 by mantis-gitlab-migration bug website
- 3
updated Feb 22, 2021
Error in frama-clang make file

#141 · created Jul 07, 2019 by mantis-gitlab-migration bug frama-clang
- 1
updated Feb 22, 2021
frama-clang failed to install

#142 · created Jul 04, 2019 by mantis-gitlab-migration bug frama-clang
- 2
updated Feb 22, 2021
configure does not detect gtksourceview due to wrong path

#157 · created Jun 20, 2019 by mantis-gitlab-migration bug compilation
- 3
updated Feb 22, 2021
build failure due to mangled variable assignment in Makefile

#158 · created Jun 20, 2019 by mantis-gitlab-migration bug compilation
- 1
updated Feb 22, 2021
Does not build with OCaml 4.08.0

#160 · created Jun 18, 2019 by mantis-gitlab-migration bug compilation
- 1
updated Feb 22, 2021
frama-c installation needs dune > 1.5 package installed

#164 · created Jun 04, 2019 by mantis-gitlab-migration bug website
- 1
updated Feb 22, 2021
kernel generates UnspecifiedSequence when 2 following ternary operators

#166 · created May 07, 2019 by mantis-gitlab-migration bug kernel
- 0
updated Feb 22, 2021
Failure to detect overflows into an allocated area within a struct

#172 · created Aug 24, 2017 by Kostyantyn Vorobyov bug e-acsl
- 1
updated Feb 22, 2021
Failure to record global variable with initialiser

#174 · created Dec 04, 2015 by Kostyantyn Vorobyov bug e-acsl
- 0
updated Mar 30, 2021
Incorrect handling of \initialized when initialized struct is passed to a function by value

#177 · created Jun 13, 2017 by Kostyantyn Vorobyov bug e-acsl
- 0
updated Feb 22, 2021
Can't use e-acsl on a dynamic library containing all the instrumentations

#179 · created Jan 22, 2019 by mantis-gitlab-migration confirmed critical e-acsl
- 2
updated Feb 22, 2021
missing E-ACSL code, control flow graph, function pointer

#182 · created Dec 11, 2018 by mantis-gitlab-migration bug e-acsl
- 3
updated Mar 30, 2021
missing E-ACSL code when ignoring asm annotation

#183 · created Dec 05, 2018 by mantis-gitlab-migration bug confirmed e-acsl
- 2
updated Mar 30, 2021
Wrong specification for standard library function memmove

#196 · created Feb 17, 2014 by Pascal Cuoq bug kernel
- 0
updated Feb 22, 2021
frama-clang fails to compile

#240 · created Oct 01, 2018 by mantis-gitlab-migration critical frama-clang
- 3
updated Feb 22, 2021
const fields in constructors

#243 · created Aug 24, 2018 by mantis-gitlab-migration bug frama-clang
- 2
updated Feb 22, 2021
Model Variables in Frama C

#249 · created Aug 27, 2018 by mantis-gitlab-migration ACSL enhancement kernel
- 1
updated Feb 22, 2021
Expose ACSL annotations through host language pragmas

#264 · created Mar 08, 2018 by mantis-gitlab-migration ACSL enhancement kernel
- 0
updated Apr 14, 2021
e-acsl-gcc failes on macOS

#266 · created Feb 23, 2018 by Jens Gerlach bug e-acsl
- 8
updated Feb 22, 2021
user-defined type not accepted after builtin type in quantifier chain

#269 · created Feb 12, 2018 by Jochen Burghardt bug frama-clang
- 0
updated Feb 22, 2021
Frama-clang reports overloading ambiguity where Frama-C doesn't

#270 · created Feb 12, 2018 by Jochen Burghardt enhancement frama-clang
- 0
updated Mar 30, 2021
variable declared in "for" init-part unrecognized in loop body assigns clause; 100% verification degree reported nevertheless

#271 · created Feb 12, 2018 by Jochen Burghardt bug frama-clang
- 0
updated Feb 22, 2021
"let" in predicate body unrecognized

#272 · created Feb 12, 2018 by Jochen Burghardt bug frama-clang
- 0
updated Feb 22, 2021
"assigns" in statement contract causes abort or crash

#273 · created Feb 12, 2018 by Jochen Burghardt critical frama-clang
- 0
updated Feb 22, 2021
"Here" as predicate label in statement contract causes Segmentation fault

#274 · created Feb 12, 2018 by Jochen Burghardt critical frama-clang
- 0
updated Feb 22, 2021
Frama-clang complains when reserved keywords are used as property labels, while Frama-C doesn't

#275 · created Feb 12, 2018 by Jochen Burghardt enhancement frama-clang
- 0
updated Feb 22, 2021
insufficient contracts for generated constructors and assignment operator(s)

#276 · created Feb 07, 2018 by Jens Gerlach confirmed enhancement frama-clang
- 2
updated Mar 30, 2021
can't handle lemma with 3 labels

#277 · created Feb 08, 2018 by Jochen Burghardt bug frama-clang
- 2
updated Feb 22, 2021
Alt-Ergo reports about " bool and int cannot be unified"

#280 · created Feb 05, 2018 by Jens Gerlach bug frama-clang
- 1
updated Feb 22, 2021
Frama-Clang crashes on error in contract

#281 · created Jan 31, 2018 by Jens Gerlach critical frama-clang
- 0
updated Feb 22, 2021
warning from kernel about exceptions

#283 · created Jan 31, 2018 by Jens Gerlach confirmed enhancement frama-clang
- 1
updated Feb 22, 2021
unknown variable in contract is not treated as an error

#285 · created Jan 30, 2018 by Jens Gerlach bug frama-clang
- 1
updated Feb 22, 2021
direct initialisation of bool by nullptr

#286 · created Jan 22, 2018 by Jens Gerlach critical frama-clang
- 1
updated Feb 22, 2021
C++11 delegating constructor not supported

#287 · created Jan 19, 2018 by Jens Gerlach bug frama-clang
- 0
updated Feb 22, 2021
range based for loop from C++11 not supported

#288 · created Jan 19, 2018 by Jens Gerlach bug frama-clang
- 0
updated Feb 22, 2021
std::bad_alloc not supported

#289 · created Jan 18, 2018 by Jens Gerlach bug confirmed frama-clang
- 2
updated Feb 22, 2021
How to use the "Callers ..." context menu item

#290 · created May 27, 2013 by mantis-gitlab-migration confirmed enhancement gui
- 2
updated Feb 22, 2021
Option "-lib-entry" results misses possible values of function pointers

#296 · created Nov 07, 2016 by Jochen Burghardt bug eva
- 1
updated Feb 22, 2021
"pointer comparison" warning emitted for "p==NULL"

#298 · created Nov 11, 2016 by Jochen Burghardt bug eva
- 4
updated Feb 22, 2021
Duplicates are created on the tab "Messages"

#318 · created Feb 03, 2017 by mantis-gitlab-migration enhancement gui
- 3
updated Feb 22, 2021
Statement contracts and WP

#327 · created Jul 18, 2017 by Jens Gerlach documentation
- 0
updated Feb 22, 2021
Instrumentation Failure Error in Online Pathcrawler

#329 · created Jul 06, 2017 by mantis-gitlab-migration bug pathcrawler
- 0
updated Feb 22, 2021
suggestions for improvement of Sect.3.6 and 3.7 of the wp manual

#331 · created Jun 15, 2017 by Jochen Burghardt documentation
- 1
updated Feb 22, 2021
poor errors message texts for Hoare memory model checks

#334 · created Jun 15, 2017 by Jochen Burghardt wp
- 0
updated Feb 22, 2021
suggest to check (loop) assigns clauses by data flow analysis

#337 · created Jun 01, 2017 by Jochen Burghardt enhancement wp
- 0
updated Feb 22, 2021
preprocessor fail: unterminated comment

#348 · created May 30, 2017 by mantis-gitlab-migration bug kernel
- 5
updated Feb 22, 2021
Check that all occurrences of *p in assigns are guarded by a \valid(p) in requires

#357 · created Apr 23, 2014 by Jens Gerlach ACSL bug kernel
- 1
updated Feb 22, 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
- 1
updated Feb 22, 2021
problem with Qed's simplification power

#370 · created Feb 06, 2017 by Jochen Burghardt bug wp
- 1
updated Feb 22, 2021
It is impossble to change log file without kinds of message changing.

#372 · created Jan 19, 2017 by mantis-gitlab-migration confirmed enhancement kernel
- 1
updated Feb 22, 2021
WP appears to assume left-to-right evaluation order for int addition

#381 · created Jan 16, 2017 by Jochen Burghardt bug kernel
- 2
updated Feb 22, 2021
structure in logic not supported?

#383 · created Dec 20, 2016 by Jens Gerlach ACSL bug kernel
- 1
updated Feb 22, 2021
label Pre in function contracts

#386 · created Jan 02, 2017 by Jens Gerlach ACSL bug kernel
- 0
updated Feb 22, 2021
wp: the example from Getting Started guide doesn't work (all goals are Unknown)

#389 · created Dec 14, 2016 by mantis-gitlab-migration enhancement parsing
- 13
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
- 0
updated Apr 15, 2021
Path for 'make install-doc-code' for external plug-in

#427 · created Sep 26, 2012 by mantis-gitlab-migration compilation enhancement
- 6
updated Feb 22, 2021
Compilation of kernel native cmx is messed up with plugin makefile

#428 · created Sep 16, 2015 by mantis-gitlab-migration bug compilation
- 1
updated Feb 22, 2021
Namespace through packs - packing frama-c cmx into a cmxa

#429 · created Sep 16, 2015 by mantis-gitlab-migration enhancement kernel
- 2
updated Feb 22, 2021
typo in output of 'frama-c -wp-help'

#482 · created Dec 09, 2015 by Jens Gerlach bug documentation
- 1
updated Feb 22, 2021
Frama-C upgrade installation not foolproof

#510 · created Apr 11, 2016 by Jochen Burghardt compilation
- 7
updated Feb 22, 2021
insertion of "assert true" after a statement influences provability of the statement's contract

#511 · created May 02, 2016 by Jochen Burghardt bug kernel
- 4
updated Feb 22, 2021
Make find(1) command POSIX-compliant

#513 · created Apr 09, 2016 by mantis-gitlab-migration bug wp
- 0
updated Apr 15, 2021
ambiguity with consecutive comparison and ternary expressions

#575 · created Dec 05, 2015 by David Cok ACSL bug kernel
- 1
updated Feb 22, 2021
No syntax to apply lambda expressions

#576 · created Dec 05, 2015 by David Cok ACSL enhancement kernel
- 0
updated Feb 22, 2021
Nested VLA are not supported

#581 · created Mar 25, 2014 by Pascal Cuoq enhancement kernel
- 0
updated Mar 29, 2021
mixed virtual/nonvirtual base class causes error

#588 · created Feb 09, 2015 by Jochen Burghardt confirmed enhancement frama-clang
- 4
updated Feb 22, 2021
ACSL typing fails when performing unification of type variables

#590 · created Sep 24, 2015 by Patrick Baudin ACSL bug kernel
- 0
updated Mar 29, 2021
With struct containing arrays, option -unspecified-access is too strict

#602 · created Aug 21, 2015 by Pascal Cuoq bug kernel
- 0
updated Apr 28, 2021
Control dependencies between labelled instructuctions and the corresponding goto statement

#609 · created Nov 25, 2014 by mantis-gitlab-migration bug pdg
- 1
updated Feb 22, 2021
implicit conversion of terms to predicates

#611 · created Jul 17, 2015 by David Cok ACSL bug kernel
- 0
updated Feb 22, 2021
validity of obligation from statement contract depends on whether the statement is enclosed in block {}

#625 · created Jun 01, 2015 by Jochen Burghardt bug wp
- 2
updated Apr 15, 2021
Weak and Strong Invariants are not supported

#630 · created Jun 12, 2015 by mantis-gitlab-migration ACSL bug kernel
- 0
updated Feb 22, 2021
Redefintion of variables in same scope is allowed in annotations

#634 · created Jun 01, 2015 by mantis-gitlab-migration ACSL bug confirmed kernel
- 1
updated Feb 22, 2021
access to static struct fields unsupported in annotation

#638 · created May 07, 2015 by Jochen Burghardt bug frama-clang
- 0
updated Feb 22, 2021
declarations of static variable of class type in function body causes crash

#640 · created Nov 27, 2014 by Jochen Burghardt confirmed critical frama-clang
- 1
updated Mar 29, 2021
can't prove (trivial) validity of memory access of "p->a"

#642 · created May 04, 2015 by Jochen Burghardt bug frama-clang
- 0
updated Feb 22, 2021