add __builtin_isnormal

Daniel Kroening · Daniel Kroening · commit a69c60392241 · 2018-05-22T15:23:36.000+01:00
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
@@ -2376,9 +2376,10 @@ exprt c_typecheck_baset::do_special_functions(
         from_integer(1, expr.type())),
       from_integer(0, expr.type()));
   }
-  else if(identifier==CPROVER_PREFIX "isnormalf" ||
-          identifier==CPROVER_PREFIX "isnormald" ||
-          identifier==CPROVER_PREFIX "isnormalld")
+  else if(identifier == CPROVER_PREFIX "isnormalf" ||
+          identifier == CPROVER_PREFIX "isnormald" ||
+          identifier == CPROVER_PREFIX "isnormalld" ||
+          identifier == "__builtin_isnormal")
   {
     if(expr.arguments().size()!=1)
     {

Original file line number	Diff line number	Diff line change
`@@ -2376,9 +2376,10 @@ exprt c_typecheck_baset::do_special_functions(`
`2376`	`2376`	`from_integer(1, expr.type())),`
`2377`	`2377`	`from_integer(0, expr.type()));`
`2378`	`2378`	`}`
`2379`		`- else if(identifier==CPROVER_PREFIX "isnormalf" \|\|`
`2380`		`- identifier==CPROVER_PREFIX "isnormald" \|\|`
`2381`		`- identifier==CPROVER_PREFIX "isnormalld")`
	`2379`	`+ else if(identifier == CPROVER_PREFIX "isnormalf" \|\|`
	`2380`	`+ identifier == CPROVER_PREFIX "isnormald" \|\|`
	`2381`	`+ identifier == CPROVER_PREFIX "isnormalld" \|\|`
	`2382`	`+ identifier == "__builtin_isnormal")`
`2382`	`2383`	`{`
`2383`	`2384`	`if(expr.arguments().size()!=1)`
`2384`	`2385`	`{`