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

#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

#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

#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

#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

#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

#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

#44 - Simplify equality permissions when recombining

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

#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

#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

#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

#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