1#ifndef ROSE_BinaryAnalysis_InstructionSemantics_BaseSemantics_SValue_H 
    2#define ROSE_BinaryAnalysis_InstructionSemantics_BaseSemantics_SValue_H 
    3#include <featureTests.h> 
    4#ifdef ROSE_ENABLE_BINARY_ANALYSIS 
    6#include <Rose/BinaryAnalysis/BasicTypes.h> 
    7#include <Combinatorics.h>                               
    9#include <Sawyer/SharedObject.h> 
   10#include <Sawyer/SmallObject.h> 
   12#ifdef ROSE_ENABLE_BOOST_SERIALIZATION 
   13#include <boost/serialization/access.hpp> 
   14#include <boost/serialization/export.hpp> 
   15#include <boost/serialization/nvp.hpp> 
   19namespace BinaryAnalysis {
 
   20namespace InstructionSemantics {
 
   51#ifdef ROSE_ENABLE_BOOST_SERIALIZATION 
   53    friend class boost::serialization::access;
 
   56    void serialize(S &s, 
const unsigned ) {
 
   57        s & BOOST_SERIALIZATION_NVP(width);
 
   65    explicit SValue(
size_t nbits);                      
 
  249    virtual 
void hash(Combinatorics::Hasher&) const = 0;
 
  270        void print(std::ostream&) 
const;
 
 
 
  319std::ostream& operator<<(std::ostream&, 
const SValue&);
 
  327#ifdef ROSE_ENABLE_BOOST_SERIALIZATION 
Base class for semantic values.
 
Sawyer::Optional< uint64_t > toUnsigned() const
Converts a concrete value to a native unsigned integer.
 
void print(std::ostream &) const
Print a value to a stream using default format.
 
virtual Sawyer::Optional< SValuePtr > createOptionalMerge(const SValuePtr &other, const MergerPtr &merger, const SmtSolverPtr &solver) const =0
Possibly create a new value by merging two existing values.
 
virtual bool must_equal(const SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const =0
Virtual API.
 
virtual void set_width(size_t nbits)
Virtual API.
 
virtual void set_comment(const std::string &) const
Some subclasses support the ability to add comments to values.
 
WithFormatter with_format(Formatter &)
Used for printing values with formatting.
 
virtual size_t get_width() const
Virtual API.
 
std::string comment() const
Property: Comment.
 
SValuePtr createMerged(const SValuePtr &other, const MergerPtr &, const SmtSolverPtr &) const
Create a new value by merging two existing values.
 
virtual bool may_equal(const SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const =0
Virtual API.
 
virtual SValuePtr number_(size_t nbits, uint64_t number) const =0
Create a new concrete semantic value.
 
virtual uint64_t get_number() const =0
Virtual API.
 
WithFormatter operator+(Formatter &)
Used for printing values with formatting.
 
WithFormatter operator+(const std::string &linePrefix)
Used for printing values with formatting.
 
std::string toString() const
Render this symbolic expression as a string.
 
virtual SValuePtr boolean_(bool value) const
Create a new, Boolean value.
 
virtual SValuePtr undefined_(size_t nbits) const =0
Create a new undefined semantic value.
 
virtual bool isBottom() const =0
Determines whether a value is a data-flow bottom.
 
virtual SValuePtr unspecified_(size_t nbits) const =0
Create a new unspecified semantic value.
 
bool mayEqual(const SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const
Tests two values for possible equality.
 
virtual std::string get_comment() const
Some subclasses support the ability to add comments to values.
 
bool isFalse() const
Returns true if concrete zero.
 
virtual bool is_number() const =0
Virtual API.
 
bool isTrue() const
Returns true if concrete non-zero.
 
virtual SValuePtr copy(size_t new_width=0) const =0
Create a new value from an existing value, changing the width if new_width is non-zero.
 
bool mustEqual(const SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const
Tests two values for equality.
 
Sawyer::Optional< int64_t > toSigned() const
Converts a concrete value to a native signed integer.
 
bool isConcrete() const
Determines if the value is a concrete number.
 
virtual SValuePtr bottom_(size_t nBits) const =0
Data-flow bottom value.
 
size_t nBits() const
Property: value width.
 
Holds a value or nothing.
 
Creates SharedPointer from this.
 
Base class for reference counted objects.
 
Base classes for instruction semantics.
 
Sawyer::SharedPointer< SValue > SValuePtr
Shared-ownership pointer to a semantic value in any domain.
 
std::shared_ptr< SmtSolver > SmtSolverPtr
Reference counting pointer.