Changes between Version 4 and Version 5 of CIVL-C


Ignore:
Timestamp:
07/22/22 11:19:10 (4 years ago)
Author:
Alex Wilton
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • CIVL-C

    v4 v5  
    1919* If `-showProgram` enabled and we get an error, then print AST before exiting.
    2020* Be able to specify hardware environment to verify under like ints are 32 bits, floats are 32 bits, big-endian vs little-endian, etc.
     21* Increased emphasis on static analysis.
    2122
    2223=== Design
     
    2526* The ability to associate static traits to ASTs like "no for loops" or "side effect free", etc.
    2627* Be able to easily loop over AST nodes of a certain type (in program order). Maybe just support visitor pattern.
     28* Make it easy to create custom static analyses, especially fundamental ones like dataflow analysis
    2729* CIVL-C language and library must be completely well-defined and documented.
    2830* CIVL-IR must be completely well-defined and documented.
     31* Remove StatePredicate abstraction and just check for deadlocks directly in the enabler.
    2932* Break up Evaluator by removing big switch:
    3033  * Have "Executable Expression" and "Executable Statement"-type classes which have an evaluate method and extend the syntactic Expression and Statement classes.