add __builtin_isnormal

Daniel Kroening · Daniel Kroening · commit f876018dd6da · 2018-05-22T14:42:54.000+01:00
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
@@ -2318,7 +2318,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
`@@ -2318,7 +2318,8 @@ exprt c_typecheck_baset::do_special_functions(`
`2318`	`2318`	`}`
`2319`	`2319`	`else if(identifier==CPROVER_PREFIX "isnormalf" \|\|`
`2320`	`2320`	`identifier==CPROVER_PREFIX "isnormald" \|\|`
`2321`		`- identifier==CPROVER_PREFIX "isnormalld")`
	`2321`	`+ identifier==CPROVER_PREFIX "isnormalld" \|\|`
	`2322`	`+ identifier=="__builtin_isnormal")`
`2322`	`2323`	`{`
`2323`	`2324`	`if(expr.arguments().size()!=1)`
`2324`	`2325`	`{`