cprover
|
SMT Backend. More...
#include "smt2_conv.h"
#include <cassert>
#include <util/arith_tools.h>
#include <util/base_type.h>
#include <util/c_types.h>
#include <util/expr_util.h>
#include <util/fixedbv.h>
#include <util/ieee_float.h>
#include <util/invariant.h>
#include <util/pointer_offset_size.h>
#include <util/std_types.h>
#include <util/std_expr.h>
#include <util/string2int.h>
#include <ansi-c/string_constant.h>
#include <langapi/language_util.h>
#include <solvers/flattening/boolbv_width.h>
#include <solvers/flattening/flatten_byte_operators.h>
#include <solvers/flattening/c_bit_field_replacement_type.h>
#include <solvers/floatbv/float_bv.h>
Go to the source code of this file.
Macros | |
#define | PARSERERROR(S) throw S |
#define | INVALIDEXPR(S) throw "Invalid expression: " S |
#define | UNEXPECTEDCASE(S) throw "Unexpected case: " S |
#define | SMT2_TODO(S) throw "TODO: " S |
SMT Backend.
Definition in file smt2_conv.cpp.
#define INVALIDEXPR | ( | S | ) | throw "Invalid expression: " S |
Definition at line 42 of file smt2_conv.cpp.
Referenced by smt2_convt::convert_address_of_rec(), smt2_convt::convert_byte_update(), smt2_convt::convert_expr(), smt2_convt::convert_member(), smt2_convt::convert_minus(), smt2_convt::convert_plus(), smt2_convt::convert_rounding_mode_FPA(), smt2_convt::convert_type(), smt2_convt::convert_union(), smt2_convt::convert_with(), smt2_convt::find_symbols_rec(), smt2_convt::flatten2bv(), smt2_convt::flatten_array(), and smt2_convt::unflatten().
#define PARSERERROR | ( | S | ) | throw S |
Definition at line 39 of file smt2_conv.cpp.
Referenced by smt2_convt::parse_literal().
#define SMT2_TODO | ( | S | ) | throw "TODO: " S |
Definition at line 49 of file smt2_conv.cpp.
Referenced by smt2_convt::convert_expr(), smt2_convt::convert_floatbv_plus(), smt2_convt::convert_index(), smt2_convt::convert_minus(), smt2_convt::convert_typecast(), smt2_convt::convert_update(), and smt2_convt::convert_with().
#define UNEXPECTEDCASE | ( | S | ) | throw "Unexpected case: " S |
Definition at line 46 of file smt2_conv.cpp.
Referenced by smt2_convt::convert_address_of_rec(), smt2_convt::convert_byte_update(), smt2_convt::convert_constant(), smt2_convt::convert_div(), smt2_convt::convert_expr(), smt2_convt::convert_floatbv_plus(), smt2_convt::convert_floatbv_typecast(), smt2_convt::convert_index(), smt2_convt::convert_member(), smt2_convt::convert_minus(), smt2_convt::convert_mod(), smt2_convt::convert_mult(), smt2_convt::convert_plus(), smt2_convt::convert_relation(), smt2_convt::convert_type(), smt2_convt::convert_typecast(), smt2_convt::convert_with(), and smt2_convt::parse_literal().