[Analysis-scripts] update list-files

share/analysis-scripts/list_files.py

@@ -31,58 +31,69 @@ import sys
 import os
 import json
 import re
+from pathlib import Path
+
+MIN_PYTHON = (3, 6) # for glob(recursive) and automatic Path conversions
+if sys.version_info < MIN_PYTHON:
+    sys.exit("Python %s.%s or later is required.\n" % MIN_PYTHON)
 
-arg = ""
 if len(sys.argv) < 2:
    # no argument, assume default name
-   arg = "compile_commands.json"
+   arg = Path("compile_commands.json")
 else:
-   arg = sys.argv[1]
+   arg = Path(sys.argv[1])
 
-if not os.path.exists(arg):
+if not arg.exists():
    print(f"error: file '{arg}' not found")
    sys.exit(f"usage: {sys.argv[0]} [compile_commands.json]")
 
 # check if arg has a known extension
-def has_known_c_extension(arg):
-   return arg.endswith(".c") or arg.endswith(".i") or arg.endswith(".h")
+def is_known_c_extension(ext):
+   return ext == ".c" or ext == ".i" or ext == ".h"
 
 pwd = os.getcwd()
+fcmake_pwd = pwd / Path(".frama-c") # pwd as seen by the Frama-C makefile
 json = json.loads(open(arg).read())
-jcdb_dir = os.path.dirname(arg)
+jcdb_dir = arg.parent
 includes = set()
 defines = set()
-files = set()
+files = set() # set of pairs of (file, file_for_fcmake)
 for entry in json:
    arg_includes = [] # before normalization
-   dir = entry["directory"]
-   file = entry["file"]
-   # json compile spec says either command or arguments are mandatory
-   if os.path.isabs(file):
+   if not "file" in entry:
+       # ignore entries without a filename
+       continue
+   file = Path(entry["file"])
+   dir = Path(entry["directory"]) if "directory" in entry else None
+   if file.is_absolute():
       filepath = file
-   elif os.path.isabs(dir):
-      filepath = os.path.join(dir, file)
+   elif dir and dir.is_absolute():
+      filepath = dir / file
+   elif dir:
+      filepath = jcdb_dir / dir / file
    else:
-      filepath = os.path.join(jcdb_dir, dir, file)
-   if not has_known_c_extension(filepath):
+      filepath = jcdb_dir / file
+   if not is_known_c_extension(filepath.suffix):
       print(f"warning: ignoring file of unknown type: {filepath}")
    else:
-      files.add(os.path.relpath(filepath, pwd))
+      files.add((os.path.relpath(filepath, pwd), os.path.relpath(filepath, fcmake_pwd)))
 
-print("SRCS=\\\n" + " \\\n".join(sorted(files)) + " \\")
+files_for_fcmake = map (lambda x:(x[1]), files)
+print("# Paths as seen by a makefile inside subdirectory '.frama-c':")
+print("SRCS=\\\n" + " \\\n".join(sorted(files_for_fcmake)) + " \\")
 print("")
 
 files_defining_main = set()
 re_main = re.compile("(int|void)\s+main\s*\([^)]*\)\s*\{")
-for file in files:
+for (file, file_for_fcmake) in files:
    assert os.path.exists(file), "file does not exist: %s" % file
    with open(file, 'r') as content_file:
       content = content_file.read()
       res = re.search(re_main, content)
       if res is not None:
-         files_defining_main.add(file)
+         files_defining_main.add(file_for_fcmake)
 
 if files_defining_main != []:
    print("")
-   print("# Possible definition of main function in the following file(s):")
+   print("# Possible definition of main function in the following file(s), as seen from '.frama-c':")
    print("\n".join(sorted(files_defining_main)))

tests/fc_script/oracle/list_files.res

+# Paths as seen by a makefile inside subdirectory '.frama-c':
 SRCS=\
-tests/fc_script/main.c \
-tests/fc_script/main2.c \
-tests/fc_script/main3.c \
+../tests/fc_script/main.c \
+../tests/fc_script/main2.c \
+../tests/fc_script/main3.c \
 
 
-# Possible definition of main function in the following file(s):
-tests/fc_script/main.c
-tests/fc_script/main3.c
+# Possible definition of main function in the following file(s), as seen from '.frama-c':
+../tests/fc_script/main.c
+../tests/fc_script/main3.c

tests/jcdb/oracle/list_files.res

+# Paths as seen by a makefile inside subdirectory '.frama-c':
 SRCS=\
-tests/jcdb/file_without_main.c \
-tests/jcdb/jcdb.c \
+../tests/jcdb/file_without_main.c \
+../tests/jcdb/jcdb.c \
 
 
-# Possible definition of main function in the following file(s):
-tests/jcdb/jcdb.c
+# Possible definition of main function in the following file(s), as seen from '.frama-c':
+../tests/jcdb/jcdb.c