viperproject/viperserver

Debugger support

viper-admin opened this issue · 2 comments

viper-admin commented

Pull request 🔀 created by bitbucket user aurecchia on 2018-09-09 18:26
Last updated on 2019-04-23 16:42
Original Bitbucket pull request id: 7

Participants:

  • @aterga (reviewer)
  • bitbucket user aurecchia

Source: fb6266b on branch aurecchia/viperserver/debugger-support
Destination: fdad473 on branch master
Marge commit: 636c96f

State: MERGED

  • 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.
viper-admin commented

@aterga commented on 2018-09-10 09:05

Outdated location: line 283 of src/main/scala/viper/server/VerificationWorker.scala

Not the right time stamp.

viper-admin commented

Bitbucket user aurecchia commented on 2018-09-10 09:46

Outdated location: src/main/scala/viper/server/VerificationWorker.scala

Not the right time stamp.

Which one would be the correct one?