Merge remote-tracking branch 'origin/stable/chromium'

.gitlab-ci.yml

@@ -37,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();

Makefile

@@ -77,10 +77,10 @@ tests:: dontrun
 dontrun:
 	(cd tests; echo `grep -r 'DONTRUN' $(PLUGIN_TESTS_DIRS) | wc -l` test files marked DONTRUN )
 
-$(Frama_Clang_DIR)/gen_ast: $(Frama_Clang_DIR)/gen_ast.ml
+$(Frama_Clang_DIR)/gen_ast: $(Frama_Clang_DIR)/gen_ast.ml $(Frama_Clang_DIR)/gen_ast.cmi
 	$(PRINT_OCAMLC) $@
 	$(OCAMLC) $(Frama_Clang_BFLAGS) -o $@ -pp $(CAMLP5O) \
-        zarith.cma dynlink.cma $^
+        zarith.cma dynlink.cma $<
 
 $(Frama_Clang_DIR)/test_ast: \
   $(Frama_Clang_DIR)/intermediate_format.cmo \

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"

gen_ast.mli

+(* Nothing is exported *)

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

reorder_defs.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)                                                  *)
 (*                                                                        *)
@@ -41,7 +41,7 @@ type dep_node =
     name: string;
     is_def: bool;
     mutable glob: definition option;
-    mutable ghost: bool; (* TODO: take ghost into account. *)
+    (* mutable ghost: bool; (* TODO: take ghost into account. *) *)
     mutable id: int
   }
 
@@ -179,7 +179,7 @@ end = struct
   let nodes = H.create 37
 
   let default_node kind name is_def =
-    { kind; name; is_def; glob = None; id = -1; ghost = false }
+    { kind; name; is_def; glob = None; id = -1; (* ghost = false *) }
 
   let replace_deps orig rep =
     if G.mem_vertex deps orig then begin

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] 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;