Adapt to goblint/analyzer#785

Author: michael-schwarz

gobpie-demos/chrony/chrony-4.2.json

@@ -52,9 +52,6 @@
   "exp": {
     "earlyglobs": true
   },
-  "dbg": {
-    "print_dead_code": true
-  },
   "cil": {
     "merge": {
       "inlines": false

gobpie-demos/silver-searcher/goblint.json

@@ -11,9 +11,6 @@
         "domain": "plain"
       }
     },
-    "dbg": {
-      "print_dead_code": true
-    },
     "exp": {
       "earlyglobs": true
     },
@@ -22,4 +19,4 @@
         "spawn": false
       }
     }
-  }
+  }

gobpie-demos/silver-searcher/the_silver_searcher.json

@@ -37,9 +37,6 @@
   "exp": {
     "earlyglobs": true
   },
-  "dbg": {
-    "print_dead_code": true
-  },
   "cil": {
     "merge": {
       "inlines": false

gobpie-demos/smtprc/smtprc-fuel.json

@@ -53,9 +53,6 @@
   "exp": {
     "earlyglobs": true
   },
-  "dbg": {
-    "print_dead_code": true
-  },
   "cil": {
     "merge": {
       "inlines": false

gobpie-demos/smtprc/smtprc.json

@@ -53,9 +53,6 @@
   "exp": {
     "earlyglobs": true
   },
-  "dbg": {
-    "print_dead_code": true
-  },
   "cil": {
     "merge": {
       "inlines": false

index/conf/zstd-race-baseline.json

@@ -63,9 +63,6 @@
       "ZSTD_customFree"
     ]
   },
-  "dbg": {
-    "print_dead_code": true
-  },
   "pre": {
     "cppflags": ["-DZSTD_NO_INTRINSICS", "-D_FORTIFY_SOURCE=0", "-DGOBLINT_NO_ASSERT", "-DGOBLINT_NO_BSEARCH"]
   },

index/conf/zstd-race-incrpostsolver.json

@@ -56,9 +56,6 @@
       "ZSTD_customFree"
     ]
   },
-  "dbg": {
-    "print_dead_code": true
-  },
   "pre": {
     "cppflags": ["-DZSTD_NO_INTRINSICS", "-D_FORTIFY_SOURCE=0", "-DGOBLINT_NO_ASSERT", "-DGOBLINT_NO_BSEARCH"]
   },

juliet/juliet_summary.py

@@ -15,7 +15,7 @@
 	try:
 		zip_path, _ = urllib.request.urlretrieve(juliet_url)
 		with zipfile.ZipFile(zip_path, "r") as f:
-			f.extractall()	
+			f.extractall()
 	except urllib.error.HTTPError:
 		os.system('echo "FAILURE: Download url invalid."')
 		quit()
@@ -31,7 +31,7 @@
 	path = sys.argv[1] # path + '/' + sys.argv[1]
 	# Checking if the path is valid
 	if not os.path.exists(juliet_path):
-		os.system('echo "PATH NOT FOUND: "' + path)	
+		os.system('echo "PATH NOT FOUND: "' + path)
 elif len(sys.argv) != 1:
 	os.system('echo "FAILURE: Run script with no arguments to run on all testcases or add path to a specific testcases folder (that has individual cases or folders containing testcases)."')
 	quit()
@@ -42,7 +42,7 @@
 
 # The definitive function that performs all the main operations:
 #	- Takes current working directory and HTML contents as input
-#	- Finds valid C files for Goblint in that dir and establishes 
+#	- Finds valid C files for Goblint in that dir and establishes
 #	other potential sub-directories for the future
 #	- Runs Goblint on valid test cases if they exist
 #	- Generates HTML table with new results from those cases
@@ -57,30 +57,30 @@ def goblint_analyse(current_directory, HTML_info):
 		HTML_info[0] = files_output_to_HTML(valid_files, current_directory, HTML_info[0])
 		HTML_info[1].append(current_directory)
 	return pot_directories, HTML_info
-		
-# Goes through all the files in given path, returns all suitable testcase files and 
+
+# Goes through all the files in given path, returns all suitable testcase files and
 # all directories that might potentially contain testcases1
 def check_path(filepath):
 	files = os.listdir(filepath)
 	v_files = [] # Valid files
 	dirs = [] # Directories
 	for f in files:
 		if re.search('^CWE', f) != None and re.search('[0-9]{2}a?\.c$', f) != None and re.search('w32', f) == None: v_files.append(f)
-		elif os.path.isdir(filepath + '/' + f): 
+		elif os.path.isdir(filepath + '/' + f):
 			dirs.append(f)
 	return v_files, dirs
-	
+
 # Runs Goblint to process a testcase function, testcase function will be either
 # '_good' or '_bad' determined by input parameter 'mode'
 def goblint_cmd(filepath, filename, mode):
 	func = re.sub('a?\.c$', mode, filename) # File ending is cut and replaced by mode
-	cmd = goblint_path + ' ' + filepath + ' ' + testsupport_files + ' -I ' + testsupport_path + ' --sets "mainfun[+]" ' + func + ' --enable dbg.print_dead_code --enable dbg.debug --enable printstats'
+	cmd = goblint_path + ' ' + filepath + ' ' + testsupport_files + ' -I ' + testsupport_path + ' --sets "mainfun[+]" ' + func + ' --enable dbg.debug --enable printstats'
 	print(filename + ' -- ' + mode[1:] + '     ', end='\r')
 	process = subprocess.run(cmd, shell=True, check=True, stdout=subprocess.PIPE, stderr=subprocess.PIPE, universal_newlines=True)
 	#title = '#####################\n' + mode.upper() + '\n#####################\n\n'
 	return cmd + "\n\n" + process.stdout + process.stderr
-	
-# Takes a list of testcase files as input and iterates through them to analyze 
+
+# Takes a list of testcase files as input and iterates through them to analyze
 # outputs for both 'good' and 'bad' function. Generates an HTML table based on outputs.
 def files_output_to_HTML(testcases, filepath, html_table):
 	# Creating column headers for the table
@@ -92,14 +92,14 @@ def files_output_to_HTML(testcases, filepath, html_table):
 		html_table += "    <th>{0}</th>\n".format(column.strip())
 	html_table += "  </tr>\n"
 	# Going through valid testcase files
-	testcases.sort()	
+	testcases.sort()
 	for t in testcases:
 		f_path = filepath + '/' + t
 		v_good = '-' # Vulnerabilities in 'good', initial value: nothing found
 		v_bad = '-' # Vulnerabilities in 'bad', initial value: nothing found
 		output_good = 'Function missing / Error unrelated to Goblint\n' # initial value
 		output_bad = 'Function missing / Error unrelated to Goblint\n' # initial value
-		# The upcoming 'try' statements are used because at least one test case 
+		# The upcoming 'try' statements are used because at least one test case
 		#from Juliet suite does not contain both functions.
 		try:
 			output_good = goblint_cmd(f_path, t, '_good') # 'good' function
@@ -111,7 +111,7 @@ def files_output_to_HTML(testcases, filepath, html_table):
 			if re.search(v_detection, output_bad) != None:
 				v_bad = 'X'
 		except: v_bad = '?'
-		
+
 		# Generating .txt file for the output
 		title = t + '\n\n'
 		good_title = '#####################\n_GOOD\n#####################\n\n'
@@ -134,9 +134,9 @@ def files_output_to_HTML(testcases, filepath, html_table):
 
 # # # MAIN PROCEDURES # # #
 
-# Regex string that is used to confirm that vulnerabilities were detected 
+# Regex string that is used to confirm that vulnerabilities were detected
 v_detection = 'is dead!|Summary for all memory locations:'
-	
+
 # Blanks for HTML content
 # '' - empty string for HTML table that will contain results from Goblint
 # [] - empty array for href values that will be used for table of contents
@@ -153,7 +153,7 @@ def files_output_to_HTML(testcases, filepath, html_table):
 current_dir = path
 # Running Goblint on current directory and getting new potential sub-directories
 directories, HTML = goblint_analyse(current_dir, HTML)
-		
+
 # Going through the main CWE directories if present
 directories.sort()
 for d in directories:
@@ -166,7 +166,7 @@ def files_output_to_HTML(testcases, filepath, html_table):
 		current_subdir = current_dir + '/' + s
 		# Running Goblint, max depth achieved so no sub-directories
 		goblint_analyse(current_subdir, HTML)
-		
+
 
 # Generating content for HTML
 HTML_content = '<p id="top" style="font-size:30px">RESULTS</p>\n'
@@ -177,7 +177,7 @@ def files_output_to_HTML(testcases, filepath, html_table):
 for href in HTML[1]:
 	HTML_content += '<a href="#' + href + '">' + href + '</a><br>\n'
 # Adding table of contents and results table together
-HTML_content = HTML_content + '<br><hr><br>\n' + HTML[0] + '<a href="#top">Go to top</a>'		
+HTML_content = HTML_content + '<br><hr><br>\n' + HTML[0] + '<a href="#top">Go to top</a>'
 # Creating HTML file
 with open('summary_table.html', 'w', encoding='utf-8') as file:
 	file.write(HTML_content)

pthread/aget_comb_traces_rel.yml

@@ -10,9 +10,9 @@
         ''/home/simmo/dev/goblint/sv-comp/analyzer/conf/traces-rel.json'' ''--set''
         ''dbg.timeout'' ''900'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
         ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.apron.privatization''
-        ''mutex-meet-tid-cluster12'' ''aget_comb.c'' ''--enable'' ''dbg.uncalled''
+        ''mutex-meet-tid-cluster12'' ''aget_comb.c''
         ''--enable'' ''allglobs'' ''--enable'' ''printstats'' ''--enable'' ''dbg.debug''
-        ''-v'' ''--enable'' ''dbg.print_dead_code'' ''--enable'' ''witness.yaml.enabled''
+        ''-v''  ''--enable'' ''witness.yaml.enabled''
         ''--set'' ''witness.yaml.path'' ''./aget_comb_traces_rel.yml'''
     task:
       input_files:
@@ -43,9 +43,9 @@
         ''/home/simmo/dev/goblint/sv-comp/analyzer/conf/traces-rel.json'' ''--set''
         ''dbg.timeout'' ''900'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
         ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.apron.privatization''
-        ''mutex-meet-tid-cluster12'' ''aget_comb.c'' ''--enable'' ''dbg.uncalled''
+        ''mutex-meet-tid-cluster12'' ''aget_comb.c''
         ''--enable'' ''allglobs'' ''--enable'' ''printstats'' ''--enable'' ''dbg.debug''
-        ''-v'' ''--enable'' ''dbg.print_dead_code'' ''--enable'' ''witness.yaml.enabled''
+        ''-v''  ''--enable'' ''witness.yaml.enabled''
         ''--set'' ''witness.yaml.path'' ''./aget_comb_traces_rel.yml'''
     task:
       input_files:
@@ -76,9 +76,9 @@
         ''/home/simmo/dev/goblint/sv-comp/analyzer/conf/traces-rel.json'' ''--set''
         ''dbg.timeout'' ''900'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
         ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.apron.privatization''
-        ''mutex-meet-tid-cluster12'' ''aget_comb.c'' ''--enable'' ''dbg.uncalled''
+        ''mutex-meet-tid-cluster12'' ''aget_comb.c''
         ''--enable'' ''allglobs'' ''--enable'' ''printstats'' ''--enable'' ''dbg.debug''
-        ''-v'' ''--enable'' ''dbg.print_dead_code'' ''--enable'' ''witness.yaml.enabled''
+        ''-v''  ''--enable'' ''witness.yaml.enabled''
         ''--set'' ''witness.yaml.path'' ''./aget_comb_traces_rel.yml'''
     task:
       input_files:
@@ -109,9 +109,9 @@
         ''/home/simmo/dev/goblint/sv-comp/analyzer/conf/traces-rel.json'' ''--set''
         ''dbg.timeout'' ''900'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
         ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.apron.privatization''
-        ''mutex-meet-tid-cluster12'' ''aget_comb.c'' ''--enable'' ''dbg.uncalled''
+        ''mutex-meet-tid-cluster12'' ''aget_comb.c''
         ''--enable'' ''allglobs'' ''--enable'' ''printstats'' ''--enable'' ''dbg.debug''
-        ''-v'' ''--enable'' ''dbg.print_dead_code'' ''--enable'' ''witness.yaml.enabled''
+        ''-v''  ''--enable'' ''witness.yaml.enabled''
         ''--set'' ''witness.yaml.path'' ''./aget_comb_traces_rel.yml'''
     task:
       input_files:
@@ -142,9 +142,9 @@
         ''/home/simmo/dev/goblint/sv-comp/analyzer/conf/traces-rel.json'' ''--set''
         ''dbg.timeout'' ''900'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
         ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.apron.privatization''
-        ''mutex-meet-tid-cluster12'' ''aget_comb.c'' ''--enable'' ''dbg.uncalled''
+        ''mutex-meet-tid-cluster12'' ''aget_comb.c''
         ''--enable'' ''allglobs'' ''--enable'' ''printstats'' ''--enable'' ''dbg.debug''
-        ''-v'' ''--enable'' ''dbg.print_dead_code'' ''--enable'' ''witness.yaml.enabled''
+        ''-v''  ''--enable'' ''witness.yaml.enabled''
         ''--set'' ''witness.yaml.path'' ''./aget_comb_traces_rel.yml'''
     task:
       input_files:
@@ -175,9 +175,9 @@
         ''/home/simmo/dev/goblint/sv-comp/analyzer/conf/traces-rel.json'' ''--set''
         ''dbg.timeout'' ''900'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
         ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.apron.privatization''
-        ''mutex-meet-tid-cluster12'' ''aget_comb.c'' ''--enable'' ''dbg.uncalled''
+        ''mutex-meet-tid-cluster12'' ''aget_comb.c''
         ''--enable'' ''allglobs'' ''--enable'' ''printstats'' ''--enable'' ''dbg.debug''
-        ''-v'' ''--enable'' ''dbg.print_dead_code'' ''--enable'' ''witness.yaml.enabled''
+        ''-v''  ''--enable'' ''witness.yaml.enabled''
         ''--set'' ''witness.yaml.path'' ''./aget_comb_traces_rel.yml'''
     task:
       input_files:
@@ -208,9 +208,9 @@
         ''/home/simmo/dev/goblint/sv-comp/analyzer/conf/traces-rel.json'' ''--set''
         ''dbg.timeout'' ''900'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
         ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.apron.privatization''
-        ''mutex-meet-tid-cluster12'' ''aget_comb.c'' ''--enable'' ''dbg.uncalled''
+        ''mutex-meet-tid-cluster12'' ''aget_comb.c''
         ''--enable'' ''allglobs'' ''--enable'' ''printstats'' ''--enable'' ''dbg.debug''
-        ''-v'' ''--enable'' ''dbg.print_dead_code'' ''--enable'' ''witness.yaml.enabled''
+        ''-v''  ''--enable'' ''witness.yaml.enabled''
         ''--set'' ''witness.yaml.path'' ''./aget_comb_traces_rel.yml'''
     task:
       input_files:
@@ -241,9 +241,9 @@
         ''/home/simmo/dev/goblint/sv-comp/analyzer/conf/traces-rel.json'' ''--set''
         ''dbg.timeout'' ''900'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
         ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.apron.privatization''
-        ''mutex-meet-tid-cluster12'' ''aget_comb.c'' ''--enable'' ''dbg.uncalled''
+        ''mutex-meet-tid-cluster12'' ''aget_comb.c''
         ''--enable'' ''allglobs'' ''--enable'' ''printstats'' ''--enable'' ''dbg.debug''
-        ''-v'' ''--enable'' ''dbg.print_dead_code'' ''--enable'' ''witness.yaml.enabled''
+        ''-v''  ''--enable'' ''witness.yaml.enabled''
         ''--set'' ''witness.yaml.path'' ''./aget_comb_traces_rel.yml'''
     task:
       input_files:
@@ -274,9 +274,9 @@
         ''/home/simmo/dev/goblint/sv-comp/analyzer/conf/traces-rel.json'' ''--set''
         ''dbg.timeout'' ''900'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
         ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.apron.privatization''
-        ''mutex-meet-tid-cluster12'' ''aget_comb.c'' ''--enable'' ''dbg.uncalled''
+        ''mutex-meet-tid-cluster12'' ''aget_comb.c''
         ''--enable'' ''allglobs'' ''--enable'' ''printstats'' ''--enable'' ''dbg.debug''
-        ''-v'' ''--enable'' ''dbg.print_dead_code'' ''--enable'' ''witness.yaml.enabled''
+        ''-v''  ''--enable'' ''witness.yaml.enabled''
         ''--set'' ''witness.yaml.path'' ''./aget_comb_traces_rel.yml'''
     task:
       input_files:
@@ -307,9 +307,9 @@
         ''/home/simmo/dev/goblint/sv-comp/analyzer/conf/traces-rel.json'' ''--set''
         ''dbg.timeout'' ''900'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
         ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.apron.privatization''
-        ''mutex-meet-tid-cluster12'' ''aget_comb.c'' ''--enable'' ''dbg.uncalled''
+        ''mutex-meet-tid-cluster12'' ''aget_comb.c''
         ''--enable'' ''allglobs'' ''--enable'' ''printstats'' ''--enable'' ''dbg.debug''
-        ''-v'' ''--enable'' ''dbg.print_dead_code'' ''--enable'' ''witness.yaml.enabled''
+        ''-v''  ''--enable'' ''witness.yaml.enabled''
         ''--set'' ''witness.yaml.path'' ''./aget_comb_traces_rel.yml'''
     task:
       input_files: