Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

heapster-saw: Export block entry-point and implication error information for IDE ingestion #1442

Open
wants to merge 34 commits into
base: master
Choose a base branch
from
Open
Changes from 1 commit
Commits
Show all changes
34 commits
Select commit Hold shift + click to select a range
3a9c13b
add basic IDE logging, start error cleanup
Jun 28, 2021
bfd0566
clean up additional implication errors
Jun 28, 2021
49f72e4
add structure to stmt fail in line with impl fail
Jun 29, 2021
716a2e1
redesign error message types, pipe through to log
Jul 7, 2021
9283f0e
fix default heapster environments missing ioref
Jul 8, 2021
1e427a4
carry more information through on most common implication error
Jul 9, 2021
059ab7b
Merge branch 'heapster-ide-info' of github.com:GaloisInc/saw-script i…
Jul 9, 2021
6fef67a
remove Some from error constructor
Jul 9, 2021
f3b76bb
Merge branch 'master' into heapster-ide-info
glguy Jul 26, 2021
e2c9cd6
Export valueperms in full json detail
glguy Jul 28, 2021
b59adb9
Avoid generating orphan ToJSON instances and using Given
glguy Jul 28, 2021
65ae7dd
refine jsonexport instances
glguy Jul 28, 2021
931d802
Document JSONExport
glguy Jul 28, 2021
2ad2225
Remove need for passing undefined
glguy Jul 30, 2021
ce3313b
JSONExport support for PermImpls
glguy Jul 30, 2021
df114c1
export entrypoint and caller ID information
Aug 12, 2021
8875708
cleanup imports, 80 char columns
Aug 12, 2021
5f12cc4
heapster: export function name for IDE
Aug 12, 2021
cb7c57c
heapster-saw: LogEntry with names and structure
glguy Aug 19, 2021
e768f1f
Incorporate names from bindings in JsonExport
glguy Aug 20, 2021
f60affd
Merge remote-tracking branch 'origin/master' into heapster-ide-info
glguy Aug 20, 2021
51665d7
Update PPInfo while exporting
glguy Aug 23, 2021
dc70b93
checkpoint
glguy Aug 27, 2021
f0c7747
Use types to generate names for pretty permissions where possible
glguy Aug 27, 2021
e634949
Checkpoint
glguy Aug 28, 2021
b284fc4
Checkpoint
glguy Aug 28, 2021
491c38f
Update cabal file
glguy Aug 30, 2021
4454faf
Merge branch 'master' into glguy/heapster-ide-info
Aug 30, 2021
3d0ae00
user the error prefix when logging errors for IDE
Aug 31, 2021
4e4cc4b
revert commented error prefix code
Aug 31, 2021
f60e26b
Change Mb' to NMb
glguy Aug 31, 2021
f34cabb
Merge branch 'glguy/heapster-ide-info' of github.com:GaloisInc/saw-sc…
glguy Aug 31, 2021
24d7122
Comments and more consistent naming
glguy Aug 31, 2021
2ac547b
Merge branch 'master' of github.com:GaloisInc/saw-script into heapste…
glguy Aug 31, 2021
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Incorporate names from bindings in JsonExport
  • Loading branch information
glguy committed Aug 20, 2021
commit e768f1fdfeb58dc574ae7c8b7b10c8c3f17e7bb9
2 changes: 2 additions & 0 deletions heapster-saw/src/Verifier/SAW/Heapster/JSONExport.hs
Original file line number Diff line number Diff line change
Expand Up @@ -62,8 +62,10 @@ instance JsonExport1 f => JsonExport (Assignment f x) where
instance JsonExport1 f => JsonExport (RAssign f x) where
jsonExport = toJSON . mapToList jsonExport1


instance JsonExport b => JsonExport (Mb (a :: RList CrucibleType) b) where
jsonExport mb = mbLift $ flip nuMultiWithElim1 mb $ \names body ->
let ?ppi = ppInfoAddExprNames "x" names ?ppi in
object [
("args", jsonExport names),
("body", jsonExport body)
Expand Down