diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index d604612c638ba2c5ada1eb5bb785245f22953997..118bc741e0f8b4be03fe59e1f98485058852fe71 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -27,6 +27,8 @@ tests-on-llvm-10: stage: tests script: - nix/frama-ci.sh build -A frama-clang.on-llvm10.tests + tags: + - nix when: manual tests-on-llvm-11: @@ -35,3 +37,11 @@ tests-on-llvm-11: - nix/frama-ci.sh build -A frama-clang.on-llvm11.tests tags: - nix + when: manual + +tests-on-llvm-13: + stage: tests + script: + - nix/frama-ci.sh build -A frama-clang.on-llvm13.tests + tags: + - nix diff --git a/ClangVisitor.cpp b/ClangVisitor.cpp index 1fcd7ff6f3ed2328c2b5d31c6515fefff1c61fdd..452446f60db4b4be7c6c6958ecfc2d581399494f 100644 --- a/ClangVisitor.cpp +++ b/ClangVisitor.cpp @@ -24,7 +24,12 @@ // Description: // Definition of a translator clang -> intermediate_format (-> cabs -> cil). // - +extern "C" { +#include "intermediate_format.h" +}; +#include <clang/AST/Expr.h> +#include <clang/AST/ExprCXX.h> +#include <llvm/Support/Casting.h> #ifdef __GNUC__ #pragma GCC diagnostic push #pragma GCC diagnostic ignored "-Wclass-memaccess" @@ -3910,9 +3915,23 @@ statement FramacVisitor::makeReturnStmt( bool* shouldDelay) { // implicit precondition: commentLocation != NULL => stmts != NULL // the reverse is not true any more thanks to cleanups - const clang::Expr* re = returnStmt->getRetValue(); - expression result = re ? makeLocExpression(re, shouldDelay) : NULL; - option e = re ? opt_some_container(result) : opt_none(); + option e = opt_none(); + expression result = NULL; + const clang::VarDecl* v = returnStmt->getNRVOCandidate(); + if (v && v->isNRVOVariable()) { + // The returned expression should be a CXXConstructorExpr, which + // is not marked as elidable since clang 13.0. Hence, do the elision here + const clang::CXXConstructExpr* ce = + llvm::dyn_cast<clang::CXXConstructExpr>(returnStmt->getRetValue()); + assert(ce && ce->getNumArgs() == 1); + const clang::Expr *re = ce->getArg(0); + result = makeLocExpression(re,shouldDelay); + } + else { + const clang::Expr* re = returnStmt->getRetValue(); + if (re) result = makeLocExpression(re, shouldDelay); + } + if (result) e = opt_some_container(result); if (stmts || !_cleanups.empty()) { /* statement */ list* cursor = forwardStmts.getBack() ? &forwardStmts.getBack()->next : &forwardStmts.getFront(); diff --git a/configure.ac b/configure.ac index 0571a058bfe5415adad1c42e6f5512a4ab6528ad..d9dccf69d7e10fbac1cddf94820e6ba841524bdb 100644 --- a/configure.ac +++ b/configure.ac @@ -63,9 +63,9 @@ AC_SUBST(RUN_TESTS) DEFAULT_FC_C_HEADERS=$datarootdir/frama-c/libc DEFAULT_FC_CXX_HEADERS=$datarootdir/libc++ -AC_CHECK_PROGS([CLANG],[clang clang-12 clang-11 clang-10 clang-9 clang-8 clang-7 clang-6.0],no) -AC_CHECK_PROGS([CLANGXX],[clang++ clang++-12 clang++-11 clang++-10 clang++-9 clang++-8 clang++-7 clang++6.0],no) -AC_CHECK_PROGS([LLVM_CONFIG],[llvm-config llvm-config-12 llvm-config-11 llvm-config-10 llvm-config-9 llvm-config-8 llvm-config-7 llvm-config-6.0],no) +AC_CHECK_PROGS([CLANG],[clang clang-13 clang-12 clang-11 clang-10 clang-9 clang-8 clang-7 clang-6.0],no) +AC_CHECK_PROGS([CLANGXX],[clang++ clang++13 clang++-12 clang++-11 clang++-10 clang++-9 clang++-8 clang++-7 clang++6.0],no) +AC_CHECK_PROGS([LLVM_CONFIG],[llvm-config llvm-config-13 llvm-config-12 llvm-config-11 llvm-config-10 llvm-config-9 llvm-config-8 llvm-config-7 llvm-config-6.0],no) if test "$LLVM_CONFIG" = "no"; then plugin_disable(frama_clang,[llvm-config not found]); @@ -95,8 +95,9 @@ case $LLVM_VERSION in 10.*) AC_MSG_RESULT([$LLVM_VERSION: Good]); RUN_TESTS=yes;; 11.*) AC_MSG_RESULT([$LLVM_VERSION: Good]); RUN_TESTS=yes;; 12.*) AC_MSG_RESULT([$LLVM_VERSION: Good]); RUN_TESTS=yes;; + 13.*) AC_MSG_RESULT([$LLVM_VERSION: Good]); RUN_TESTS=yes;; *) plugin_disable(frama_clang, - [[LLVM Version $LLVM_VERSION is not supported. Please install LLVM 6.x, 7.x, 8.x, 9.x, 10.x, 11.x, or 12.x]]);; + [[LLVM Version $LLVM_VERSION is not supported. Please install LLVM 6.x, 7.x, 8.x, 9.x, 10.x, 11.x, 12.x, or 13.x]]);; esac LLVM_CONFIG="$LLVM_CONFIG $LLVM_STATIC" diff --git a/nix/default.nix b/nix/default.nix index 32d6548e052e7f3deb6bb23e0a1155c8e5e54ecb..eeef53864cd131b122c4a831180898a722321910 100644 --- a/nix/default.nix +++ b/nix/default.nix @@ -23,10 +23,18 @@ let frama_clang_build = why3 config detect ''; }); + pkgs = import ( + builtins.fetchTarball { + url = "https://github.com/NixOS/nixpkgs/archive/ed2c99e65f4f5f4bf3bb3a3422f07fc8ec9a97ce.tar.gz"; + sha256="1bp4fkswpl7s2clxbdbff8j42dsns4ihvc5l9399v9kapxb7wx5f"; + } + ) + {}; in (frama_clang_build { llvm_version="9"; }) .extend( self: super: { on-llvm10 = (frama_clang_build { llvm_version="10"; }); on-llvm11 = (frama_clang_build { llvm_version="11"; }); + on-llvm13 = (frama_clang_build { inherit pkgs; llvm_version="13"; }); }) diff --git a/tests/val_analysis/oracle/result.res.oracle b/tests/val_analysis/oracle/result.res.oracle index 3b23f6ed4e6a82458c2a697f5f940cc5022c3ae0..e4d64e807d194b5da2b6f5cc6dbaa1f4dc203fb5 100644 --- a/tests/val_analysis/oracle/result.res.oracle +++ b/tests/val_analysis/oracle/result.res.oracle @@ -7,16 +7,22 @@ Now output intermediate result _frama_c_rtti_name_info.name ∈ {{ "A" }} {.base_classes; .number_of_base_classes; .pvmt} ∈ {0} -[eva:alarm] tests/val_analysis/result.cc:7: Warning: - function f, behavior default: postcondition got status invalid. [eva] done for function main [eva] ====== VALUES COMPUTED ====== +[eva:final-states] Values at end of function g: + __retres ∈ {3} [eva:final-states] Values at end of function A::Ctor: a ∈ {0} +[eva:final-states] Values at end of function A::Ctor: + __fc_tmp_1.x ∈ {3} [eva:final-states] Values at end of function A::Dtor: [eva:final-states] Values at end of function f: a.x ∈ {2} z ∈ {2} [eva:final-states] Values at end of function main: - NON TERMINATING FUNCTION + b.x ∈ {2} + __fc_tmp_0.x ∈ {2} + z ∈ {3} + __fc_tmp_1.x ∈ {3} + __retres ∈ {0} diff --git a/tests/val_analysis/result.cc b/tests/val_analysis/result.cc index 275321a823661d21bbc9f5b9f4bd5b4b938cf2ef..2fb26faabab5c8c73076f4ef70374e4366a512b8 100644 --- a/tests/val_analysis/result.cc +++ b/tests/val_analysis/result.cc @@ -4,7 +4,6 @@ struct A { A(const A& a) { x = a.x + 1; } }; -/*@ behavior default: ensures \result.x == y; */ A f(int y) { A a; int z = y -1;