CHC support #183
CHC support #183
Conversation
There was a problem hiding this comment.
All in all, I think this is a very nice work. I left some minor comments. The only major thing missing (and we do not set a good example on this matter 😅) is to add the copyright to the new source files you created.
See an example here. Please do update the year though.
| private static SmtLibTypeTransformer typeTransformer = new GenericSmtLibTypeTransformer(null); | ||
| private static SmtLibTermTransformer termTransformer = new GenericSmtLibTermTransformer(initialSymbolTable); | ||
| private static CharStream charStream; | ||
|
|
There was a problem hiding this comment.
Missing private constructor.
| private ChcUtils() {} | |
| @@ -83,7 +83,7 @@ public class XcfaPassManager { | |||
| // new AssignmentChainRemoval(), | |||
| // new NoReadVarRemovalPass(), | |||
| // new GlobalVarsToStoreLoad(), | |||
| new UnusedVarRemovalPass(), | |||
| // new UnusedVarRemovalPass(), | |||
There was a problem hiding this comment.
This is a global modification that will also affect C source codes. My questions are:
- Why was this modification needed?
- If the change is needed for CHCs, can we somehow make XcfaPassManager configurable to include the pass for C codes and remove it for CHCs?
There was a problem hiding this comment.
The modification was necessary because the pass removed variables that would've been necessary for correct verification, resulting in incorrect answers. I added methods to XcfaPassManager that can remove passes and moved the removal to CHC handling part of XcfaCli.
I implemented the requested changes.
I added the license text to all |
There was a problem hiding this comment.
Thank you for the changes! I think this can be merged @leventeBajczi .
This is the result of my BSc degree project: a CHC frontend implemented in Theta. It can be enabled with the
--chcflag, and different transformation methods can be chosen using the--chc-transformation FORWARD/BACKWARDflag. See the documentation for details.