diff --git a/.LICENSE b/.LICENSE index 15ecd250104ca63658b5eeff731daa3872454d5b..812560cbfdbde7e34379b3f7317ef2e4f66e1201 100644 --- a/.LICENSE +++ b/.LICENSE @@ -1,7 +1,7 @@ This file is part of Frama-Clang -Copyright (C) 2012-2021 +Copyright (C) 2012-2022 CEA (Commissariat à l'énergie atomique et aux énergies alternatives) diff --git a/ACSLCodeAnnotation.cpp b/ACSLCodeAnnotation.cpp index c2d576edf14252ec0bc16b670f922cb0ab5d36c8..165a25a41b0b5ebbcb83c5422a070c72a0bd74f9 100644 --- a/ACSLCodeAnnotation.cpp +++ b/ACSLCodeAnnotation.cpp @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/ACSLCodeAnnotation.h b/ACSLCodeAnnotation.h index 2496992f791b92d3622e38b7e6cc7969774977c7..ce4b892d459df6622023626bc955446b21129f00 100644 --- a/ACSLCodeAnnotation.h +++ b/ACSLCodeAnnotation.h @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/ACSLComment.cpp b/ACSLComment.cpp index 91e663a20a3da63a05291c6a0eb733918a5953c9..d38b3486e3b69cd7006e569c3d1480fc7701fd80 100644 --- a/ACSLComment.cpp +++ b/ACSLComment.cpp @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/ACSLComment.h b/ACSLComment.h index 8984fbfe45213f799365488b890351892d0ec81e..a2f7b810dbd3d542df33c57629be8deb12fc9e16 100644 --- a/ACSLComment.h +++ b/ACSLComment.h @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/ACSLComponent.cpp b/ACSLComponent.cpp index 884e1964b664aee90b353559251eba721a854889..8435765a2171dbfd85d98f0269a52aab08c1e54e 100644 --- a/ACSLComponent.cpp +++ b/ACSLComponent.cpp @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/ACSLComponent.h b/ACSLComponent.h index ce4a42e1a0aa0fa70edbf238d4515403ac8e5d3f..0f2f206bbf5522fca8d81fa0eb1e55f67d70c3ab 100644 --- a/ACSLComponent.h +++ b/ACSLComponent.h @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/ACSLFunctionContract.cpp b/ACSLFunctionContract.cpp index 0e287b1169a19803b85e4fecc4e1eb3424273050..d9642e276f8f3b4bae587029b0a0cd6b2f195276 100644 --- a/ACSLFunctionContract.cpp +++ b/ACSLFunctionContract.cpp @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/ACSLFunctionContract.h b/ACSLFunctionContract.h index 0c2554bdce2a06d8b22cd9a2ccf526b2437bafd0..cc599a07de8ecda5b48b3e73a4445d6b4846b89c 100644 --- a/ACSLFunctionContract.h +++ b/ACSLFunctionContract.h @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/ACSLGlobalAnnotation.cpp b/ACSLGlobalAnnotation.cpp index a1cdcf78ce17af99a5661aa7540558665ddcb2ec..07d3e3182fe08922411667c4b5cc2c46c26e9260 100644 --- a/ACSLGlobalAnnotation.cpp +++ b/ACSLGlobalAnnotation.cpp @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/ACSLGlobalAnnotation.h b/ACSLGlobalAnnotation.h index 3ada9db443bad172187cc06de2d5828aa7b58a73..8ce81414e4249c4134add43d0d12551917dcc937 100644 --- a/ACSLGlobalAnnotation.h +++ b/ACSLGlobalAnnotation.h @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/ACSLLexer.cpp b/ACSLLexer.cpp index 25292b18110fa8dab331c14007a9ba99d94a1704..fb429821ea44d8e17be6fbc39eb96b6b9e9df0e3 100644 --- a/ACSLLexer.cpp +++ b/ACSLLexer.cpp @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/ACSLLexer.h b/ACSLLexer.h index ff7118fb9b0dc4b26eb139f5fefcc8dd283437fb..26a9a97c77755e006fd065b55a0836189e9cc5f5 100644 --- a/ACSLLexer.h +++ b/ACSLLexer.h @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/ACSLLogicType.cpp b/ACSLLogicType.cpp index 3a8ef6ab4cef2485838594a726fd882e486af70a..3cbd303737881840f80db624e6f1c5adc9e6ccc7 100644 --- a/ACSLLogicType.cpp +++ b/ACSLLogicType.cpp @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/ACSLLogicType.h b/ACSLLogicType.h index 028680259b05e12ca36d9b8eddceb5e678d7f107..82fa7bb03f47c1b01447e2f34472fee1d2c050f2 100644 --- a/ACSLLogicType.h +++ b/ACSLLogicType.h @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/ACSLLoopAnnotation.cpp b/ACSLLoopAnnotation.cpp index 67bfeb1545c6f14922fca7ed0f078c971d979063..5bca81b5de11c16feb533eb92ed976c9ba377b87 100644 --- a/ACSLLoopAnnotation.cpp +++ b/ACSLLoopAnnotation.cpp @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/ACSLLoopAnnotation.h b/ACSLLoopAnnotation.h index 0aab4dddbbfca7d189568416a9bcbece776e3e45..08f04704a18791cd56655b75993282a3a69908f6 100644 --- a/ACSLLoopAnnotation.h +++ b/ACSLLoopAnnotation.h @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/ACSLParser.cpp b/ACSLParser.cpp index e3b932962a1433f559dda221cba1be2acb3cc2ce..fe7997d407e10476e213289ae3649e81949a7c1b 100644 --- a/ACSLParser.cpp +++ b/ACSLParser.cpp @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/ACSLParser.h b/ACSLParser.h index 8bcb76eabf005d255647f8e1083d89b10bfccbde..a707821f43cd927b30e9bb9d7fcc51759b71cc0d 100644 --- a/ACSLParser.h +++ b/ACSLParser.h @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/ACSLStatementAnnotation.cpp b/ACSLStatementAnnotation.cpp index 8a8f93ec842788b5b42ec5c5731aaf6e16debff5..f826e54d014c2698366d010ff045b70b0cade39f 100644 --- a/ACSLStatementAnnotation.cpp +++ b/ACSLStatementAnnotation.cpp @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/ACSLStatementAnnotation.h b/ACSLStatementAnnotation.h index d7f9e835d39fddeeddf79cb932fea1bc2ef0e249..4e1bd351f1b89744e4f786ab4e86f63d589fb12c 100644 --- a/ACSLStatementAnnotation.h +++ b/ACSLStatementAnnotation.h @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/ACSLTermOrPredicate.cpp b/ACSLTermOrPredicate.cpp index 26622784e9eb8de3c2078f48625f4fbcf77bd029..abdcc5f85ea62e6609ef24d59286606982c8b1d7 100644 --- a/ACSLTermOrPredicate.cpp +++ b/ACSLTermOrPredicate.cpp @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/ACSLTermOrPredicate.h b/ACSLTermOrPredicate.h index 006b63f48dc91372340bc328b5487eb3d0178e14..7efc9ca5b283aa8e2b7c1d3522db1b2561601bf3 100644 --- a/ACSLTermOrPredicate.h +++ b/ACSLTermOrPredicate.h @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/ACSLToken.cpp b/ACSLToken.cpp index 649d4b9572d34049eef196536dd376054e5ed144..3625f64646c92edd9e96600667e3b49c2410b077 100644 --- a/ACSLToken.cpp +++ b/ACSLToken.cpp @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/ACSLToken.h b/ACSLToken.h index 9f8288905f99dfb65a83718acb72f3fb7ed9d7e2..f77177eed001c138d15f32dc1e9339dc59b8c5f9 100644 --- a/ACSLToken.h +++ b/ACSLToken.h @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/AnnotationComment.h b/AnnotationComment.h index 92b9e82648312af4efb422172efcf0693b0ff144..1c3e5fe088478e1d9e3f9e2fba0aba370cce3bd2 100644 --- a/AnnotationComment.h +++ b/AnnotationComment.h @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/ClangVisitor.cpp b/ClangVisitor.cpp index 452446f60db4b4be7c6c6958ecfc2d581399494f..67b951103b2714484474256d925272de376301c7 100644 --- a/ClangVisitor.cpp +++ b/ClangVisitor.cpp @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/ClangVisitor.h b/ClangVisitor.h index f5d5ce9267f2e65c1e34bfe72800e30ebad9bf63..663c37aaab6bbdae723b300f30206fac79cae9af 100644 --- a/ClangVisitor.h +++ b/ClangVisitor.h @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/Clang_utils.cpp b/Clang_utils.cpp index e7228964a582abd41787771605df4d9b3d46ddc4..373d636715d6c65feee627d2903648ae8efaba9d 100644 --- a/Clang_utils.cpp +++ b/Clang_utils.cpp @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/Clang_utils.h b/Clang_utils.h index d504ab88b51a88977953c40c3debe347d1ed56bc..e8a4003c1f94088b6c2c99f723f568b8a798cdfb 100644 --- a/Clang_utils.h +++ b/Clang_utils.h @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/DescentParse.cpp b/DescentParse.cpp index 52414571b00cf04d9c9599f3ad9e6591ab415703..a80ed56fb8870ca122c1c769fc7c4a349ce72c6b 100644 --- a/DescentParse.cpp +++ b/DescentParse.cpp @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/DescentParse.h b/DescentParse.h index 819e759ba0d1a1214b28310fa205a484f2308329..d14aedf511f34a0264528d5ba1c376921651ca09 100644 --- a/DescentParse.h +++ b/DescentParse.h @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/DescentParse.template b/DescentParse.template index c08b3ee31fd26514215cf24127343bc959773b8b..e4e896d7624cafce82f92c7a54420bb1513c1889 100644 --- a/DescentParse.template +++ b/DescentParse.template @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/Doxyfile b/Doxyfile index 8ee2b92d47d0f8bd5ee4253455ddf44b662e515a..8aa565f963f89a0f83bbfd2f89845d8d891c8216 100644 --- a/Doxyfile +++ b/Doxyfile @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/FramaCIRGen.cpp b/FramaCIRGen.cpp index 9585a3a6c4a536b58b8753642c8f1bb0d9226fe1..016176d37e289d2612037130b431968500aeac8a 100644 --- a/FramaCIRGen.cpp +++ b/FramaCIRGen.cpp @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/Frama_Clang.mli b/Frama_Clang.mli index 61986f6f53b3917269191cb8cb486565057259a3..86b10a9a91bc4da998da799639dd9cfd83e5507c 100644 --- a/Frama_Clang.mli +++ b/Frama_Clang.mli @@ -2,7 +2,7 @@ (* *) (* This file is part of Frama-Clang *) (* *) -(* Copyright (C) 2012-2021 *) +(* Copyright (C) 2012-2022 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/Makefile b/Makefile index 6ec6c416a388dd88f422f7c94709edaa780c9f7a..3fe37e5737646c3dc9a5ba31389024d8e363b6ae 100644 --- a/Makefile +++ b/Makefile @@ -2,7 +2,7 @@ # # # This file is part of Frama-Clang # # # -# Copyright (C) 2012-2021 # +# Copyright (C) 2012-2022 # # CEA (Commissariat à l'énergie atomique et aux énergies # # alternatives) # # # diff --git a/Makefile.clang b/Makefile.clang index 3733640ddec5a7dae77f45630bfb55e7c5cf91df..4b13b6fb71b4d674ace93502e4ddcca3b0df4c8e 100644 --- a/Makefile.clang +++ b/Makefile.clang @@ -2,7 +2,7 @@ # # # This file is part of Frama-Clang # # # -# Copyright (C) 2012-2021 # +# Copyright (C) 2012-2022 # # CEA (Commissariat à l'énergie atomique et aux énergies # # alternatives) # # # diff --git a/Makefile.common b/Makefile.common index 1b97c34a76652484a254988fbc9658378fa7dd36..cfc5918c4d528e1f836bcd3bbea9d9ffd377d9e9 100644 --- a/Makefile.common +++ b/Makefile.common @@ -2,7 +2,7 @@ # # # This file is part of Frama-Clang # # # -# Copyright (C) 2012-2021 # +# Copyright (C) 2012-2022 # # CEA (Commissariat à l'énergie atomique et aux énergies # # alternatives) # # # diff --git a/Makefile.config.in b/Makefile.config.in index 800f19ae6b1137a3da7a2ea2891dcf0d46b8f23b..61126b970364f7c5c0b0184e24172626162f8b56 100644 --- a/Makefile.config.in +++ b/Makefile.config.in @@ -2,7 +2,7 @@ # # # This file is part of Frama-Clang # # # -# Copyright (C) 2012-2021 # +# Copyright (C) 2012-2022 # # CEA (Commissariat à l'énergie atomique et aux énergies # # alternatives) # # # diff --git a/README.md b/README.md index 53794961fa9d4ede64594172765eacb9a6aa5c5b..69a21e41302bef42a1c3576e17c3c306ab002783 100644 --- a/README.md +++ b/README.md @@ -40,16 +40,16 @@ with `.cpp`, `.C`, `.cxx`, `.c++` or `.cc` will be treated as C++ files. Files ending with `.ii` will be considered as already pre-processed C++ files. Options of the plug-in are the following. -- `-cxx-demangling-full` tells Frama-C to display C++ global - identifiers with their fully-qualified name (e.g. `::A::x`) -- `-cxx-demangling-short` tells Frama-C to display global - C++ identifiers with their unqualified name (e.g. `x`) -- `-cxx-keep-mangling` tells Frama-C to display global C++ - identifiers with the name they have in the C translation (e.g. - `_Z1A1x`, that allows to distinguish between overloaded symbols. - This mangled name is computed from the fully-qualified C++ name - according to the rules described in the Itanium C++ ABI. Pretty-printing - the AST with this option should result in compilable C code. +- `-cxx-unmangling key` indicates what to do when outputting a C++ symbol name. + `key` can be one the following: + - `help`: outputs a list of existing `key` with a short description + - `fully-qualified`: displays the fully qualified name (e.g. `::A::x`) + - `without-qualifier`: only display the unqualified name (e.g. `x`) + - `none`: do not any transformation, displays the name as it is stored + in Frama-C's AST (e.g. `_Z1A1x`) +- `-cxx-parseable-output` indicates that the pretty-printed code resulting + from the translation should be able to be parsed again by Frama-C. + implies `-cxx-unmangling none` - `-cxx-cstdlib-path <path>` specifies where to look for standard C library headers (default is the path to Frama-C's headers) - `-cxx-c++stdlib-path <path>` specifies where to look for @@ -62,6 +62,12 @@ Options of the plug-in are the following. This should only be needed if the front-end as a whole has not been installed properly. +Older versions of the plug-in used specific options for unmangling. +These are now obsolete: +- `-cxx-demangling-full`: use `-cxx-unmangling fully-qualified` +- `-cxx-demangling-short`: use `-cxx-unmangling without-qualifier` +- `-cxx-keep-mangling`: use `-cxx-unmangling none` + In addition, any command-line option taking a function name as argument (e.g. `-main`, `-eva-slevel-function`, ...) will accept a fully qualified C++ name (provided it refers to an existing function diff --git a/RTTITable.cpp b/RTTITable.cpp index c00c8dd0b8fd504e8fa324c1d4664a0812246eea..4cb729a7267e007e2766989485231622529494b5 100644 --- a/RTTITable.cpp +++ b/RTTITable.cpp @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/RTTITable.h b/RTTITable.h index 5ec7171797a0d6d7edf37e1c01713078df5b6a12..9d507067585edee865182b875563551190513d78 100644 --- a/RTTITable.h +++ b/RTTITable.h @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/VisitTable.cpp b/VisitTable.cpp index 3c0cde1dd93dc1bbb186dde56d3cba20f6c6a7dc..45c84ffbf23d5e3772865e77ec28bd2f6899300e 100644 --- a/VisitTable.cpp +++ b/VisitTable.cpp @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/VisitTable.h b/VisitTable.h index f3b339e4bfdbadade77287fa35ffacdd10db1957..362d66bc0cd238b319eeb573dfa1c250179009d0 100644 --- a/VisitTable.h +++ b/VisitTable.h @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/class.ml b/class.ml index d263805270df3984a4b57418acf0dc689d4fcbe7..dd635659ec54df728bba26f95c18879946aa2959 100644 --- a/class.ml +++ b/class.ml @@ -2,7 +2,7 @@ (* *) (* This file is part of Frama-Clang *) (* *) -(* Copyright (C) 2012-2021 *) +(* Copyright (C) 2012-2022 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/class.mli b/class.mli index 9fff34005ead911b5684e9843541a62768849581..231047ef49f11d64552721ac3445e0d9baa55ea6 100644 --- a/class.mli +++ b/class.mli @@ -2,7 +2,7 @@ (* *) (* This file is part of Frama-Clang *) (* *) -(* Copyright (C) 2012-2021 *) +(* Copyright (C) 2012-2022 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/configure.ac b/configure.ac index d9dccf69d7e10fbac1cddf94820e6ba841524bdb..b030149c85685ed9fa3f3b8590d31e171e452426 100644 --- a/configure.ac +++ b/configure.ac @@ -2,7 +2,7 @@ # # # This file is part of Frama-Clang # # # -# Copyright (C) 2012-2021 # +# Copyright (C) 2012-2022 # # CEA (Commissariat à l'énergie atomique et aux énergies # # alternatives) # # # diff --git a/convert.ml b/convert.ml index acbd3ea21dbf26f90557aa565a27768a34a3ed97..57374686848f0cf0c66882b25e9644f6ac22b8ee 100644 --- a/convert.ml +++ b/convert.ml @@ -2,7 +2,7 @@ (* *) (* This file is part of Frama-Clang *) (* *) -(* Copyright (C) 2012-2021 *) +(* Copyright (C) 2012-2022 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/convert.mli b/convert.mli index 13b759b5115e6a75cc25b9d067d0d474457001dc..089910de5228be82d5e6bc91da1b18992dc9b4bb 100644 --- a/convert.mli +++ b/convert.mli @@ -2,7 +2,7 @@ (* *) (* This file is part of Frama-Clang *) (* *) -(* Copyright (C) 2012-2021 *) +(* Copyright (C) 2012-2022 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/convert_acsl.ml b/convert_acsl.ml index de3b79cba13d08b6111348bc876bce27145bb38a..326398c63b81774bc80197005df562596f34da69 100644 --- a/convert_acsl.ml +++ b/convert_acsl.ml @@ -2,7 +2,7 @@ (* *) (* This file is part of Frama-Clang *) (* *) -(* Copyright (C) 2012-2021 *) +(* Copyright (C) 2012-2022 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/convert_acsl.mli b/convert_acsl.mli index 07525db712ebc26dd4aefff7b16b310f7a5e7d59..624ee0b69a5b06e1bf5f030f49fcffc0bfe8531e 100644 --- a/convert_acsl.mli +++ b/convert_acsl.mli @@ -2,7 +2,7 @@ (* *) (* This file is part of Frama-Clang *) (* *) -(* Copyright (C) 2012-2021 *) +(* Copyright (C) 2012-2022 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/convert_env.ml b/convert_env.ml index 149e795b37dc74bfeae06c78cfdeae629e1dde1e..7ae537b801cdf72f93e392ffe61868ea3ed54c65 100644 --- a/convert_env.ml +++ b/convert_env.ml @@ -2,7 +2,7 @@ (* *) (* This file is part of Frama-Clang *) (* *) -(* Copyright (C) 2012-2021 *) +(* Copyright (C) 2012-2022 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/convert_env.mli b/convert_env.mli index df17b3066b2497a5ef7798c0fa08f53eb23c4c65..5058797f41109888d753a814f7629e2de1a6d258 100644 --- a/convert_env.mli +++ b/convert_env.mli @@ -2,7 +2,7 @@ (* *) (* This file is part of Frama-Clang *) (* *) -(* Copyright (C) 2012-2021 *) +(* Copyright (C) 2012-2022 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/convert_link.ml b/convert_link.ml index d2a7df72032bc50c82bfb5afe01c4e142c104f99..899362abb938973da6e29d9e1f990cb1f905bd42 100644 --- a/convert_link.ml +++ b/convert_link.ml @@ -2,7 +2,7 @@ (* *) (* This file is part of Frama-Clang *) (* *) -(* Copyright (C) 2012-2021 *) +(* Copyright (C) 2012-2022 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/convert_link.mli b/convert_link.mli index 069216495ebae2eb49a74388777319f5519d1c29..bd93055199c18ee5faf4fe196287abe91f3a4c80 100644 --- a/convert_link.mli +++ b/convert_link.mli @@ -2,7 +2,7 @@ (* *) (* This file is part of Frama-Clang *) (* *) -(* Copyright (C) 2012-2021 *) +(* Copyright (C) 2012-2022 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/cxx_utils.ml b/cxx_utils.ml index 0d68b00e7111a96b9796bb890457f153e118e680..df4ec5ed807201645a24850a42a4f7bd78627063 100644 --- a/cxx_utils.ml +++ b/cxx_utils.ml @@ -2,7 +2,7 @@ (* *) (* This file is part of Frama-Clang *) (* *) -(* Copyright (C) 2012-2021 *) +(* Copyright (C) 2012-2022 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/cxx_utils.mli b/cxx_utils.mli index c511be531f3843d99ab5935ef6f62941e99febfe..3ba006eae03c5c7d9367a43c0f5b30f9519bc11a 100644 --- a/cxx_utils.mli +++ b/cxx_utils.mli @@ -2,7 +2,7 @@ (* *) (* This file is part of Frama-Clang *) (* *) -(* Copyright (C) 2012-2021 *) +(* Copyright (C) 2012-2022 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/doc/userman/fclangversion.tex b/doc/userman/fclangversion.tex index ed36f53328fa6099840e10c46daa49d8db85a6d1..7d68dd54cf8a62851ce5edafa1e2ab86b2055c62 100644 --- a/doc/userman/fclangversion.tex +++ b/doc/userman/fclangversion.tex @@ -1,4 +1,4 @@ -\newcommand{\version}{0.0.10\xspace} -\newcommand{\fclangversion}{0.0.10\xspace} -\newcommand{\fcversion}{22.x~Titanium\xspace} -\newcommand{\clangversion}{6.0-11.0\xspace} +\newcommand{\version}{0.0.11+dev\xspace} +\newcommand{\fclangversion}{0.0.11+dev\xspace} +\newcommand{\fcversion}{24.0~Chromium\xspace} +\newcommand{\clangversion}{9.0-13.0\xspace} diff --git a/doc/userman/frama-c-book.cls b/doc/userman/frama-c-book.cls index f82a033e742632216258e8f6a8c37c23c8297825..e2d476f9ae44f43b4c17f7d5099d33bb1fd0be9e 100644 --- a/doc/userman/frama-c-book.cls +++ b/doc/userman/frama-c-book.cls @@ -3,28 +3,52 @@ % -------------------------------------------------------------------------- \NeedsTeXFormat{LaTeX2e} \ProvidesPackage{frama-c-book}[2009/02/05 LaTeX Class for Frama-C Books] +\newif\ifusecc +\usecctrue % -------------------------------------------------------------------------- % --- Base Class management --- % -------------------------------------------------------------------------- -\LoadClass[a4paper,11pt,twoside,openright]{report} -\DeclareOption{web}{\PassOptionsToPackage{colorlinks,urlcolor=blue}{hyperref}} -\DeclareOption{paper}{\PassOptionsToPackage{pdfborder=0 0 0}{hyperref}} -\ProcessOptions -\RequirePackage{fullpage} -\RequirePackage{hevea} +\makeatletter +\RequirePackage{kvoptions} +\SetupKeyvalOptions{ +family=framacbook, +prefix=framacbook@, +} \RequirePackage{ifthen} +\DeclareVoidOption{web}{\PassOptionsToPackage{colorlinks,urlcolor=blue}{hyperref}} +\DeclareVoidOption{paper}{\PassOptionsToPackage{pdfborder=0 0 0}{hyperref}} +\DeclareStringOption[{type=CC,version=4.0,modifier=by-sa}]{license} +\DeclareStringOption[english]{lang} +\DeclareDefaultOption{\PassOptionsToClass{\CurrentOption}{report}} +\PassOptionsToClass{a4paper,11pt,twoside,openright}{report} + +\ProcessKeyvalOptions* + +\LoadClass{report} + +\PassOptionsToPackage{\framacbook@lang}{babel} + +\ifthenelse{\equal{\framacbook@license}{no}}{\useccfalse}{} +\ifusecc + \PassOptionsToPackage{\framacbook@license}{doclicense} +\fi +\RequirePackage{babel} +\RequirePackage{fullpage} +\RequirePackage{lmodern} \RequirePackage[T1]{fontenc} \RequirePackage[utf8]{inputenc} -\RequirePackage[a4paper,pdftex,pdfstartview=FitH]{hyperref} \RequirePackage{amssymb} -\RequirePackage{xcolor} +\RequirePackage[table]{xcolor} \RequirePackage[pdftex]{graphicx} +\RequirePackage{ifthen} \RequirePackage{xspace} \RequirePackage{makeidx} \RequirePackage[leftbars]{changebar} -\RequirePackage[english]{babel} \RequirePackage{fancyhdr} \RequirePackage{titlesec} +\RequirePackage{upquote} +\RequirePackage[pdftex,pdfstartview=FitH]{hyperref} +\ifusecc\RequirePackage{doclicense}\else\fi % -------------------------------------------------------------------------- % --- Page Layout --- % -------------------------------------------------------------------------- @@ -101,14 +125,49 @@ {#1} \medskip +\ifusecc\doclicenseThis\else\fi +} + +% \acknowledge{<flag image file>}{<text inside box>} +\newcommand{\acknowledge}[2]{ + \fbox{ + \begin{minipage}{0.97\textwidth} + \begin{minipage}{1.2cm} + \includegraphics[width=\linewidth]{#1} + \end{minipage} + \begin{minipage}{0.90\textwidth} + This project has received funding from #2. + \end{minipage} + \end{minipage} + } } + +\newcommand{\acknowledgeANR}{ + \acknowledge{anr-logo.png}{the French ANR projects + CAT~(ANR-05-RNTL-00301) and U3CAT~(08-SEGI-021-01) + } +} + +\newcommand{\acknowledgeEU}{ + \acknowledge{eu-flag.jpg}{the + European Union's Seventh Framework Programme (FP7/2007-2013) + under grant agreement N$^\circ$\,317753 (\mbox{STANCE}).\\ + It has also received funding from the Horizon 2020 research + and innovation programme, under grant agreements + N$^\circ$\,731453~(\mbox{VESSEDIA}), + N$^\circ$\,824231~(\mbox{DECODER}), + N$^\circ$\,830892~(\mbox{SPARTA}), + and N$^\circ$\,883242~(\mbox{ENSURESEC}) + } +} + % -------------------------------------------------------------------------- % --- Sectionning --- % -------------------------------------------------------------------------- \titleformat{\chapter}[display]{\Huge\raggedleft}% {\huge\chaptertitlename\,\thechapter}{0.5em}{} \titleformat{\section}[hang]{\Large\bfseries}{\thesection}{1em}{}% -[\vspace{-14pt}\rule{\textwidth}{0.1pt}\vspace{-8pt}] +[\vspace{-14pt}\rule{\textwidth}{0.1pt}\nopagebreak\vspace{-8pt}] \titleformat{\subsubsection}[hang]{\bfseries}{}{}{}% [\vspace{-8pt}] @@ -146,7 +205,7 @@ \definecolor{lstspecial}{rgb}{0.2,0.6,0.0} \definecolor{lstfile}{gray}{0.85} \newcommand{\lstbrk}{\mbox{$\color{blue}\scriptstyle\cdots$}} -\def\lp@basic{\ifmmode\normalfont\mathtt\mdseries\scriptsize\else\normalfont\ttfamily\mdseries\scriptsize\fi} +\def\lp@basic{\ifmmode\normalfont\mathtt\mdseries\small\else\normalfont\ttfamily\mdseries\small\fi} \def\lp@inline{\ifmmode\normalfont\mathtt\scriptstyle\else\normalfont\ttfamily\mdseries\small\fi} \def\lp@keyword{} \def\lp@special{\color{lstfg}} @@ -154,6 +213,7 @@ \def\lp@string{\color{lstfg}} \def\lp@ident{} \def\lp@number{\rmfamily\tiny\color{lstnum}} \lstdefinestyle{frama-c-style}{% + columns=flexible,% basicstyle=\lp@inline,% identifierstyle=\lp@ident,% commentstyle=\lp@comment,% @@ -204,8 +264,16 @@ % --- Verbatim Stuff ------------------------------------------------------- \lstdefinelanguage{Shell}[]{csh}% -{identifierstyle=\lp@basic,mathescape=false,backgroundcolor=,literate={\\\$}{\$}1} -\lstnewenvironment{shell}[1][]{\lstset{language=Shell,basicstyle=\lp@basic,#1}}{} +{escapechar=@ + identifierstyle=\lp@basic, + mathescape=false, + backgroundcolor=, + literate={\\\$}{\$}1 +} + +\lstnewenvironment{shell}[1][] +{\lstset{language=Shell,basicstyle=\lp@basic,#1}} +{} % ---- Stdout Stuff -------------------------------------------------------- \lstdefinelanguage{Logs}[]{csh}% @@ -242,7 +310,9 @@ keywordstyle=[3]\sffamily\bfseries,% identifierstyle=\ttfamily,% stringstyle=\ttfamily\color{lstfg},% commentstyle=\rmfamily\bfseries\color{lsttxt},% -literate={\\\$}{\$}1,% +literate={\\\$}{\$}1% +{€}{\textbackslash}1% +,% } % --- Configure ------------------------------------------------------------ \lstdefinelanguage{Configure}[]{csh}{% @@ -277,20 +347,21 @@ morekeywords=[2]{failwith,raise,when},% morekeywords=[3]{module,struct,sig,begin,end},% literate=% {~}{${\scriptstyle\thicksim}$}1% -{<}{$<$}1% -{>}{$>$}1% -{->}{$\rightarrow$}1% -{<-}{$\leftarrow$}1% -{:=}{$\leftarrow$}1% -{<=}{$\leq$}1% -{>=}{$\geq$}1% -{==}{$\equiv$}1% -{!=}{$\not\equiv$}1% -{<>}{$\neq$}1% -{'a}{$\alpha$}1% -{'b}{$\beta$}1% -{'c}{$\gamma$}1% -{µ}{`{}}1% +{<}{$<$ }1% +{>}{$>$ }1% +{->}{$\rightarrow$ }1% +{<-}{$\leftarrow$ }1% +{:=}{$\leftarrow$ }1% +{<=}{$\leq$ }1% +{>=}{$\geq$ }1% +{==}{$\equiv$ }1% +{!=}{$\not\equiv$ }1% +{<>}{$\neq$ }1% +{'a}{$\alpha$ }1% +{'b}{$\beta$ }1% +{'c}{$\gamma$ }1% +{µ}{`{}}1% +{€}{\textbackslash}1% } \lstdefinestyle{ocaml-basic}% @@ -326,7 +397,7 @@ basicstyle=\lp@inline,% {\lstinputlisting[style=why-style,basicstyle=\lp@basic]{#1}} \newcommand{\whyinline}[1]% {\lstinline[style=why-style]{#1}} - +\makeatother % -------------------------------------------------------------------------- % --- End. --- % -------------------------------------------------------------------------- diff --git a/doc/userman/main.tex b/doc/userman/main.tex index a1831078a61fe244e856cc79ef5d1bec1f6fcc68..61f49a25a9b392d18c12afd913d244dcf243bedd 100644 --- a/doc/userman/main.tex +++ b/doc/userman/main.tex @@ -1,14 +1,11 @@ -\documentclass[web]{frama-c-book} +\documentclass{frama-c-book} \usepackage{graphicx} \usepackage{calc} \usepackage{datetime} \newdateformat{ddMyyyydate}{\THEDAY~\monthname[\THEMONTH]~\THEYEAR} - - -\include{macros} -\include{fclangversion} - +\input{macros.tex} +\input{fclangversion.tex} \makeindex diff --git a/fclang_datatype.ml b/fclang_datatype.ml index 5670b617e17c2472af4cbc465276bfcc7b6da518..ed48a2269d0a60b49aa8f0c9338ace256d86d547 100644 --- a/fclang_datatype.ml +++ b/fclang_datatype.ml @@ -2,7 +2,7 @@ (* *) (* This file is part of Frama-Clang *) (* *) -(* Copyright (C) 2012-2021 *) +(* Copyright (C) 2012-2022 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/fclang_datatype.mli b/fclang_datatype.mli index 6378c1c10eccdf380b8bd7e0c76ec85117f8ef64..2485f3248f80c61e19e13dfdf27aca6b69df1421 100644 --- a/fclang_datatype.mli +++ b/fclang_datatype.mli @@ -2,7 +2,7 @@ (* *) (* This file is part of Frama-Clang *) (* *) -(* Copyright (C) 2012-2021 *) +(* Copyright (C) 2012-2022 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/frama_Clang_option.ml b/frama_Clang_option.ml index 12405a98dab3c5b2e94d6037e0d1fca7de1113f3..b709171723e04921bad9283bec597fad04c75bbf 100644 --- a/frama_Clang_option.ml +++ b/frama_Clang_option.ml @@ -2,7 +2,7 @@ (* *) (* This file is part of Frama-Clang *) (* *) -(* Copyright (C) 2012-2021 *) +(* Copyright (C) 2012-2022 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) @@ -42,46 +42,69 @@ module Clang_command = let () = Parameter_customize.no_category () module Clang_extra_args = String_list( - struct - let option_name = "-fclang-cpp-extra-args" - let help = - "pass additional options to clang. If not set, the content of \ - -cpp-extra-args (if any) is used instead" - let arg_name = "opt" - end) - -module Unmangling: -sig - val set: string -> unit - val get: unit -> string - val clear: unit -> unit - val get_val: unit -> (string -> string) - val register_mangling_func: string -> (string->string) -> unit -end -= struct - module Rep = - State_builder.Ref(Datatype.String) - (struct let dependencies = [] - let name = "Unmangling" - let default () = "short" - end) - let available_opt = Hashtbl.create 7 - let set s = if Hashtbl.mem available_opt s then Rep.set s - let clear () = Rep.clear () - let get () = Rep.get () - let get_val () = Hashtbl.find available_opt (Rep.get ()) - let register_mangling_func s f = Hashtbl.add available_opt s f - let () = - register_mangling_func "id" (fun s -> s); - set "short" + let option_name = "-fclang-cpp-extra-args" + let help = + "pass additional options to clang. If not set, the content of \ + -cpp-extra-args (if any) is used instead" + let arg_name = "opt" + end) + +let unmangling_functions: (string*(string->string)) Datatype.String.Hashtbl.t = + Datatype.String.Hashtbl.create 7 + +let pp_unmangling_functions fmt = + Datatype.String.Hashtbl.iter + (fun key (help, _) -> Format.fprintf fmt "%s: %s@\n" key help) + unmangling_functions + +let () = + Datatype.String.Hashtbl.add + unmangling_functions "none" ("keep mangled names", Fun.id) + +module Unmangling = + String( + struct + let option_name = "-cxx-unmangling" + let help = + "how to pretty-print mangled symbols. Use `-cxx-unmangling help' to list \ + available options" + let arg_name = "s" + let default = "none" end +) + +let unmangling_help () = + feedback "Possible unmangling functions are:@\n%t" pp_unmangling_functions; + Cmdline.nop + +let unmangling_hook _ v = + if Datatype.String.equal v "help" then + Cmdline.run_after_exiting_stage unmangling_help + +let () = Unmangling.add_set_hook unmangling_hook + +let () = Unmangling.set_possible_values [ "none"; "help" ] +let add_unmangling_function key descr f = + let l = Unmangling.get_possible_values () in + Unmangling.set_possible_values (key :: l); + Datatype.String.Hashtbl.add unmangling_functions key (descr,f) + +let get_unmangling_function () = + let v = Unmangling.get () in + if v <> "help" then + snd (Datatype.String.Hashtbl.find unmangling_functions v) + else + fatal + "cannot get current unmangling function: \ + Frama-C is not supposed to run analyses if `-cxx-unmangling help' is set " module UnmanglingFull = Bool(struct let default = false let option_name = "-cxx-demangling-full" - let help= "displays identifiers with their full C++ name" + let help= "displays identifiers with their full C++ name. \ + DEPRECATED: use -cxx-unmangling fully-qualified instead)" end) let () = Parameter_customize.set_negative_option_name "" @@ -92,7 +115,8 @@ module UnmanglingShort = let option_name = "-cxx-demangling-short" let help= "displays identifiers with their C++ short name \ - (without qualifiers)" + (without qualifiers). \ + DEPRECATED: use -cxx-unmangling without-qualifier instead" end) let () = Parameter_customize.set_negative_option_name "" @@ -101,17 +125,33 @@ module UnmanglingNo = Bool(struct let default = false let option_name= "-cxx-keep-mangling" - let help= "displays identifiers with their mangled name" + let help= "displays identifiers with their mangled name \ + DEPRECATED: use -cxx-unmangling none instead" end) let add_unmangling_option s _ new_flag = if new_flag then Unmangling.set s - else if Unmangling.get () = s then Unmangling.clear () let () = - UnmanglingFull.add_set_hook (add_unmangling_option "full"); - UnmanglingShort.add_set_hook (add_unmangling_option "short"); - UnmanglingNo.add_set_hook (add_unmangling_option "id"); + UnmanglingFull.add_set_hook (add_unmangling_option "fully-qualified"); + UnmanglingShort.add_set_hook (add_unmangling_option "without-qualifier"); + UnmanglingNo.add_set_hook (add_unmangling_option "none") + +module ParseableOutput = + False(struct + let option_name = "-cxx-parseable-output" + let help = "set up Frama-C pretty-printer to output C code that can be reparsed by Frama-C" + end) + +let parseable_output_hook _ f = + let k = Kernel.dkey_print_attrs in + if f then begin + Kernel.add_debug_keys k; + Unmangling.set "none" + end + else Kernel.del_debug_keys k + +let () = ParseableOutput.add_set_hook parseable_output_hook module C_std_headers = String( diff --git a/frama_Clang_option.mli b/frama_Clang_option.mli index 387872fcab408e822792adc7f348f64dc087b2c2..91e3d5a42d0cee7f99fc06be3fa552b3b8b7b527 100644 --- a/frama_Clang_option.mli +++ b/frama_Clang_option.mli @@ -2,7 +2,7 @@ (* *) (* This file is part of Frama-Clang *) (* *) -(* Copyright (C) 2012-2021 *) +(* Copyright (C) 2012-2022 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) @@ -27,13 +27,21 @@ module Clang_command: Parameter_sig.String module Clang_extra_args: Parameter_sig.String_list -(** state of the demangling options. *) -module Unmangling: -sig - val set: string -> unit - val get_val: unit -> (string -> string) - val register_mangling_func: string -> (string->string) -> unit -end +(** state of the -cxx-unmangling option. *) +module Unmangling: Parameter_sig.String + +(** [add_unmangling_function key descr f] registers [f] as an unmangling + function, activated by [-cxx-unmangling key]. [descr] will be displayed + along with [key] in the [-cxx-unmangling help] output. + *) +val add_unmangling_function: string -> string -> (string -> string) -> unit + +(** gets the unmangling function corresponding + to the current value of [Unmangling] *) +val get_unmangling_function: unit -> (string -> string) + +(** -cxx-parseable-output *) +module ParseableOutput: Parameter_sig.Bool (** -cxx-cstdlib-path option *) module C_std_headers: Parameter_sig.String diff --git a/frama_Clang_register.ml b/frama_Clang_register.ml index fc85953c3fd5c0d430b1774e68e1b5da9d61cc29..3348df276a248ad03e9fdc267a0ab373a07a710a 100644 --- a/frama_Clang_register.ml +++ b/frama_Clang_register.ml @@ -2,7 +2,7 @@ (* *) (* This file is part of Frama-Clang *) (* *) -(* Copyright (C) 2012-2021 *) +(* Copyright (C) 2012-2022 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) @@ -121,21 +121,36 @@ struct class printer = object inherit M.printer method! varname fmt name = - Format.pp_print_string fmt (Frama_Clang_option.Unmangling.get_val() name) + Format.pp_print_string fmt + (Frama_Clang_option.get_unmangling_function () name) end end (* we avoid any side effect on the kernel unless we are parsing explicitly a C++ file. *) +let is_cxx_printer_initialized = ref false + +let init_cxx_printer _ v = + if v <> "help" && not !is_cxx_printer_initialized then + begin + is_cxx_printer_initialized := true; + Cil_printer.register_shallow_attribute Convert.fc_implicit_attr; + Cil_printer.register_shallow_attribute Convert.fc_pure_template_decl_attr; + Printer.update_printer (module Cxx_printer); + end + +let () = + Frama_Clang_option.Unmangling.add_set_hook init_cxx_printer + let is_initialized = ref false let init_cxx_normalization () = if not !is_initialized then begin is_initialized:=true; - Cil_printer.register_shallow_attribute Convert.fc_implicit_attr; - Cil_printer.register_shallow_attribute Convert.fc_pure_template_decl_attr; - Printer.update_printer (module Cxx_printer); + (* If unmangling has not been set, default to short. *) + if not (Frama_Clang_option.Unmangling.is_set ()) then + Frama_Clang_option.Unmangling.set "without-qualifier"; (* enable exception removal unless it has explicitely been set to false on the command line. *) @@ -146,7 +161,7 @@ let init_cxx_normalization () = (* C++ allows this *) Cil.set_acceptEmptyCompinfo () end - + let parse_cxx file = init_cxx_normalization (); Frama_Clang_option.feedback diff --git a/frama_Clang_register.mli b/frama_Clang_register.mli index 1a1bf4e3c8aed2fe39c83c2a029c53a808d4a163..4b6640cdd44487e1ebe4a327bb50cdd864445b09 100644 --- a/frama_Clang_register.mli +++ b/frama_Clang_register.mli @@ -2,7 +2,7 @@ (* *) (* This file is part of Frama-Clang *) (* *) -(* Copyright (C) 2012-2021 *) +(* Copyright (C) 2012-2022 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/gen_ast.ml b/gen_ast.ml index e0a905edab09b7da727f5635c1e351a29d93ce95..d52429f6a2d9831c1a145453346277dec6367736 100644 --- a/gen_ast.ml +++ b/gen_ast.ml @@ -2,7 +2,7 @@ (* *) (* This file is part of Frama-Clang *) (* *) -(* Copyright (C) 2012-2021 *) +(* Copyright (C) 2012-2022 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/generate_spec.ml b/generate_spec.ml index 56bb8f1eeb9cbadb7e9ca5dba9bbe31ce9a1af2d..123b53448a3fe839951c2e96c0804bf1a265df0c 100644 --- a/generate_spec.ml +++ b/generate_spec.ml @@ -2,7 +2,7 @@ (* *) (* This file is part of Frama-Clang *) (* *) -(* Copyright (C) 2012-2021 *) +(* Copyright (C) 2012-2022 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/generate_spec.mli b/generate_spec.mli index aa875221f040f274b9762c9b38b34dc6211e76f6..ac2305c3a2fae23de5a7989e6d98a301137c18b3 100644 --- a/generate_spec.mli +++ b/generate_spec.mli @@ -2,7 +2,7 @@ (* *) (* This file is part of Frama-Clang *) (* *) -(* Copyright (C) 2012-2021 *) +(* Copyright (C) 2012-2022 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/intermediate_format.ast b/intermediate_format.ast index 79a6a561486877acdfab84c7755e73ddd572dc9a..e237db52043e3c28b3014c2d1444f06b2ff62ac9 100644 --- a/intermediate_format.ast +++ b/intermediate_format.ast @@ -2,7 +2,7 @@ (* *) (* This file is part of Frama-Clang *) (* *) -(* Copyright (C) 2012-2021 *) +(* Copyright (C) 2012-2022 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/mainpage.dox b/mainpage.dox index 102d18a5b0359caca5a309c508d84cfe7c5a25d0..4b250058803234624beec2841c35f7060d5b3f43 100644 --- a/mainpage.dox +++ b/mainpage.dox @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/mangling.ml b/mangling.ml index 0c958e14e0cb9ac3d14bdb98884436e33bd735ef..51b84c99ee8760a40c5f1511dccbb632dba4fc0c 100644 --- a/mangling.ml +++ b/mangling.ml @@ -2,7 +2,7 @@ (* *) (* This file is part of Frama-Clang *) (* *) -(* Copyright (C) 2012-2021 *) +(* Copyright (C) 2012-2022 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) @@ -801,6 +801,7 @@ let short_name name = let is_constructor_name name = basename name = "Ctor" let () = - Frama_Clang_option.Unmangling.register_mangling_func "short" short_name; - Frama_Clang_option.Unmangling.register_mangling_func "full" unmangle; - Frama_Clang_option.Unmangling.set "short" + Frama_Clang_option.add_unmangling_function + "without-qualifier" "short version of the symbol" short_name; + Frama_Clang_option.add_unmangling_function + "fully-qualified" "fully qualified symbol" unmangle diff --git a/mangling.mli b/mangling.mli index f4433d8f9c15365394034e9ae0b7fcc98866f991..29cae0c066181198ad56163735d0605bbb407ef6 100644 --- a/mangling.mli +++ b/mangling.mli @@ -2,7 +2,7 @@ (* *) (* This file is part of Frama-Clang *) (* *) -(* Copyright (C) 2012-2021 *) +(* Copyright (C) 2012-2022 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/reorder_defs.mli b/reorder_defs.mli index b2fb3a48bc48276de9aad0e649233838af073925..1ce6f4a946456c6a4a3091a2e56ac78aaef5b984 100644 --- a/reorder_defs.mli +++ b/reorder_defs.mli @@ -2,7 +2,7 @@ (* *) (* This file is part of Frama-Clang *) (* *) -(* Copyright (C) 2012-2021 *) +(* Copyright (C) 2012-2022 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) diff --git a/share/libc++/__fc_define_char_traits_char b/share/libc++/__fc_define_char_traits_char index d21f04651c82c77173de771dc553eacf505f90e3..0ddc7d950ad76526783683d414c5fb47791d1197 100644 --- a/share/libc++/__fc_define_char_traits_char +++ b/share/libc++/__fc_define_char_traits_char @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/__fc_define_fpos b/share/libc++/__fc_define_fpos index e6356b71396aa5090e9edad357915e8d889957ce..61d65f97b63ad02b7eccea1d8ac05fcb6529e29e 100644 --- a/share/libc++/__fc_define_fpos +++ b/share/libc++/__fc_define_fpos @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/__fc_define_ios_base_seekdir b/share/libc++/__fc_define_ios_base_seekdir index 95dfcfb372660c67a1a13106553a225979c45a88..2c603068c557352c8afda7a53de7bf2b7952baec 100644 --- a/share/libc++/__fc_define_ios_base_seekdir +++ b/share/libc++/__fc_define_ios_base_seekdir @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/__fc_define_mbstate_t b/share/libc++/__fc_define_mbstate_t index b99e5dd730535d0a0e57c77dd9ef1078b2875096..af345a80356fef3e70b89b2ecffcfd32034b3eca 100644 --- a/share/libc++/__fc_define_mbstate_t +++ b/share/libc++/__fc_define_mbstate_t @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/__fc_define_streamoff b/share/libc++/__fc_define_streamoff index 00762f6906365c78f65a77dddc68f4772c675c1a..2a61559a802e8b67faf6ff29b34c03ce9896e251 100644 --- a/share/libc++/__fc_define_streamoff +++ b/share/libc++/__fc_define_streamoff @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/__fc_define_streampos b/share/libc++/__fc_define_streampos index 6bfb9b0d0d6642104d85f2aeac2ebb6af578160d..bf762f6dd4488af84d9e6e80c9faccfbb64c40c9 100644 --- a/share/libc++/__fc_define_streampos +++ b/share/libc++/__fc_define_streampos @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/__fc_define_streamsize b/share/libc++/__fc_define_streamsize index f5cab56e61b3b0a0bfc472bd54a8e8d52cfd6b63..094f5be2458d78c85959322efa00942f83b248c0 100644 --- a/share/libc++/__fc_define_streamsize +++ b/share/libc++/__fc_define_streamsize @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/algorithm b/share/libc++/algorithm index 92991571b2fae39cc7079860f2e8019ee0b114b3..61177aa14c1739a804cc9ef55afb45aef225b242 100644 --- a/share/libc++/algorithm +++ b/share/libc++/algorithm @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/array b/share/libc++/array index 6e9372c36552b74e08857e5a2a7ec935051cc695..bc58c84df86ff9b03ed73f9bfe1b28b3705f5d54 100644 --- a/share/libc++/array +++ b/share/libc++/array @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/atomic b/share/libc++/atomic index 794dc870364b2bb076e87647a661ac775eee08fd..1f9fbcd87641a1cb1a8328513f3a7fbad4ac0c23 100644 --- a/share/libc++/atomic +++ b/share/libc++/atomic @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/bitset b/share/libc++/bitset index 1fc147084bdde509ff1af7f5833746da56554219..1877e34d3eaee05fe7a84956ab2d69d04e1ef039 100644 --- a/share/libc++/bitset +++ b/share/libc++/bitset @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/cassert b/share/libc++/cassert index cfc2759bc717110c6b2e0d33f75cb26fc4aa75d5..a98a577218a67ae0eea2556a93c53c0b682d54c7 100644 --- a/share/libc++/cassert +++ b/share/libc++/cassert @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/cerrno b/share/libc++/cerrno index ea104d7d9cc98f91fb798d0c4d6dcfdb9fa2d1dc..5a6443f6e4803e35165fd60f18c27ab4ee3dafbf 100644 --- a/share/libc++/cerrno +++ b/share/libc++/cerrno @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/climits b/share/libc++/climits index 431caa0f13d333a5bd60dcaac66ebae3ff7f86f4..8bb431996cf9f00442e1800f8b07d06b44906154 100644 --- a/share/libc++/climits +++ b/share/libc++/climits @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/clocale b/share/libc++/clocale index 86be8542ff4e811c656ffe3eade2c61303a3b99d..a5bcede6713d722a87acc2bc08037493de4e8e8f 100644 --- a/share/libc++/clocale +++ b/share/libc++/clocale @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/cstdarg b/share/libc++/cstdarg index 6162a46a28c645a392ea98dcecfd4e6ee5cc983a..1c5574d05763881c0f5616cb8b076bcb9746d807 100644 --- a/share/libc++/cstdarg +++ b/share/libc++/cstdarg @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/cstdbool b/share/libc++/cstdbool index 93873b15e79ffd41056adb91f329e58eeb19ed3e..589ac5ef897862efdd91ae9d8dccea709f41d455 100644 --- a/share/libc++/cstdbool +++ b/share/libc++/cstdbool @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/cstddef b/share/libc++/cstddef index 42de6a8b79c219c130e358efb3dcb1c0bdb06aa8..8da0fa7754e72cf69d2788a24d5df5b260f20363 100644 --- a/share/libc++/cstddef +++ b/share/libc++/cstddef @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/cstdint b/share/libc++/cstdint index d4e475326dbdab7eb46d1e646e5abd81164139e6..1ef9f308fb73a1e7ddb5f4ab594a024e1a92120c 100644 --- a/share/libc++/cstdint +++ b/share/libc++/cstdint @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/cstdio b/share/libc++/cstdio index 246617d9aa4a88aeb72b5bdfc9f7bc94ee0af8a6..745fcf3cbd91a5a63221cfaabd6cde0cbe5ab681 100644 --- a/share/libc++/cstdio +++ b/share/libc++/cstdio @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/cstdlib b/share/libc++/cstdlib index c226cefa165827da947a7d183df3443b13adb548..ee82d8c56055c72aad0a8f382a374d26e0ff32bd 100644 --- a/share/libc++/cstdlib +++ b/share/libc++/cstdlib @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/cstring b/share/libc++/cstring index a82b8459066b2fc46dd7a964f5ec367db54b7905..8cfab2a7e99ccea9bd92e4106d392118a2cb9125 100644 --- a/share/libc++/cstring +++ b/share/libc++/cstring @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/ctime b/share/libc++/ctime index b2ed957b3cbae16098a91bac85656b0e4e9aa746..d4ff4366cb653f3c6dff24d1118ff982bc506694 100644 --- a/share/libc++/ctime +++ b/share/libc++/ctime @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/cwchar b/share/libc++/cwchar index bcc3dd29404cbfeeb8139beaad047a77e51194bd..ea4cc074150ad8f1054d17db7c95c5b415c584d9 100644 --- a/share/libc++/cwchar +++ b/share/libc++/cwchar @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/cxx_builtin.cc b/share/libc++/cxx_builtin.cc index 232f594ed40dbbf9906e0f68ee72303074fd5a1a..ebb0557626aead6e27b91f15313646b1b572e48e 100644 --- a/share/libc++/cxx_builtin.cc +++ b/share/libc++/cxx_builtin.cc @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/cxxabi.h b/share/libc++/cxxabi.h index 448614e86428524a49e4188c6a5ed195e4f993d2..27b4f978ddeedb0038b17907655c60f90b11479c 100644 --- a/share/libc++/cxxabi.h +++ b/share/libc++/cxxabi.h @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/exception b/share/libc++/exception index 95440187333278c105f10e3286b42ebc9caa5c53..a3e97e5e186e27a9f4b1304a83c3c2a94b406e26 100644 --- a/share/libc++/exception +++ b/share/libc++/exception @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/functional b/share/libc++/functional index acf1ba77635f7ec5db78e670b346aaeb5f56a54d..c1abdb619197d6629e5c5d6a641ee70eb5f5da6d 100644 --- a/share/libc++/functional +++ b/share/libc++/functional @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/initializer_list b/share/libc++/initializer_list index 374710fc1f501bf05ea85f4b33ded1bb27c1360b..d749230fbdc148873c81433cf7be1b3051a3ad3e 100644 --- a/share/libc++/initializer_list +++ b/share/libc++/initializer_list @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/ios b/share/libc++/ios index b53e9ae9c3029984b56b059c52ac4634af302467..62747f668d09f55ed6e52714e559451c4ff8b03a 100644 --- a/share/libc++/ios +++ b/share/libc++/ios @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/iosfwd b/share/libc++/iosfwd index b5978c0022ef6ab75adcbf89055909f2b79fe40b..a8d1301e0c8dd36a0623a7d70a11dfa607bcf803 100644 --- a/share/libc++/iosfwd +++ b/share/libc++/iosfwd @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/iostream b/share/libc++/iostream index c8b53835c5cfb465d238df1063489a7dfa9dcd9b..83cf962e3737e74f9cd0c2c230e99fc9aebd2931 100644 --- a/share/libc++/iostream +++ b/share/libc++/iostream @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/istream b/share/libc++/istream index ee498d114b3f1fa670f640a5c5c406f9dbfadc8a..770b275cfc77ee98b23f1ce30f200345735ee277 100644 --- a/share/libc++/istream +++ b/share/libc++/istream @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/iterator b/share/libc++/iterator index b12e7f41383475218af84e4b89daa49291fa2e84..a8f2737fc94b66fd8542d491bd8ccf82c3016200 100644 --- a/share/libc++/iterator +++ b/share/libc++/iterator @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/locale b/share/libc++/locale index 6cbf322a4cf4306e4463f4b41aa8eb95d082464f..50354f4ca6a16ab7f9b7c23d3260b21e5f16b20c 100644 --- a/share/libc++/locale +++ b/share/libc++/locale @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/memory b/share/libc++/memory index 2c13f2ba59a8e9ffbc5fce3ceaab8c373aff76ee..5e7df28a3115ab8e7bb6205946cdcbbda3e7de49 100644 --- a/share/libc++/memory +++ b/share/libc++/memory @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/new b/share/libc++/new index a24abaf4776a869d6d8c0013cb02522c75a66c79..a99349d6410bf879e8db60972cea19b67b7902c2 100644 --- a/share/libc++/new +++ b/share/libc++/new @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/ostream b/share/libc++/ostream index 7f7c1ebad2813030043d94f0e9ab4064773194a4..3620e22f7a046a7cde62e6d1fdf6c45ce56f04e9 100644 --- a/share/libc++/ostream +++ b/share/libc++/ostream @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/stdexcepts b/share/libc++/stdexcepts index c20e060640b585a7ef4f2d0f27d8657cd5758653..a5fe7af186ef8a2dba9d819e06e243974eb3d74a 100644 --- a/share/libc++/stdexcepts +++ b/share/libc++/stdexcepts @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/streambuf b/share/libc++/streambuf index 00a57d8a13f361502993e3bc1ef5f56813cf47cd..d21f51a4fd2e81b52cf6462da8a93e9e39ffad1b 100644 --- a/share/libc++/streambuf +++ b/share/libc++/streambuf @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/string b/share/libc++/string index 3c61dac361072052826618c028cbd64f0bfd6385..ea26c142f372f91c25af435c680b7c2faa136a59 100644 --- a/share/libc++/string +++ b/share/libc++/string @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/system_error b/share/libc++/system_error index 71ce408af97a92299843222bc4cb8bdaeebc2a13..490fa287353e3ae79a9032d61f778111b01294c9 100644 --- a/share/libc++/system_error +++ b/share/libc++/system_error @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/type_traits b/share/libc++/type_traits index 37c53563284cabeaae444e3e5c574bbecc2f54d6..5a1c9b0313318b10902abb9ba8d1f687dee51977 100644 --- a/share/libc++/type_traits +++ b/share/libc++/type_traits @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/typeinfo b/share/libc++/typeinfo index 6212829ae201c6fce969914e464761dfac518ee7..3eab620efaa046a42f07bcab951f3c0b1b00e466 100644 --- a/share/libc++/typeinfo +++ b/share/libc++/typeinfo @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/share/libc++/utility b/share/libc++/utility index 4ac360afd350787866d215e8dcf99512a3411762..8fe1d405af09b02bab6f57a1057be9d7d5e7f93f 100644 --- a/share/libc++/utility +++ b/share/libc++/utility @@ -2,7 +2,7 @@ /* */ /* This file is part of Frama-Clang */ /* */ -/* Copyright (C) 2012-2021 */ +/* Copyright (C) 2012-2022 */ /* CEA (Commissariat à l'énergie atomique et aux énergies */ /* alternatives) */ /* */ diff --git a/tests/basic/oracle/printer.res.c b/tests/basic/oracle/printer.res.c new file mode 100644 index 0000000000000000000000000000000000000000..8a05f7715faa35df236be5d7f6f9b6541478d15b --- /dev/null +++ b/tests/basic/oracle/printer.res.c @@ -0,0 +1,50 @@ +/* Generated by Frama-C */ +struct _Z20_frama_c_vmt_content { + void (*method_ptr)() ; + int shift_this ; +}; +struct _Z28_frama_c_rtti_name_info_node; +struct _Z12_frama_c_vmt { + struct _Z20_frama_c_vmt_content *table ; + int table_size ; + struct _Z28_frama_c_rtti_name_info_node *rtti_info ; +}; +struct _Z31_frama_c_rtti_name_info_content { + struct _Z28_frama_c_rtti_name_info_node *value ; + int shift_object ; + int shift_vmt ; +}; +struct _Z28_frama_c_rtti_name_info_node { + char const *name ; + struct _Z31_frama_c_rtti_name_info_content *base_classes ; + int number_of_base_classes ; + struct _Z12_frama_c_vmt *pvmt ; +}; +struct _ZN1AE1B; +struct _ZN1AE1B { + int x ; +}; +struct _Z28_frama_c_rtti_name_info_node _ZN1A1BE23_frama_c_rtti_name_info; + +/*@ requires \valid_read(this); */ +void _ZN1A1BEC1(struct _ZN1AE1B const *this __attribute__((____fc_initialized_object__))) +{ + this->x = 42; + return; +} + +struct _Z28_frama_c_rtti_name_info_node _ZN1A1BE23_frama_c_rtti_name_info = + {.name = "B", + .base_classes = (struct _Z31_frama_c_rtti_name_info_content *)0, + .number_of_base_classes = 0, + .pvmt = (struct _Z12_frama_c_vmt *)0}; +int main(void) +{ + int __retres; + struct _ZN1AE1B b; + _ZN1A1BEC1(& b); + __retres = b.x; + return __retres; +} + + diff --git a/tests/basic/oracle/printer.res2.c b/tests/basic/oracle/printer.res2.c new file mode 100644 index 0000000000000000000000000000000000000000..7429be90efd6040f4f808241dff999931db7978c --- /dev/null +++ b/tests/basic/oracle/printer.res2.c @@ -0,0 +1,50 @@ +/* Generated by Frama-C */ +struct _frama_c_vmt_content { + void (*method_ptr)() ; + int shift_this ; +}; +struct _frama_c_rtti_name_info_node; +struct _frama_c_vmt { + struct _frama_c_vmt_content *table ; + int table_size ; + struct _frama_c_rtti_name_info_node *rtti_info ; +}; +struct _frama_c_rtti_name_info_content { + struct _frama_c_rtti_name_info_node *value ; + int shift_object ; + int shift_vmt ; +}; +struct _frama_c_rtti_name_info_node { + char const *name ; + struct _frama_c_rtti_name_info_content *base_classes ; + int number_of_base_classes ; + struct _frama_c_vmt *pvmt ; +}; +struct B; +struct B { + int x ; +}; +struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info; + +/*@ requires \valid_read(this); */ +void B::Ctor(struct B const *this) +{ + this->x = 42; + return; +} + +struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info = + {.name = "B", + .base_classes = (struct _frama_c_rtti_name_info_content *)0, + .number_of_base_classes = 0, + .pvmt = (struct _frama_c_vmt *)0}; +int main(void) +{ + int __retres; + struct B b; + B::Ctor((struct B const *)(& b)); + __retres = b.x; + return __retres; +} + + diff --git a/tests/basic/printer.cpp b/tests/basic/printer.cpp new file mode 100644 index 0000000000000000000000000000000000000000..cea6de5029e705209075820a15a335f108edeb48 --- /dev/null +++ b/tests/basic/printer.cpp @@ -0,0 +1,17 @@ +/* run.config +NOFRAMAC: +EXECNOW: LOG printer.res.c @frama-c@ @PTEST_FILE@ @CXX@ @MACHDEP@ -cxx-parseable-output -ocode @PTEST_RESULT@/printer.res.c -print +EXECNOW: LOG printer.res2.c @frama-c@ @CXX@ @MACHDEP@ -cxx-unmangling without-qualifier @PTEST_RESULT@/printer.res.c -ocode @PTEST_RESULT@/printer.res2.c -print +*/ + +namespace A { + struct B { + int x; + B() { x = 42; } + }; +}; // namespace A + +int main() { + A::B b; + return b.x; +}