Merge branch 'feature/llvm-13' into 'stable/chromium'

Update for LLVM-13 compatibility

See merge request frama-c/frama-clang!163

.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

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();

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"

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"; });
     })

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}

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;