Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 208
    • Issues 208
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues

  • Open 208
  • Closed 1,261
  • All 1,469
New issue
  • Priority Created date Updated date Milestone due date Due date Popularity Label priority Manual Title
  • 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
  • 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 Aug 05, 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • insufficient preconditions given to verify constructor call from global variable initialization
    #643 · created Dec 01, 2014 by Jochen Burghardt   bug confirmed frama-clang
    • 2
    updated Feb 22, 2021
  • loop invariant referring to body-local variable causes crash, when body is enclosed in curly braces "{...}"
    #646 · created Apr 27, 2015 by Jochen Burghardt   critical frama-clang
    • 1
    updated Mar 29, 2021
  • variable declared in loop initializer is unknown in loop body "assert"
    #647 · created Apr 27, 2015 by Jochen Burghardt   bug frama-clang
    • 0
    updated Feb 22, 2021
  • use of body-declared variable in loop annotation causes crash
    #648 · created Nov 27, 2014 by Jochen Burghardt   confirmed critical frama-clang
    • 3
    updated Feb 22, 2021
  • declaration of local variable of class type results in unprovable assigns clause
    #649 · created Apr 27, 2015 by Jochen Burghardt   bug frama-clang
    • 1
    updated Feb 22, 2021
  • template parameter type can't used in typedef
    #650 · created Nov 17, 2014 by Jochen Burghardt   bug confirmed frama-clang
    • 5
    updated Feb 22, 2021
  • CLASSNAME::PREDICATENAME not recognized as predicate (or even as term)
    #660 · created Oct 30, 2014 by Jochen Burghardt   confirmed enhancement frama-clang
    • 3
    updated Feb 22, 2021
  • use of "CLASSNAME::VARIABLENAME" in assigns clase causes abort
    #664 · created Feb 05, 2015 by Jochen Burghardt   bug confirmed frama-clang
    • 1
    updated Feb 22, 2021
  • indexing of string literal apparently causes memory leak in framaCIRGen
    #666 · created Nov 24, 2014 by Jochen Burghardt   confirmed critical frama-clang
    • 3
    updated Feb 22, 2021
  • "=" in contract causes abort rather than syntax error message
    #667 · created Nov 13, 2014 by Jochen Burghardt   confirmed enhancement frama-clang
    • 1
    updated Feb 22, 2021
  • Prev
  • 1
  • 2
  • 3
  • Next