Merge pull request #3217 from romainbrenguier/bugfix/is_bmp_code_point

romainbrenguier · web-flow · commit ebce18aae3cd · 2018-10-23T10:03:08.000+01:00
Fix is_bmp_code_point
diff --git a/jbmc/src/java_bytecode/character_refine_preprocess.cpp b/jbmc/src/java_bytecode/character_refine_preprocess.cpp
@@ -402,8 +402,9 @@ codet character_refine_preprocesst::convert_is_alphabetic(
 exprt character_refine_preprocesst::expr_of_is_bmp_code_point(
   const exprt &chr, const typet &type)
 {
-  binary_relation_exprt is_bmp(chr, ID_le, from_integer(0xFFFF, chr.type()));
-  return is_bmp;
+  return and_exprt(
+    binary_relation_exprt(chr, ID_le, from_integer(0xFFFF, chr.type())),
+    binary_relation_exprt(chr, ID_ge, from_integer(0, chr.type())));
 }
 
 /// Converts function call to an assignment of an expression corresponding to

Original file line number	Diff line number	Diff line change
`@@ -402,8 +402,9 @@ codet character_refine_preprocesst::convert_is_alphabetic(`
`402`	`402`	`exprt character_refine_preprocesst::expr_of_is_bmp_code_point(`
`403`	`403`	`const exprt &chr, const typet &type)`
`404`	`404`	`{`
`405`		`- binary_relation_exprt is_bmp(chr, ID_le, from_integer(0xFFFF, chr.type()));`
`406`		`- return is_bmp;`
	`405`	`+ return and_exprt(`
	`406`	`+ binary_relation_exprt(chr, ID_le, from_integer(0xFFFF, chr.type())),`
	`407`	`+ binary_relation_exprt(chr, ID_ge, from_integer(0, chr.type())));`
`407`	`408`	`}`
`408`	`409`
`409`	`410`	`/// Converts function call to an assignment of an expression corresponding to`