1 files changed, 167 insertions, 0 deletions
diff --git a/proofs/lfsc_checker/check.h b/proofs/lfsc_checker/check.h
new file mode 100644
index 000000000..a70599b0f
--- /dev/null
+++ b/proofs/lfsc_checker/check.h
@@ -0,0 +1,167 @@
+#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 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 != 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 != 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