summaryrefslogtreecommitdiff
path: root/proofs/lfsc_checker/code.h
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/lfsc_checker/code.h')
-rw-r--r--proofs/lfsc_checker/code.h15
1 files changed, 15 insertions, 0 deletions
diff --git a/proofs/lfsc_checker/code.h b/proofs/lfsc_checker/code.h
new file mode 100644
index 000000000..9d00a6378
--- /dev/null
+++ b/proofs/lfsc_checker/code.h
@@ -0,0 +1,15 @@
+#ifndef SC2_CODE_H
+#define SC2_CODE_H
+
+#include "expr.h"
+
+Expr *read_code();
+Expr *check_code(Expr *); // compute the type for the given code
+Expr *run_code(Expr *);
+
+int read_index();
+
+extern bool dbg_prog;
+extern bool run_scc;
+
+#endif
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback