GaloisInc heapster-saw issues

GaloisInc / heapster-saw

Implementation of the Heapster type system of separation types inside SAW, including a translation to SAW core

BSD 3-Clause "New" or "Revised" License

8 stars 3 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Crash while typechecking

#91 abakst opened 2 years ago
0
Widening

#90 eddywestbrook closed 3 years ago
0
resolve GHC warnings

#89 glguy closed 3 years ago
1
Simplify and isolate the GenStateCont type

#88 glguy closed 3 years ago
0
Build against hobbits-1.4

#87 glguy closed 3 years ago
0
Implement IDE support

#86 karljs opened 3 years ago
0
Support building Heapster shapes from Rust type declarations

#85 ChrisEPhifer closed 3 years ago
2
Implement a widening operation

#84 eddywestbrook opened 3 years ago
13
Update Heapster to work with the latest Crucible

#83 eddywestbrook opened 3 years ago
1
Change reachability permissions to reach a variable instead of an arbitrary permission

#82 eddywestbrook closed 3 years ago
0
Make an explicit named shape expression constructor

#81 eddywestbrook closed 3 years ago
0
Get rid of Heapster's GHC warnings

#80 m-yac opened 3 years ago
0
Replace KnownRepr TypeRepr instances with TypeReprs in existentials

#79 eddywestbrook opened 3 years ago
0
Add support for error functions, exit, and other functions that do not return

#78 eddywestbrook opened 3 years ago
0
Change array permissions so they only have one modality

#77 eddywestbrook opened 3 years ago
0
Specialized build script for heapster

#76 m-yac opened 3 years ago
1
Use computational reflection for proving refinement

#75 m-yac opened 3 years ago
0
General data type for recursive permissions

#74 m-yac opened 3 years ago
0
Model Alloca'd Storage via a Lifetime

#73 eddywestbrook opened 3 years ago
0
Array shapes should contain lists of shapes, not lists of permissions

#72 eddywestbrook opened 3 years ago
0
Allow Named Shapes to be Defined with Rust Types

#71 eddywestbrook opened 3 years ago
0
Allow permissions to be specified with Rust types

#70 eddywestbrook opened 3 years ago
13
Handle structs and permissions on structs

#69 eddywestbrook closed 3 years ago
0
Cannot translate casts that change the translation type

#68 eddywestbrook closed 3 years ago
1
Cannot translate casts that change the translation type

#67 eddywestbrook opened 3 years ago
0
Allow permissions on ghost variables in function permissions

#66 eddywestbrook opened 3 years ago
0
Have partial substitution failure be a type-checking failure, not an error

#65 eddywestbrook closed 3 years ago
0
Rewrite proveVarLLVMField

#64 eddywestbrook opened 3 years ago
0
Prove fields from arrays of bytes

#63 eddywestbrook closed 3 years ago
0
Figure out how to effectively use lifetimes

#62 eddywestbrook opened 3 years ago
23
Add Support for Local Proofs

#61 eddywestbrook opened 3 years ago
2
Implement LLVM shapes

#60 eddywestbrook closed 3 years ago
18
Change the definition of `BVVec` to use normal `Vec`

#59 eddywestbrook closed 3 years ago
1
Implement a General Matching Algorithm

#58 eddywestbrook closed 3 years ago
0
Reachability permissions

#57 eddywestbrook closed 3 years ago
1
Make it easier to see when type-checking fails

#56 eddywestbrook closed 4 years ago
0
Figure out how to write correct permissions for memcpy

#55 eddywestbrook closed 3 years ago
6
Change heapster_gen_block_perms_hint to generalize equality to other types, not just bitvectors

#54 eddywestbrook closed 4 years ago
0
Print higher-level typing errors in Coq specs

#53 eddywestbrook closed 4 years ago
1
Enable separate verification for different C files

#52 eddywestbrook opened 4 years ago
1
Simplify sigma types with a unit second projection in the translation

#51 eddywestbrook opened 4 years ago
0
Simplify the translation of non-mutually recursive functions

#50 eddywestbrook opened 4 years ago
0
Verbosity flag to disable trace output

#49 eddywestbrook opened 4 years ago
0
Remember C variable names in Coq specs

#48 eddywestbrook opened 4 years ago
1
Rewrite parser

#47 eddywestbrook opened 4 years ago
0
Remove all compiler warnings in Heapster code

#46 eddywestbrook opened 4 years ago
0
Change the representation of bitvector expressions to use the BV type

#45 eddywestbrook closed 4 years ago
0
Simplify equality permissions when recombining

#44 eddywestbrook closed 4 years ago
0
Change the implication prover to not rely on the ordering of arguments

#43 eddywestbrook closed 4 years ago
0
Add support for non-function global variables

#42 eddywestbrook opened 4 years ago
0