Merge pull request #1885 from goblint/svcomp-conf-explicit-malloc-fail

sim642 · web-flow · commit c286cce44649 · 2025-12-01T12:40:58.000+02:00
Make `sem.malloc.*` explicit in svcomp confs
diff --git a/conf/svcomp-ghost.json b/conf/svcomp-ghost.json
@@ -109,6 +109,10 @@
     },
     "null-pointer": {
       "dereference": "assume_none"
+    },
+    "malloc": {
+      "fail": false,
+      "zero": "pointer"
     }
   },
   "witness": {
diff --git a/conf/svcomp-yaml-validate.json b/conf/svcomp-yaml-validate.json
@@ -89,6 +89,10 @@
     },
     "null-pointer": {
       "dereference": "assume_none"
+    },
+    "malloc": {
+      "fail": false,
+      "zero": "pointer"
     }
   }
 }
diff --git a/conf/svcomp-yaml.json b/conf/svcomp-yaml.json
@@ -106,6 +106,10 @@
     },
     "null-pointer": {
       "dereference": "assume_none"
+    },
+    "malloc": {
+      "fail": false,
+      "zero": "pointer"
     }
   }
 }
diff --git a/conf/svcomp21.json b/conf/svcomp21.json
@@ -61,6 +61,10 @@
     },
     "null-pointer": {
       "dereference": "assume_none"
+    },
+    "malloc": {
+      "fail": false,
+      "zero": "pointer"
     }
   }
 }
diff --git a/conf/svcomp22.json b/conf/svcomp22.json
@@ -64,6 +64,10 @@
     },
     "null-pointer": {
       "dereference": "assume_none"
+    },
+    "malloc": {
+      "fail": false,
+      "zero": "pointer"
     }
   }
 }
diff --git a/conf/svcomp23.json b/conf/svcomp23.json
@@ -87,6 +87,10 @@
     },
     "null-pointer": {
       "dereference": "assume_none"
+    },
+    "malloc": {
+      "fail": false,
+      "zero": "pointer"
     }
   }
 }
diff --git a/conf/svcomp24-validate.json b/conf/svcomp24-validate.json
@@ -109,6 +109,10 @@
     },
     "null-pointer": {
       "dereference": "assume_none"
+    },
+    "malloc": {
+      "fail": false,
+      "zero": "pointer"
     }
   },
   "witness": {
diff --git a/conf/svcomp24.json b/conf/svcomp24.json
@@ -105,6 +105,10 @@
     },
     "null-pointer": {
       "dereference": "assume_none"
+    },
+    "malloc": {
+      "fail": false,
+      "zero": "pointer"
     }
   },
   "witness": {
diff --git a/conf/svcomp25-validate.json b/conf/svcomp25-validate.json
@@ -90,6 +90,10 @@
     },
     "null-pointer": {
       "dereference": "assume_none"
+    },
+    "malloc": {
+      "fail": false,
+      "zero": "pointer"
     }
   },
   "witness": {
diff --git a/conf/svcomp25.json b/conf/svcomp25.json
@@ -86,6 +86,10 @@
     },
     "null-pointer": {
       "dereference": "assume_none"
+    },
+    "malloc": {
+      "fail": false,
+      "zero": "pointer"
     }
   },
   "witness": {
diff --git a/conf/svcomp26/common.json b/conf/svcomp26/common.json
@@ -36,6 +36,10 @@
     },
     "null-pointer": {
       "dereference": "assume_none"
+    },
+    "malloc": {
+      "fail": false,
+      "zero": "either"
     }
   },
   "witness": {
diff --git a/conf/svcomp2var.json b/conf/svcomp2var.json
@@ -104,6 +104,10 @@
     },
     "null-pointer": {
       "dereference": "assume_none"
+    },
+    "malloc": {
+      "fail": false,
+      "zero": "pointer"
     }
   },
   "witness": {

Original file line number	Diff line number	Diff line change
`@@ -89,6 +89,10 @@`
`89`	`89`	`},`
`90`	`90`	`"null-pointer": {`
`91`	`91`	`"dereference": "assume_none"`
	`92`	`+ },`
	`93`	`+ "malloc": {`
	`94`	`+ "fail": false,`
	`95`	`+ "zero": "pointer"`
`92`	`96`	`}`
`93`	`97`	`}`
`94`	`98`	`}`
Original file line number	Diff line number	Diff line change
`@@ -106,6 +106,10 @@`
`106`	`106`	`},`
`107`	`107`	`"null-pointer": {`
`108`	`108`	`"dereference": "assume_none"`
	`109`	`+ },`
	`110`	`+ "malloc": {`
	`111`	`+ "fail": false,`
	`112`	`+ "zero": "pointer"`
`109`	`113`	`}`
`110`	`114`	`}`
`111`	`115`	`}`
Original file line number	Diff line number	Diff line change
`@@ -61,6 +61,10 @@`
`61`	`61`	`},`
`62`	`62`	`"null-pointer": {`
`63`	`63`	`"dereference": "assume_none"`
	`64`	`+ },`
	`65`	`+ "malloc": {`
	`66`	`+ "fail": false,`
	`67`	`+ "zero": "pointer"`
`64`	`68`	`}`
`65`	`69`	`}`
`66`	`70`	`}`
Original file line number	Diff line number	Diff line change
`@@ -64,6 +64,10 @@`
`64`	`64`	`},`
`65`	`65`	`"null-pointer": {`
`66`	`66`	`"dereference": "assume_none"`
	`67`	`+ },`
	`68`	`+ "malloc": {`
	`69`	`+ "fail": false,`
	`70`	`+ "zero": "pointer"`
`67`	`71`	`}`
`68`	`72`	`}`
`69`	`73`	`}`
Original file line number	Diff line number	Diff line change
`@@ -87,6 +87,10 @@`
`87`	`87`	`},`
`88`	`88`	`"null-pointer": {`
`89`	`89`	`"dereference": "assume_none"`
	`90`	`+ },`
	`91`	`+ "malloc": {`
	`92`	`+ "fail": false,`
	`93`	`+ "zero": "pointer"`
`90`	`94`	`}`
`91`	`95`	`}`
`92`	`96`	`}`