add __builtin_isnormal

Daniel Kroening · Daniel Kroening · commit 80e17f585b89 · 2018-05-22T15:14:09.000+01:00
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
@@ -2312,7 +2312,8 @@ exprt c_typecheck_baset::do_special_functions(
   }
   else if(identifier==CPROVER_PREFIX "isnormalf" ||
           identifier==CPROVER_PREFIX "isnormald" ||
-          identifier==CPROVER_PREFIX "isnormalld")
+          identifier==CPROVER_PREFIX "isnormalld" ||
+          identifier=="__builtin_isnormal")
   {
     if(expr.arguments().size()!=1)
     {

Original file line number	Diff line number	Diff line change
`@@ -2312,7 +2312,8 @@ exprt c_typecheck_baset::do_special_functions(`
`2312`	`2312`	`}`
`2313`	`2313`	`else if(identifier==CPROVER_PREFIX "isnormalf" \|\|`
`2314`	`2314`	`identifier==CPROVER_PREFIX "isnormald" \|\|`
`2315`		`- identifier==CPROVER_PREFIX "isnormalld")`
	`2315`	`+ identifier==CPROVER_PREFIX "isnormalld" \|\|`
	`2316`	`+ identifier=="__builtin_isnormal")`
`2316`	`2317`	`{`
`2317`	`2318`	`if(expr.arguments().size()!=1)`
`2318`	`2319`	`{`