Merge branch 'feature/analysis-scripts/estimate-difficulty-int128' into 'master'

[analysis-scripts] add __int128 to list of unsupported features

See merge request frama-c/frama-c!4469

share/analysis-scripts/estimate_difficulty.py

@@ -309,18 +309,20 @@ if dyncallees:
     print(f"- note: calls to dynamic allocation functions: {', '.join(sorted(dyncallees))}")
 
 
-# unsupported C11-specific features
-
-c11_unsupported = [
-    "_Alignas",
-    "_Alignof",
-    "_Complex",
-    "_Imaginary",
-    "alignas",
-    "alignof",  # stdalign.h may use these symbols
+# unsupported C11 or non-standard specific features
+
+unsupported_keywords = [
+    ("_Alignas", "C11 construct"),
+    ("_Alignof", "C11 construct"),
+    ("_Complex", "C11 construct"),
+    ("_Imaginary", "C11 construct"),
+    ("alignas", "C11 construct"),
+    ("alignof", "C11 construct"),  # stdalign.h may use these symbols
+    ("__int128", "non-standard construct (GNU extension)"),
+    ("__uint128_t", "non-standard construct (GNU extension)"),
 ]
 
-for keyword in c11_unsupported:
+for keyword, message in unsupported_keywords:
     out = subprocess.Popen(
         ["grep", "-n", "\\b" + keyword + "\\b"] + files + ["/dev/null"],
         stdout=subprocess.PIPE,
@@ -331,7 +333,7 @@ for keyword in c11_unsupported:
         n = len(lines)
         print(
             f"- warning: found {n} line{'s' if n > 1 else ''} with occurrences of "
-            f"unsupported C11 construct '{keyword}'"
+            f"unsupported {message} '{keyword}'"
         )
 
 # assembly code

tests/fc_script/estimate-difficulty.t/estimate-difficulty.c

@@ -21,3 +21,6 @@ int main() {
   ccosl(); // warning: neither code nor spec
   dprintf(); // no warning: neither code nor spec, but handled by Variadic
 }
+
+__int128 large_int;
+_Complex complex;

tests/fc_script/estimate-difficulty.t/run.t

@@ -9,3 +9,5 @@
   Estimating difficulty for 3 '#include <header>' directives...
   - WARNING: included header <complex.h> is explicitly unsupported by Frama-C
   Header-related warnings: 1
+  - warning: found 1 line with occurrences of unsupported C11 construct '_Complex'
+  - warning: found 1 line with occurrences of unsupported non-standard construct (GNU extension) '__int128'