interpreter.h

Go to the documentation of this file.

 
#pragma once
 
// Inc Library
#include "determinations.h"
 
// Inc Pure
#include "dbc.h"
#include "helper.h"
 
// Inc Medium
#include "error.h"
 
 
class Context;
class SOF;
 
 
class Interpreter : protected DbC {
 
  static Interpreter * instance_;  
  int startup_nof_ = -1;           
  Context * curctx_{};             
  struct PimplTime;                
  PimplTime * pimpltime_;          
  size_t odo_changes_ = 0;         
  std::string iif_{};                         
  SOF * outf_;                                
  bool verbose_ = false;                      
  bool odo_ = false;                          
  bool suppressaec_ = false;                  
  size_t odo_iterations_ = DET_MAXODO;        
  size_t maxopeelevel_ = 2;                   
  size_t realprecision_ = DET_REALPRECISION;  
  Interpreter();
 
 
  virtual ~Interpreter();
 
 
  void help();
 
 
  static std::string unescape( const std::string & p_s );
 
 
  void print( const char * p_line );
 
 
  void property_statistics();
 
 
  void status_statistics();
 
protected:
 
#ifndef DBC_IS_VOID
  bool invariant() const noexcept override {    /* LCOV_EXCL_START */
    if( pimpltime_ == nullptr )
      return false;
    if( outf_ == nullptr )
      return false;
    return true;
  }                                             /* LCOV_EXCL_STOP */
#endif
 
public:
 
  Interpreter( const Interpreter& ) = delete;
  Interpreter( Interpreter&& ) = delete;
  Interpreter& operator=( const Interpreter& ) = delete;
  Interpreter& operator=( Interpreter&& ) = delete;
 
public: /* accessor */
 
  static auto get() {
    if( !instance_ ) {
      instance_ = new (std::nothrow) Interpreter;
      if( instance_ == nullptr )
        panicExit( "memory" );                                              /* LCOV_EXCL_LINE */
    }
 
    DBC_POST( instance_ != nullptr );
    return instance_;
  }
 
 
  std::string getIif() const { return iif_; }
 
 
  int getStartup_nof() const { return startup_nof_; }
 
 
  bool getVerbose() const { return verbose_; }
 
 
  void setContext( Context * p_c ) { curctx_ = p_c; }
 
 
  void setSuppressAEC( bool p_saec ) { suppressaec_ = p_saec; }
 
 
  bool getSuppressAEC() const { return suppressaec_; }
 
 
  void setOdo( bool p_odo ) { odo_ = p_odo; }
 
 
  bool getOdo() const { return odo_; }
 
 
  size_t getOdoIterations() const { return odo_iterations_; }
 
 
  size_t getMaxopeelevel() const { return maxopeelevel_; }
 
 
  size_t getRealprecision() const { return realprecision_; }
 
 
  void setRealprecision( size_t p_prec ) { realprecision_ = p_prec; }
 
public: /* other */
 
  void processLeonLine( std::string & p_line, Context & k );
 
 
  void print( const std::string & p_line );
 
 
  static void addchanges( size_t p_allchanges ) {
    get()->odo_changes_ += p_allchanges;
  }
 
 
  static void shutdown();
 
 
  void startup( int p_argc, char * p_argv[] );
 
 
  __int128 msec() const;
 
 
  static void leak_statistics( bool p_force, const std::string & p_fname, int p_nof );
 
 
  void snap();
 
};