From 298dbfb08cc57c3d554b8c34f3fae6c0ff58440b Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Fri, 16 Dec 2016 13:57:53 +0000 Subject: [PATCH 1/5] Fix _Bool XML output --- src/util/xml_expr.cpp | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/util/xml_expr.cpp b/src/util/xml_expr.cpp index 11a4ac1d2c6..adf13167046 100644 --- a/src/util/xml_expr.cpp +++ b/src/util/xml_expr.cpp @@ -263,6 +263,15 @@ xmlt xml( result.set_attribute("binary", expr.is_true()?"1":"0"); result.data=expr.is_true()?"TRUE":"FALSE"; } + else if(type.id()==ID_c_bool) + { + result.name="integer"; + result.set_attribute("c_type", "_Bool"); + result.set_attribute("binary", expr.get_string(ID_value)); + mp_integer b; + to_integer(to_constant_expr(expr), b); + result.data=integer2string(b); + } else { result.name="unknown"; From a1741459f850868c43532074ebe24abf3f21c1ea Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Fri, 16 Dec 2016 14:12:17 +0000 Subject: [PATCH 2/5] Fixed cpplint warnings --- src/util/xml_expr.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/util/xml_expr.cpp b/src/util/xml_expr.cpp index adf13167046..6eb49b8261b 100644 --- a/src/util/xml_expr.cpp +++ b/src/util/xml_expr.cpp @@ -126,7 +126,8 @@ xmlt xml( { result.name="vector"; result.new_element("subtype").new_element()=xml(type.subtype(), ns); - result.new_element("size").new_element()=xml(to_vector_type(type).size(), ns); + result.new_element("size").new_element()= + xml(to_vector_type(type).size(), ns); } else if(type.id()==ID_struct) { @@ -318,7 +319,8 @@ xmlt xml( xmlt &e=result.new_element("member"); e.new_element(xml(expr.op0(), ns)); - e.set_attribute("member_name", + e.set_attribute( + "member_name", id2string(to_union_expr(expr).get_component_name())); } else From 70b89c326c9db879a587f66d7a223953fa785582 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 7 Jan 2017 18:05:31 +0100 Subject: [PATCH 3/5] Ensure that _Bool parameter has only 0 or 1 values --- src/ansi-c/ansi_c_entry_point.cpp | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index 1acfb7d4459..1e7f8922262 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/src/ansi-c/ansi_c_entry_point.cpp @@ -74,6 +74,18 @@ exprt::operandst build_function_environment( init_code.add(decl); + // nondet init for _Bool + if(decl.symbol().type().id()==ID_c_bool) + { + code_assignt assign( + decl.symbol(), + typecast_exprt( + side_effect_expr_nondett(bool_typet()), + decl.symbol().type())); + + init_code.move_to_operands(assign); + } + codet input(ID_input); input.operands().resize(2); From 2461ecf80e1a011c09f0f57d2065f1741d61717b Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 7 Jan 2017 18:06:17 +0100 Subject: [PATCH 4/5] Regression test for _Bool parameter --- regression/cbmc/c99_Bool/main.c | 11 +++++++++++ regression/cbmc/c99_Bool/test.desc | 8 ++++++++ 2 files changed, 19 insertions(+) create mode 100644 regression/cbmc/c99_Bool/main.c create mode 100644 regression/cbmc/c99_Bool/test.desc diff --git a/regression/cbmc/c99_Bool/main.c b/regression/cbmc/c99_Bool/main.c new file mode 100644 index 00000000000..532ff6e2efe --- /dev/null +++ b/regression/cbmc/c99_Bool/main.c @@ -0,0 +1,11 @@ +#include + +void foo(_Bool y) +{ + int x; + if(y) + { + x=(int)y; + assert(x==1); + } +} diff --git a/regression/cbmc/c99_Bool/test.desc b/regression/cbmc/c99_Bool/test.desc new file mode 100644 index 00000000000..a454c448ed0 --- /dev/null +++ b/regression/cbmc/c99_Bool/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--function foo +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring From aaa5348ca3971c471bbf7a46bbbd361bb6ee09c8 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 7 Jan 2017 22:41:42 +0100 Subject: [PATCH 5/5] Fix _Bool JSON output --- src/util/json_expr.cpp | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/util/json_expr.cpp b/src/util/json_expr.cpp index 7fd4f265f3f..727449340dc 100644 --- a/src/util/json_expr.cpp +++ b/src/util/json_expr.cpp @@ -266,6 +266,15 @@ json_objectt json( result["binary"]=json_stringt(expr.is_true()?"1":"0"); result["data"]=jsont::json_boolean(expr.is_true()); } + else if(type.id()==ID_c_bool) + { + result["name"]=json_stringt("integer"); + result["c_type"]=json_stringt("_Bool"); + result["binary"]=json_stringt(expr.get_string(ID_value)); + mp_integer b; + to_integer(to_constant_expr(expr), b); + result["data"]=json_stringt(integer2string(b)); + } else { result["name"]=json_stringt("unknown");