Support OpenBSD's __assert2

tautschnig · tautschnig · commit e8505bd604ba · 2023-12-18T12:17:51.000Z
This has the same usage as __assert_func in newlib. See https://github.com/openbsd/src/blob/master/include/assert.h.
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
@@ -1221,9 +1221,10 @@ void goto_convertt::do_function_call_symbol(
     dest.add(goto_programt::make_assertion(false_exprt(), annotated_location));
     // we ignore any LHS
   }
-  else if(identifier=="__assert_func")
+  else if(identifier == "__assert_func" || identifier == "__assert2")
   {
     // __assert_func is newlib (used by, e.g., cygwin)
+    // __assert2 is OpenBSD
     // These take four arguments:
     // "file.c", line, __func__, "expression"
     if(arguments.size()!=4)

Original file line number	Diff line number	Diff line change
`@@ -1221,9 +1221,10 @@ void goto_convertt::do_function_call_symbol(`
`1221`	`1221`	`dest.add(goto_programt::make_assertion(false_exprt(), annotated_location));`
`1222`	`1222`	`// we ignore any LHS`
`1223`	`1223`	`}`
`1224`		`- else if(identifier=="__assert_func")`
	`1224`	`+ else if(identifier == "__assert_func" \|\| identifier == "__assert2")`
`1225`	`1225`	`{`
`1226`	`1226`	`// __assert_func is newlib (used by, e.g., cygwin)`
	`1227`	`+ // __assert2 is OpenBSD`
`1227`	`1228`	`// These take four arguments:`
`1228`	`1229`	`// "file.c", line, __func__, "expression"`
`1229`	`1230`	`if(arguments.size()!=4)`