From 34404f0db938b954408154459a41c530023f55b0 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 22 Jun 2018 13:10:30 +0100 Subject: [PATCH] Set little_endian in the same way that boolbv_byte_extract already does Ensure that a valid id is set via PRECONDITION checks. --- src/solvers/flattening/boolbv_byte_extract.cpp | 3 +++ src/solvers/flattening/boolbv_byte_update.cpp | 12 ++++-------- src/solvers/flattening/flatten_byte_operators.cpp | 12 ++++-------- 3 files changed, 11 insertions(+), 16 deletions(-) diff --git a/src/solvers/flattening/boolbv_byte_extract.cpp b/src/solvers/flattening/boolbv_byte_extract.cpp index 86fd36231f9..29f2fd41904 100644 --- a/src/solvers/flattening/boolbv_byte_extract.cpp +++ b/src/solvers/flattening/boolbv_byte_extract.cpp @@ -100,6 +100,9 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr) const exprt &op=expr.op(); const exprt &offset=expr.offset(); + PRECONDITION( + expr.id() == ID_byte_extract_little_endian || + expr.id() == ID_byte_extract_big_endian); const bool little_endian = expr.id() == ID_byte_extract_little_endian; // first do op0 diff --git a/src/solvers/flattening/boolbv_byte_update.cpp b/src/solvers/flattening/boolbv_byte_update.cpp index 66b3cf68180..3dab1a8544e 100644 --- a/src/solvers/flattening/boolbv_byte_update.cpp +++ b/src/solvers/flattening/boolbv_byte_update.cpp @@ -25,14 +25,10 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr) const exprt &offset_expr=expr.offset(); const exprt &value=expr.value(); - bool little_endian; - - if(expr.id()==ID_byte_update_little_endian) - little_endian=true; - else if(expr.id()==ID_byte_update_big_endian) - little_endian=false; - else - UNREACHABLE; + PRECONDITION( + expr.id() == ID_byte_update_little_endian || + expr.id() == ID_byte_update_big_endian); + const bool little_endian = expr.id() == ID_byte_update_little_endian; bvt bv=convert_bv(op); diff --git a/src/solvers/flattening/flatten_byte_operators.cpp b/src/solvers/flattening/flatten_byte_operators.cpp index 2cc586c7c02..a96f28bcb8f 100644 --- a/src/solvers/flattening/flatten_byte_operators.cpp +++ b/src/solvers/flattening/flatten_byte_operators.cpp @@ -201,14 +201,10 @@ exprt flatten_byte_extract( assert(src.operands().size()==2); - bool little_endian; - - if(src.id()==ID_byte_extract_little_endian) - little_endian=true; - else if(src.id()==ID_byte_extract_big_endian) - little_endian=false; - else - UNREACHABLE; + PRECONDITION( + src.id() == ID_byte_extract_little_endian || + src.id() == ID_byte_extract_big_endian); + const bool little_endian = src.id() == ID_byte_extract_little_endian; // determine an upper bound of the number of bytes we might need exprt upper_bound=size_of_expr(src.type(), ns);