Prefer potential duplicate definitions in AST over NON TERMINATING analysis result

This allow analysis for a widely used C++ construct. Please find more details in the bugtracker:
frama-c#2564

ClangVisitor.cpp

@@ -7410,25 +7410,42 @@ bool FramacVisitor::VisitFunctionDecl(clang::FunctionDecl* Decl) {
         if (isInstance && Decl->getPrimaryTemplate())
           _clangUtils->popTemplateInstance(Decl->getPrimaryTemplate());
         if (!waitDeclarations.empty()) {
-          func->cons_translation_unit_decl.Function.body = opt_none();
-          translation_unit_decl copyFunc = translation_unit_decl_dup(func);
-          free(copyFunc->cons_translation_unit_decl.Function.body);
-          copyFunc->cons_translation_unit_decl.Function.body = body;
+          //
+          // The code below was commented out in order to allow analysis for a
+          // widely used C++ construct. For the moment, it might be useful to
+          // leave it here, so the approach can be revisited easily. Please find
+          // more details in the bugtracker:
+          // https://git.frama-c.com/pub/frama-c/-/issues/2564
+          //
+          // It appears that it was the intention to avoid duplicate definitions
+          // in the output AST and instead only emit declarations for first
+          // occurences. However, this also caused the frama-c engine to
+          // generate default definitions for such first occurences and ignore
+          // the actual implementations later on.
+          //
+          // The duplicate definitions don't seem harmful and the test suite
+          // still works well. Analysis will use only one of them and report
+          // the other one as uncovered.
+          //
+          //func->cons_translation_unit_decl.Function.body = opt_none();
+          //translation_unit_decl copyFunc = translation_unit_decl_dup(func);
+          //free(copyFunc->cons_translation_unit_decl.Function.body);
+          //copyFunc->cons_translation_unit_decl.Function.body = body;
           if (_parents.hasLexicalContext() && !_parents.isClass())
             _parents.add(func);
           else {
             _globals.insertContainer(func);
           };
-          if (decl_name->tag_decl_or_impl_name == DECLARATION) {
-            decl_name->cons_decl_or_impl_name.Declaration.name = strdup("");
-            qualified_name qual = _clangUtils->makeQualifiedName(*Decl);
-            free(const_cast<char*>(qual->decl_name));
-            qual->decl_name = name;
-            free_decl_or_impl_name(decl_name);
-            decl_name = decl_or_impl_name_Implementation(qual);
-          };
+          //if (decl_name->tag_decl_or_impl_name == DECLARATION) {
+          //  decl_name->cons_decl_or_impl_name.Declaration.name = strdup("");
+          //  qualified_name qual = _clangUtils->makeQualifiedName(*Decl);
+          //  free(const_cast<char*>(qual->decl_name));
+          //  qual->decl_name = name;
+          //  free_decl_or_impl_name(decl_name);
+          //  decl_name = decl_or_impl_name_Implementation(qual);
+          //};
           _tableForWaitingDeclarations.addIncompleteFunction(Decl,
-              waitDeclarations, copyFunc);
+              waitDeclarations, func);
           isGenerationEffective = false;
         }
       };

tests/bugs/issue2564.cpp

 /* run.config
-OPT: @MACHDEP@ -deps
+OPT: @MACHDEP@ -deps -print
 */
 
