diff options
Diffstat (limited to 'proofs/lfsc_checker/check.h')
-rw-r--r-- | proofs/lfsc_checker/check.h | 167 |
1 files changed, 0 insertions, 167 deletions
diff --git a/proofs/lfsc_checker/check.h b/proofs/lfsc_checker/check.h deleted file mode 100644 index 756bb4db6..000000000 --- a/proofs/lfsc_checker/check.h +++ /dev/null @@ -1,167 +0,0 @@ -#ifndef SC2_CHECK_H -#define SC2_CHECK_H - -#include "expr.h" -#include "trie.h" - -#ifdef _MSC_VER -#include <hash_map> -#include <stdio.h> -#else -#include <ext/hash_map> -#endif - -#include <stack> -#include <string> -#include <map> - -// see the help message in main.cpp for explanation -typedef struct args { - std::vector<std::string> files; - bool show_runs; - bool no_tail_calls; - bool compile_scc; - bool compile_scc_debug; - bool run_scc; - bool use_nested_app; - bool compile_lib; -} args; - -extern int check_time; - -class sccwriter; -class libwriter; - -void init(); - -void check_file(const char *_filename, args a, sccwriter* scw = NULL, libwriter* lw = NULL); - -void cleanup(); - -extern char our_getc_c; - -void report_error(const std::string &); - -extern int linenum; -extern int colnum; -extern const char *filename; -extern FILE *curfile; - -inline void our_ungetc(char c) { - if (our_getc_c != 0) - report_error("Internal error: our_ungetc buffer full"); - our_getc_c = c; - if (c == '\n') { - linenum--; - colnum=-1; - } - else - colnum--; -} - -inline char our_getc() { - char c; - if (our_getc_c > 0) { - c = our_getc_c; - our_getc_c = 0; - } - else{ -#ifndef __linux__ - c = fgetc(curfile); -#else - c = fgetc_unlocked(curfile); -#endif - } - switch(c) { - case '\n': - linenum++; -#ifdef DEBUG_LINES - std::cout << "line " << linenum << "." << std::endl; -#endif - colnum = 1; - break; - case char(EOF): - break; - default: - colnum++; - } - - return c; -} - -// return the next character that is not whitespace -inline char non_ws() { - char c; - while(isspace(c = our_getc())); - if (c == ';') { - // comment to end of line - while((c = our_getc()) != '\n' && c != char(EOF)); - return non_ws(); - } - return c; -} - -inline void eat_char(char expected) { - if (non_ws() != expected) { - char tmp[80]; - sprintf(tmp,"Expecting a \'%c\'",expected); - report_error(tmp); - } -} - -extern int IDBUF_LEN; -extern char idbuf[]; - -inline const char *prefix_id() { - int i = 0; - char c = idbuf[i++] = non_ws(); - while (!isspace(c) && c != '(' && c != ')' && c != char(EOF)) { - if (i == IDBUF_LEN) - report_error("Identifier is too long"); - - idbuf[i++] = c = our_getc(); - } - our_ungetc(c); - idbuf[i-1] = 0; - return idbuf; -} - -#ifdef _MSC_VER -typedef std::hash_map<std::string, Expr *> symmap; -typedef std::hash_map<std::string, SymExpr *> symmap2; -#else -typedef __gnu_cxx::hash_map<std::string, Expr *> symmap; -typedef __gnu_cxx::hash_map<std::string, SymExpr *> symmap2; -#endif -extern symmap2 progs; -extern std::vector< Expr* > ascHoles; - -#ifdef USE_HASH_MAPS -extern symmap symbols; -extern symmap symbol_types; -#else -extern Trie<std::pair<Expr *, Expr *> > *symbols; -#endif - -extern std::map<SymExpr*, int > mark_map; - -extern std::vector< std::pair< std::string, std::pair<Expr *, Expr *> > > local_sym_names; - -#ifndef _MSC_VER -namespace __gnu_cxx -{ - template<> struct hash< std::string > - { - size_t operator()( const std::string& x ) const - { - return hash< const char* >()( x.c_str() ); - } - }; -} -#endif - -extern Expr *statMpz; -extern Expr *statMpq; -extern Expr *statType; - -#endif |