Ecosyste.ms: Issues
An open API service for providing issue and pull request metadata for open source projects.
GitHub / GaloisInc/heapster-saw issues and pull requests
#91 - Crash while typechecking
Issue -
State: open - Opened by abakst over 2 years ago
#90 - Widening
Pull Request -
State: closed - Opened by eddywestbrook over 3 years ago
#89 - resolve GHC warnings
Pull Request -
State: closed - Opened by glguy over 3 years ago
- 1 comment
#88 - Simplify and isolate the GenStateCont type
Pull Request -
State: closed - Opened by glguy over 3 years ago
#87 - Build against hobbits-1.4
Pull Request -
State: closed - Opened by glguy over 3 years ago
#86 - Implement IDE support
Issue -
State: open - Opened by karljs over 3 years ago
#85 - Support building Heapster shapes from Rust type declarations
Pull Request -
State: closed - Opened by ChrisEPhifer over 3 years ago
- 2 comments
Labels: enhancement
#84 - Implement a widening operation
Issue -
State: open - Opened by eddywestbrook over 3 years ago
- 13 comments
#83 - Update Heapster to work with the latest Crucible
Issue -
State: open - Opened by eddywestbrook over 3 years ago
- 1 comment
#82 - Change reachability permissions to reach a variable instead of an arbitrary permission
Issue -
State: closed - Opened by eddywestbrook over 3 years ago
#81 - Make an explicit named shape expression constructor
Issue -
State: closed - Opened by eddywestbrook over 3 years ago
#80 - Get rid of Heapster's GHC warnings
Issue -
State: open - Opened by m-yac over 3 years ago
#79 - Replace KnownRepr TypeRepr instances with TypeReprs in existentials
Issue -
State: open - Opened by eddywestbrook over 3 years ago
#78 - Add support for error functions, exit, and other functions that do not return
Issue -
State: open - Opened by eddywestbrook over 3 years ago
#77 - Change array permissions so they only have one modality
Issue -
State: open - Opened by eddywestbrook over 3 years ago
#76 - Specialized build script for heapster
Issue -
State: open - Opened by m-yac over 3 years ago
- 1 comment
#75 - Use computational reflection for proving refinement
Issue -
State: open - Opened by m-yac over 3 years ago
#74 - General data type for recursive permissions
Issue -
State: open - Opened by m-yac over 3 years ago
#73 - Model Alloca'd Storage via a Lifetime
Issue -
State: open - Opened by eddywestbrook over 3 years ago
#72 - Array shapes should contain lists of shapes, not lists of permissions
Issue -
State: open - Opened by eddywestbrook over 3 years ago
#71 - Allow Named Shapes to be Defined with Rust Types
Issue -
State: open - Opened by eddywestbrook over 3 years ago
#70 - Allow permissions to be specified with Rust types
Issue -
State: open - Opened by eddywestbrook over 3 years ago
- 13 comments
#69 - Handle structs and permissions on structs
Issue -
State: closed - Opened by eddywestbrook over 3 years ago
#68 - Cannot translate casts that change the translation type
Issue -
State: closed - Opened by eddywestbrook over 3 years ago
- 1 comment
#67 - Cannot translate casts that change the translation type
Issue -
State: open - Opened by eddywestbrook over 3 years ago
#66 - Allow permissions on ghost variables in function permissions
Issue -
State: open - Opened by eddywestbrook almost 4 years ago
#65 - Have partial substitution failure be a type-checking failure, not an error
Issue -
State: closed - Opened by eddywestbrook almost 4 years ago
#64 - Rewrite proveVarLLVMField
Issue -
State: open - Opened by eddywestbrook almost 4 years ago
#63 - Prove fields from arrays of bytes
Issue -
State: closed - Opened by eddywestbrook almost 4 years ago
#62 - Figure out how to effectively use lifetimes
Issue -
State: open - Opened by eddywestbrook almost 4 years ago
- 23 comments
#61 - Add Support for Local Proofs
Issue -
State: open - Opened by eddywestbrook almost 4 years ago
- 2 comments
#60 - Implement LLVM shapes
Issue -
State: closed - Opened by eddywestbrook almost 4 years ago
- 18 comments
#59 - Change the definition of `BVVec` to use normal `Vec`
Issue -
State: closed - Opened by eddywestbrook almost 4 years ago
- 1 comment
#58 - Implement a General Matching Algorithm
Issue -
State: closed - Opened by eddywestbrook almost 4 years ago
#57 - Reachability permissions
Issue -
State: closed - Opened by eddywestbrook almost 4 years ago
- 1 comment
#56 - Make it easier to see when type-checking fails
Issue -
State: closed - Opened by eddywestbrook almost 4 years ago
#55 - Figure out how to write correct permissions for memcpy
Issue -
State: closed - Opened by eddywestbrook almost 4 years ago
- 6 comments
#54 - Change heapster_gen_block_perms_hint to generalize equality to other types, not just bitvectors
Issue -
State: closed - Opened by eddywestbrook almost 4 years ago
#53 - Print higher-level typing errors in Coq specs
Issue -
State: closed - Opened by eddywestbrook almost 4 years ago
- 1 comment
#52 - Enable separate verification for different C files
Issue -
State: open - Opened by eddywestbrook almost 4 years ago
- 1 comment
#51 - Simplify sigma types with a unit second projection in the translation
Issue -
State: open - Opened by eddywestbrook almost 4 years ago
#50 - Simplify the translation of non-mutually recursive functions
Issue -
State: open - Opened by eddywestbrook almost 4 years ago
#49 - Verbosity flag to disable trace output
Issue -
State: open - Opened by eddywestbrook almost 4 years ago
#48 - Remember C variable names in Coq specs
Issue -
State: open - Opened by eddywestbrook almost 4 years ago
- 1 comment
#47 - Rewrite parser
Issue -
State: open - Opened by eddywestbrook almost 4 years ago
#46 - Remove all compiler warnings in Heapster code
Issue -
State: open - Opened by eddywestbrook almost 4 years ago
#45 - Change the representation of bitvector expressions to use the BV type
Issue -
State: closed - Opened by eddywestbrook almost 4 years ago
#44 - Simplify equality permissions when recombining
Issue -
State: closed - Opened by eddywestbrook about 4 years ago
#43 - Change the implication prover to not rely on the ordering of arguments
Issue -
State: closed - Opened by eddywestbrook about 4 years ago
#42 - Add support for non-function global variables
Issue -
State: open - Opened by eddywestbrook about 4 years ago
#41 - Remove un-determined variables when creating entrypoint permissions
Issue -
State: closed - Opened by eddywestbrook about 4 years ago
- 1 comment
#40 - Add join point hints for blocks
Issue -
State: closed - Opened by eddywestbrook about 4 years ago
#39 - Permissions abbreviation bug
Issue -
State: closed - Opened by karljs about 4 years ago
- 1 comment
#38 - add bvashr
Pull Request -
State: closed - Opened by karljs about 4 years ago
#37 - Handle non-word-sized loads and stores
Issue -
State: closed - Opened by eddywestbrook about 4 years ago
- 3 comments
#36 - Remove the `AtomicPerm` type
Issue -
State: open - Opened by eddywestbrook about 4 years ago
- 1 comment
#35 - Change atomic permission constructs to named atomic permissions
Issue -
State: open - Opened by eddywestbrook about 4 years ago
- 1 comment
#34 - Fix haddocks
Pull Request -
State: closed - Opened by karljs about 4 years ago
#33 - Updated haddocks for GHC 8.6 compatibility.
Pull Request -
State: open - Opened by kquick about 4 years ago
- 2 comments
#32 - Named atomic permissions
Issue -
State: closed - Opened by eddywestbrook about 4 years ago
- 6 comments
#31 - Fix the semantics of memClear for sizes that are not a multiple of the word size
Issue -
State: closed - Opened by eddywestbrook about 4 years ago
#30 - Add heapster_get_cfg command
Issue -
State: closed - Opened by eddywestbrook about 4 years ago
- 1 comment
#29 - Fix the copyable semantics for named permissions
Issue -
State: open - Opened by eddywestbrook about 4 years ago
- 1 comment
#28 - Change types that should be RAssign to use RAssign
Issue -
State: open - Opened by eddywestbrook about 4 years ago
- 2 comments
#27 - Handle Rust symbol mangling
Issue -
State: closed - Opened by eddywestbrook about 4 years ago
#26 - Allow heapster_define_perm to change the representation type
Issue -
State: open - Opened by eddywestbrook about 4 years ago
- 1 comment
#25 - Move functionality into Hobbits
Pull Request -
State: closed - Opened by karljs about 4 years ago
#24 - Fix stylistic concerns in HeapsterBuiltins.hs
Issue -
State: closed - Opened by eddywestbrook about 4 years ago
- 6 comments
#23 - User-supplied hints for block entry permissions
Issue -
State: closed - Opened by eddywestbrook about 4 years ago
- 1 comment
#22 - Add explicit type check in parseAndInsDef
Issue -
State: closed - Opened by m-yac about 4 years ago
- 1 comment
#21 - Make a new release of Hobbits, so Heapster no longer depends on a specific commit
Issue -
State: closed - Opened by eddywestbrook about 4 years ago
- 1 comment
#20 - Incorporate building the Coq export libraries into the top-level build procedure
Issue -
State: open - Opened by eddywestbrook about 4 years ago
#19 - update for ghc 8.6 monadfail changes
Pull Request -
State: closed - Opened by karljs about 4 years ago
#18 - Implement `showHeapsterEnv`
Issue -
State: closed - Opened by eddywestbrook about 4 years ago
- 1 comment
#17 - Change the translation of the unit type to not have computational content
Issue -
State: closed - Opened by eddywestbrook over 4 years ago
- 4 comments
#16 - Add parsing support to SAW script for Heapster permissions and other constructs
Issue -
State: open - Opened by eddywestbrook over 4 years ago
#15 - Remove non-identifier characters from Heapster-generated definition names
Issue -
State: closed - Opened by eddywestbrook over 4 years ago
- 1 comment
#14 - Don't make a new definition if `parseAndInsDef` is passed an identifier
Issue -
State: closed - Opened by m-yac over 4 years ago
- 1 comment
#13 - Add strings to errorM to indicate the typing errors that produce them
Issue -
State: closed - Opened by eddywestbrook over 4 years ago
- 1 comment
#12 - Add a new atomic permission for uninitialized bytes / unstructured memory
Issue -
State: closed - Opened by eddywestbrook over 4 years ago
- 1 comment
#11 - Implement heapster_define_perm
Issue -
State: closed - Opened by eddywestbrook over 4 years ago
- 3 comments
#10 - Support GHC 8.6 and newer
Issue -
State: closed - Opened by karljs over 4 years ago
- 2 comments
#9 - Pretty-print function permissions
Issue -
State: open - Opened by eddywestbrook over 4 years ago
- 2 comments
#8 - Finish implementing array permissions
Issue -
State: closed - Opened by eddywestbrook over 4 years ago
- 4 comments
#7 - Add syntax for beginning and ending Heapster lifetimes
Issue -
State: open - Opened by eddywestbrook over 4 years ago
#6 - Remove the "function lifetime" argument from function permissions
Issue -
State: closed - Opened by eddywestbrook over 4 years ago
#5 - Fix xor_swap.saw example
Issue -
State: closed - Opened by eddywestbrook over 4 years ago
- 1 comment
#4 - Define heapster_define_recursive_perm
Issue -
State: closed - Opened by m-yac over 4 years ago
- 4 comments
#3 - Allow terms in heapster_define_opaque_perm
Issue -
State: closed - Opened by m-yac over 4 years ago
- 6 comments
#2 - Allow terms in heapster_assume_fun
Issue -
State: closed - Opened by m-yac over 4 years ago
- 12 comments
#1 - Implement heapster_init_env_from_file
Issue -
State: closed - Opened by eddywestbrook over 4 years ago
- 3 comments