-struct Foo;
-
+// Function func should be analysed based on its source definition. Generating
+// definitions with default assigns for it caused the misbehavior described in
+// the bug report:
+// https://git.frama-c.com/pub/frama-c/-/issues/2564
+//
+// Required preconditions that triggered the misbehavior:
+//   - function must be a template
+//   - function must be declared before the class used as template parameter
+//   - function must access a template member
+//   - function must be defined in a namespace
+//
 namespace test {
-  // Implementations of the two functions works() and fails() are equivalent.
-  // Their invocations from main() are equivalent as well. The only difference
-  // is that fails() gets DECLARED here, i.e. before its r-value return type got
-  // DEFINED. Commenting out this declaration avoids the problem.
-  //
-  // All known preconditions:
-  //  * function must be a template
-  //  * function must be in a namespace
-  //  * function must return an r-value reference
-  //  * function must be declared before the return type is defined
-  //
-  // This seems to be the root cause for misbehaviors of std::forward<T>() and
-  // std::move() on std::unique_ptr instances.
-  //
-  template <class X> Foo&& fails(Foo *foo, X x);
+  template <class T> T *func(T *foo, int x) {
+    foo->add(x);
+    return foo;
+  }
 }
 
 struct Foo {
@@ -28,21 +26,8 @@ struct Foo {
   void add(int x) { val = x; }
 };
 
-namespace test {
-  template <class X> Foo&& works(Foo *foo, X x) {
-    foo->add(x);
-    return static_cast<Foo&&>(*foo);
-  }
-
-  template <class X> Foo&& fails(Foo *foo, X x) {
-    foo->add(x);
-    return static_cast<Foo&&>(*foo);
-  }
-}
-
 int main(int argc, char **argv) {
   Foo foo;
-  int a = test::works(&foo, argc).get();
-  int b = test::fails(&foo, argc).get();
-  return a + b;
+  foo.add(argc);
+  return test::func(&foo, argc)->get();
 }

tests/bugs/oracle/issue2564.res.oracle

@@ -7,24 +7,19 @@ Now output intermediate result
   _frama_c_rtti_name_info.name ∈ {{ "Foo" }}
                          {.base_classes; .number_of_base_classes; .pvmt} ∈
                          {0}
-[eva:alarm] tests/bugs/issue2564.cpp:47: Warning: 
-  signed overflow. assert -2147483648 ≤ a + b;
-[eva:alarm] tests/bugs/issue2564.cpp:47: Warning: 
-  signed overflow. assert a + b ≤ 2147483647;
 [eva] done for function main
 [eva:summary] ====== ANALYSIS SUMMARY ======
   ----------------------------------------------------------------------------
-  6 functions analyzed (out of 6): 100% coverage.
-  In these functions, 18 statements reached (out of 18): 100% coverage.
+  5 functions analyzed (out of 6): 83% coverage.
+  In these functions, 12 statements reached (out of 12): 100% coverage.
   ----------------------------------------------------------------------------
   No errors or warnings raised during the analysis.
   ----------------------------------------------------------------------------
-  2 alarms generated by the analysis:
-       2 integer overflows
+  0 alarms generated by the analysis.
   ----------------------------------------------------------------------------
   Evaluation of the logical properties reached by the analysis:
     Assertions        0 valid     0 unknown     0 invalid      0 total
-    Preconditions     5 valid     0 unknown     0 invalid      5 total
+    Preconditions     4 valid     0 unknown     0 invalid      4 total
   100% of the logical properties reached have been proven.
   ----------------------------------------------------------------------------
 [from] Computing for function add
@@ -33,10 +28,8 @@ Now output intermediate result
 [from] Done for function get
 [from] Computing for function Foo::Ctor
 [from] Done for function Foo::Ctor
-[from] Computing for function fails<int>
-[from] Done for function fails<int>
-[from] Computing for function works<int>
-[from] Done for function works<int>
+[from] Computing for function func<Foo>
+[from] Done for function func<Foo>
 [from] Computing for function main
 [from] Done for function main
 [from] ====== DEPENDENCIES COMPUTED ======
@@ -47,12 +40,92 @@ Now output intermediate result
   \result FROM this; foo
 [from] Function Foo::Ctor:
   NO EFFECTS
-[from] Function fails<int>:
-  foo FROM foo; x
-  \result FROM foo
-[from] Function works<int>:
+[from] Function func<Foo>:
   foo FROM foo; x
   \result FROM foo
 [from] Function main:
   \result FROM argc
 [from] ====== END OF DEPENDENCIES ======
+/* 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 Foo;
+struct Foo {
+   int val ;
+};
+void add(struct Foo *this, int x);
+
+struct Foo *func<Foo>(struct Foo *foo, int x)
+{
+  add(foo,x);
+  return foo;
+}
+
+void Foo::Ctor(struct Foo const *this);
+
+struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
+
+/*@ requires \valid(this); */
+int get(struct Foo *this)
+{
+  int __retres;
+  __retres = this->val;
+  return __retres;
+}
+
+/*@ requires \valid(this); */
+void add(struct Foo *this, int x)
+{
+  this->val = x;
+  return;
+}
+
+/*@ requires \valid_read(this); */
+void Foo::Ctor(struct Foo const *this)
+{
+  return;
+}
+
+struct Foo *func<Foo>(struct Foo *foo, int x)
+{
+  add(foo,x);
+  return foo;
+}
+
+struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
+  {.name = "Foo",
+   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
+   .number_of_base_classes = 0,
+   .pvmt = (struct _frama_c_vmt *)0};
+int main(int argc, char **argv)
+{
+  int tmp_0;
+  struct Foo *tmp;
+  struct Foo foo;
+  Foo::Ctor(& foo);
+  add(& foo,argc);
+  tmp = func<Foo>(& foo,argc);
+  tmp_0 = get(tmp);
+  return tmp_0;
+}
+
+

tests/stl/stl_unique_ptr.cpp

+/* run.config
+OPT: @MACHDEP@ -deps -print
+*/
+
+#include <memory>
+
+int test_primitive_payload(int var) {
+  std::unique_ptr<int> up1(&var);
+  std::unique_ptr<int> up2(new int);
+  *up1 = var;
+  *up2 = 2;
+  std::swap(up1, up2);
+  up1.reset();
+
+  std::unique_ptr<int[]> up3(new int[2]);
+  up3[0] = *up2; // var
+  up3[1] = up3[0] + 1;
+
+  int *up2_raw = up2.release();
+  if (up2_raw != &var) {
+    delete up2_raw; // unreachable
+    return 0;
+  }
+
+  std::unique_ptr<int[]> up4 = std::move(up3);
+  std::unique_ptr<int[]> up5 = std::forward<std::unique_ptr<int[]>>(up4);
+
+  int *up5_raw =  up5.release();
+  int result = up5_raw[0];
+  delete[] up5_raw;
+
+  return result;
+}
+
+struct PlainOldStruct {
+  int val = 0;
+  int pull() { return val; }
+  void push(int x) { val = x; }
+};
+
+int test_struct_payload(int var) {
+  PlainOldStruct pos;
+  std::unique_ptr<PlainOldStruct> up1(&pos);
+  std::unique_ptr<PlainOldStruct> up2(new PlainOldStruct);
+  up1->push(var);
+  up2->push(up1->pull() + 1);
+  std::swap(up1, up2);
+  up1.reset();
+
+  std::unique_ptr<PlainOldStruct> up3 = std::move(up2);
+  std::unique_ptr<PlainOldStruct> up4 =
+      std::forward<std::unique_ptr<PlainOldStruct>>(up3);
+
+  int result = up4->pull();
+  PlainOldStruct *up4_raw = up4.release();
+  if (up4_raw != &pos) {
+    delete up4_raw; // unreachable
+    return 0;
+  }
+
+  return result;
+}
+
+// Declaration before use.
+template <typename T, int N = 0>
+class ClassTemplate {
+private:
+  T val = N;
+public:
+  T *pull();
+  void push(T *x);
+};
+
+// Use of declared ClassTemplate.
+int test_template_payload(int var) {
+  ClassTemplate<int> ct;
+  std::unique_ptr<ClassTemplate<int>> up1(&ct);
+  std::unique_ptr<ClassTemplate<int, 0>> up2(new ClassTemplate<int, 0>);
+  up1->push(&var);
+  std::swap(up1, up2);
+  up1.reset();
+
+  std::unique_ptr<ClassTemplate<int>> up3 = std::move(up2);
+  std::unique_ptr<ClassTemplate<int>> up4 =
+      std::forward<std::unique_ptr<ClassTemplate<int>>>(up3);
+
+  int result = *up4->pull(); // var
+  ClassTemplate<int> *up4_raw = up4.release();
+  if (up4_raw != &ct) {
+    delete up4_raw; // unreachable
+    return 0;
+  }
+
+  return result;
+}
+
+// Definitions after use.
+template <typename T, int N>
+T *ClassTemplate<T, N>::pull() { return &val; }
+
+template <typename T, int N>
+void ClassTemplate<T, N>::push(T *x) { val = *x; }
+
+// Driver loops through the input argc.
+int main(int argc, char *argv[]) {
+  int t1 = test_primitive_payload(argc);
+  int t2 = test_struct_payload(t1);
+  int t3 = test_template_payload(t2);
+  return t3; // Expecting output: \result FROM argc
+}