diff --git a/src/tricera/concurrency/CCReader.scala b/src/tricera/concurrency/CCReader.scala index beef2b0..948e83f 100644 --- a/src/tricera/concurrency/CCReader.scala +++ b/src/tricera/concurrency/CCReader.scala @@ -163,6 +163,32 @@ object CCReader { } //////////////////////////////////////////////////////////////////////////////// +trait ProgramBackTranslator +object DummyBackTranslator extends ProgramBackTranslator + +trait CCASTPreprocessor { + def translate(prog : Program) : (Program, ProgramBackTranslator) +} + +// 0) Compile visitors in ccparser, currently only the ones in Absyn are compiled. +// Look up Princess SMT-LIB parser, which had the same problem which is now fixed. +// -- Do the same for the ACSL parser as well. +// 1) Do type-inference in first pass (could be separate visitors or the same) +// Extend EVar class and create a new AST after the pass. +// We could also extend the grammar, e.g., +// EvarWithType. Exp17 ::= "$$" CIdent ":" [Declaration_specifier] "##"; +// This has the advantage of making all generated visitors know about this. +// Challenge: +// -- ComposVisitor will revert back to the old AST -- won't know about +// the augmented classes. +// -- Solution: Extend ComposVisitor so that it knows about the new types. +// 2) Detect pointer types, rewrite call sites. +// -- At each call, i) if it is a stack pointer rewrite using a new function +// name and global variables. +// 3) Create copies of functions for stack & heap pointers. +// 4) Add back-translators. +// 5) Stretch goal: output contracts in ACSL AST, and implement preprocessors & +// back-translators using this. class CCReader private (prog : Program, entryFunction : String,