diff --git a/share/analysis-scripts/estimate_difficulty.py b/share/analysis-scripts/estimate_difficulty.py index a4fb891a9f0077da691860b6125ae3f5b88f42a2..f0d29811a64f3ab90b63471a750be84fb5a11a1e 100755 --- a/share/analysis-scripts/estimate_difficulty.py +++ b/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 diff --git a/tests/fc_script/estimate-difficulty.t/estimate-difficulty.c b/tests/fc_script/estimate-difficulty.t/estimate-difficulty.c index 8a595e24c9b96bae70c579aa8b06ee518cc6b72e..4cff9e42340f58f113eb708383fd3a69692c38be 100644 --- a/tests/fc_script/estimate-difficulty.t/estimate-difficulty.c +++ b/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; diff --git a/tests/fc_script/estimate-difficulty.t/run.t b/tests/fc_script/estimate-difficulty.t/run.t index 01545694bb1b4fd051595a1e488270d16952036e..91b68551038a7b639be2e847c8b5e072a99ba10a 100644 --- a/tests/fc_script/estimate-difficulty.t/run.t +++ b/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'