viper-admin
commented
6 years ago - Rewrite JSON generation for SymbExLogReport using spray-json.
- Remove non-needed (and wrong) import.
- Fix typo.
- Implement term writer for path condtitions in SymbExLog report.
- Make trace report more generic.
- Check the actual config before writing the trace report.
- Minor tweaks.
- Add structured translation to JSON for heaps.
- Add return sort to applicables in SymbExLogReport.
- Add structured translation to JSON for store.
- Translate the last SMT query to JSON as a proper term.
- Translate sorts to structured JSON objects in SymbExLogReport.
- Change "distinct" contents to symbols as they are not terms.
- Translate sorts to structured objects in the store as well.
- Experimental model generation via Alloy.
- Send back Alloy instance in JSON format.
- Report empty collections in Alloy instance.
- Do not transform Combines with unit.
- Add position to method calls in SymbExLog.
- Remove unused SymbExLog records.
- Add axioms to Symbolic Execution Trace report.
- Report inverse functions for quantified chunks.
- Allow passing the solver backend in Alloy request.
- Report recorded macros in the SymbExLog
- Cleanup state translation in SymbExLog.
- Also report atoms inside each Alloy signature.
- Return functions postconditions in execution trace report.
- Make sure the Alloy configuration corresponds to that of the GUI.
- Align with default options in the GUI.