Ecosyste.ms: Issues
An open API service for providing issue and pull request metadata for open source projects.
GitHub / GaloisInc/reopt-vcg issues and pull requests
#138 - Manual memory safety annots
Pull Request -
State: closed - Opened by simonjwinwood about 3 years ago
#137 - WIP: remove LLVM-8 dep (archiving manual x86 semantics)
Pull Request -
State: open - Opened by pnwamk about 3 years ago
- 1 comment
#136 - doc: improve help message and README.md
Pull Request -
State: closed - Opened by pnwamk about 3 years ago
#135 - feat: stream JSON output as it is computed
Pull Request -
State: closed - Opened by Ptival about 3 years ago
#134 - chore: bump lean4 dep to leanprover/lean4:nightly-2021-08-18
Pull Request -
State: closed - Opened by pnwamk about 3 years ago
#133 - reopt-vcg does not handle absolute paths correctly
Issue -
State: closed - Opened by Ptival about 3 years ago
- 1 comment
#132 - chore: tweak the JSON goal output
Pull Request -
State: closed - Opened by pnwamk about 3 years ago
#131 - Updates to support tail calls, noreturn functions, and external funct…
Pull Request -
State: closed - Opened by simonjwinwood about 3 years ago
#130 - feat: exit codes report failure via bit flags
Pull Request -
State: closed - Opened by pnwamk about 3 years ago
#129 - memory stack assertions
Pull Request -
State: closed - Opened by simonjwinwood over 3 years ago
#128 - Added constant folding to the SMT constructors; added constant arrays
Pull Request -
State: closed - Opened by simonjwinwood over 3 years ago
#127 - Added support for instrinsic functions (llvm.ssub.with.overflow.iN)
Pull Request -
State: closed - Opened by simonjwinwood over 3 years ago
#126 - Cancel reopt-vcg on Ctrl-C
Issue -
State: open - Opened by joehendrix over 3 years ago
#125 - docs and Dockerfile
Pull Request -
State: closed - Opened by pnwamk over 3 years ago
#124 - feat: make generated script for Lean LSP env vars (set_lean_env_vars.sh)
Pull Request -
State: closed - Opened by pnwamk over 3 years ago
#123 - elan based builds
Pull Request -
State: closed - Opened by pnwamk over 3 years ago
#122 - Add support for structures
Pull Request -
State: closed - Opened by simonjwinwood over 3 years ago
#121 - Extensions to support FP args and return values.
Pull Request -
State: closed - Opened by simonjwinwood over 3 years ago
#120 - chore: fix expected test output
Pull Request -
State: closed - Opened by pnwamk over 3 years ago
#119 - FP support in VCG
Pull Request -
State: closed - Opened by simonjwinwood over 3 years ago
#118 - chore: swap default backends
Pull Request -
State: closed - Opened by pnwamk over 3 years ago
#117 - add Dockerfile build to nightly CI
Pull Request -
State: closed - Opened by pnwamk over 3 years ago
#116 - add Dockerfile build to nightly CI
Pull Request -
State: closed - Opened by pnwamk over 3 years ago
#115 - add Dockerfile build to nightly CI
Pull Request -
State: closed - Opened by pnwamk over 3 years ago
#114 - feat: DF handling matching Haskell prototype
Pull Request -
State: closed - Opened by pnwamk over 3 years ago
#113 - feat: leave instruction for kbackend
Pull Request -
State: closed - Opened by pnwamk over 3 years ago
#112 - VC gen error: unsupported argument type <8 x double>
Issue -
State: open - Opened by pnwamk over 3 years ago
Labels: vc gen error
#111 - movabsq and k-backend tests
Pull Request -
State: closed - Opened by pnwamk over 3 years ago
#110 - feat: nop* and movs* instructions
Pull Request -
State: closed - Opened by pnwamk over 3 years ago
#109 - fix: correct isBitSet for K backend
Pull Request -
State: closed - Opened by pnwamk over 3 years ago
#108 - fix: binary bitvector pretty printing
Pull Request -
State: closed - Opened by pnwamk over 3 years ago
#107 - tidy and better VCG error reporting
Pull Request -
State: closed - Opened by pnwamk over 3 years ago
#106 - fix: correct immediate size in x86 disassembler
Pull Request -
State: closed - Opened by pnwamk over 3 years ago
#105 - feat: initial support for llvm select function
Pull Request -
State: closed - Opened by pnwamk over 3 years ago
#104 - feat: add --json-goals flag, refactor verification reporting slightly
Pull Request -
State: closed - Opened by pnwamk over 3 years ago
#103 - improve error reporting, add detailed summaries
Pull Request -
State: closed - Opened by pnwamk almost 4 years ago
#102 - Update/clean up README.md and INSTALL.md
Issue -
State: closed - Opened by pnwamk almost 4 years ago
#101 - Assert stack is outside of data segment
Issue -
State: open - Opened by pnwamk almost 4 years ago
#100 - chore: lean4 bump to new frontend (0731d3f080e1ba6fcc57686e172f65e5b1…
Pull Request -
State: closed - Opened by pnwamk almost 4 years ago
#99 - chore: delete old files, move Lean4 prototype to root directory
Pull Request -
State: closed - Opened by pnwamk almost 4 years ago
#98 - feature: add support for LLVM load/store statements
Pull Request -
State: closed - Opened by pnwamk almost 4 years ago
- 1 comment
#97 - chore: make register name conversion (to/from string) nicer
Issue -
State: open - Opened by simonjwinwood about 4 years ago
#96 - Remove old files
Issue -
State: closed - Opened by pnwamk about 4 years ago
- 1 comment
#95 - feature: support FREEBSD elf binaries (or at least don't reject them)
Pull Request -
State: closed - Opened by pnwamk about 4 years ago
#94 - chore: remove no-longer-used Denote.lean from SmtLib
Pull Request -
State: closed - Opened by pnwamk about 4 years ago
#93 - integration tests
Pull Request -
State: closed - Opened by pnwamk about 4 years ago
#92 - denotation/semantics for SMTLIB concepts
Pull Request -
State: closed - Opened by pnwamk about 4 years ago
#91 - feat: initial smt denote for terms
Pull Request -
State: closed - Opened by pnwamk about 4 years ago
- 1 comment
#90 - Added actions CI
Pull Request -
State: closed - Opened by simonjwinwood about 4 years ago
#89 - CI PR, don't merge
Pull Request -
State: closed - Opened by simonjwinwood about 4 years ago
- 1 comment
#88 - Updated lean (to get --root)
Pull Request -
State: closed - Opened by simonjwinwood about 4 years ago
#87 - remove IO from core monads
Pull Request -
State: closed - Opened by pnwamk about 4 years ago
#86 - Lean4 36c971546 (well 0f598cca58b2)
Pull Request -
State: closed - Opened by simonjwinwood about 4 years ago
#85 - chore: bump lean-llvm submodule, make needed tweaks
Pull Request -
State: closed - Opened by pnwamk over 4 years ago
#84 - fix: proper set_io_error usage in FFI
Pull Request -
State: closed - Opened by pnwamk over 4 years ago
#83 - minor tweaks for cvc4 flags
Pull Request -
State: closed - Opened by pnwamk over 4 years ago
#82 - printing improvements, updated default cvc4 flags
Pull Request -
State: closed - Opened by pnwamk over 4 years ago
#81 - feature: interactive/live handling of VCs
Pull Request -
State: closed - Opened by pnwamk over 4 years ago
#80 - make fresh names prettier for SMT
Pull Request -
State: closed - Opened by pnwamk over 4 years ago
#79 - fix and add a few unit tests
Pull Request -
State: closed - Opened by pnwamk over 4 years ago
#78 - Make SMTLIB use map for fresh names over a counter
Issue -
State: open - Opened by simonjwinwood over 4 years ago
#77 - add example .smt2 files for fib example
Pull Request -
State: closed - Opened by pnwamk over 4 years ago
#76 - single operand add instruction is broken
Issue -
State: open - Opened by simonjwinwood over 4 years ago
#75 - feature: verifyBlock
Pull Request -
State: closed - Opened by pnwamk over 4 years ago
#74 - use parseAssembly from lean-llvm not parseBitcodeFile
Pull Request -
State: closed - Opened by pnwamk over 4 years ago
#73 - initial BlockVCG.verifyPreconditions impl (cf verifyBlockPreconditions)
Pull Request -
State: closed - Opened by pnwamk over 4 years ago
#72 - feature: initial SMT export mode infrastructure and simple test
Pull Request -
State: closed - Opened by pnwamk over 4 years ago
#71 - initial prover interface functions
Pull Request -
State: closed - Opened by pnwamk over 4 years ago
#70 - unsoundness: check that the return address is not mutated
Issue -
State: open - Opened by simonjwinwood over 4 years ago
#69 - fix: hex parsing bug fix, simple test for parsing fib ann file
Pull Request -
State: closed - Opened by pnwamk over 4 years ago
#68 - Progress on stepNextStmt
Pull Request -
State: closed - Opened by simonjwinwood over 4 years ago
#67 - parsing complete, precondition SMT generation needs a little attention
Pull Request -
State: closed - Opened by pnwamk over 4 years ago
#66 - BlockVar parsing, reg64 helpers in x86 semantics
Pull Request -
State: closed - Opened by pnwamk over 4 years ago
#65 - more annotation parsing, need to impl precond parsing
Pull Request -
State: closed - Opened by pnwamk over 4 years ago
#64 - Split Backend into Expr and stateful APIs
Issue -
State: open - Opened by simonjwinwood over 4 years ago
#63 - Added a symbolic backend
Pull Request -
State: closed - Opened by simonjwinwood over 4 years ago
#62 - json/llvm/elf parsing progress in reopt-vcg main
Pull Request -
State: closed - Opened by pnwamk over 4 years ago
- 2 comments
#61 - Split out concrete operations into a structure
Pull Request -
State: closed - Opened by simonjwinwood over 4 years ago
#60 - Initial annotation JSON parsing and some CI tests
Pull Request -
State: closed - Opened by pnwamk over 4 years ago
#59 - basic smtlib support
Pull Request -
State: closed - Opened by simonjwinwood over 4 years ago
#58 - Factor out nat_expr from x86 semantics
Pull Request -
State: closed - Opened by simonjwinwood over 4 years ago
- 1 comment
#57 - Lean4 bump
Pull Request -
State: closed - Opened by pnwamk over 4 years ago
#56 - tweaks to Makefile to consistently generate target names and paths
Pull Request -
State: closed - Opened by pnwamk over 4 years ago
- 1 comment
#55 - this is just a test
Pull Request -
State: closed - Opened by pnwamk over 4 years ago
#54 - fix git submodule names (make them consistent)
Pull Request -
State: closed - Opened by pnwamk over 4 years ago
- 1 comment
#53 - progress on reopt-vcg Main.hs translation
Pull Request -
State: closed - Opened by pnwamk over 4 years ago
- 1 comment
#52 - add a simple INSTALL.md file
Pull Request -
State: closed - Opened by pnwamk over 4 years ago
- 1 comment
#51 - add g++ install to vagrant provision script
Pull Request -
State: closed - Opened by pnwamk over 4 years ago
#50 - Integration with lean-llvm
Pull Request -
State: closed - Opened by robdockins over 4 years ago
#49 - Updated lean4 (2be69f1d5)
Pull Request -
State: closed - Opened by simonjwinwood over 4 years ago
#48 - Fixed errors introduced by lean upgrade
Pull Request -
State: closed - Opened by simonjwinwood over 4 years ago
#47 - Updated to latest lean4
Pull Request -
State: closed - Opened by simonjwinwood almost 5 years ago
#46 - Feature/demo updates
Pull Request -
State: closed - Opened by simonjwinwood almost 5 years ago
#45 - Added Vagrant file
Pull Request -
State: closed - Opened by simonjwinwood almost 5 years ago
#44 - Added Vagrant file
Pull Request -
State: closed - Opened by simonjwinwood almost 5 years ago
#43 - Updated lean4 and fixed resulting errors.
Pull Request -
State: closed - Opened by simonjwinwood about 5 years ago
#42 - Add support to generate x86 semantics using K
Pull Request -
State: closed - Opened by andreistefanescu about 5 years ago
#41 - Remove annotations file after migrating to reopt
Pull Request -
State: closed - Opened by joehendrix about 5 years ago
#40 - Migrate Haskell prototype VCG to main reopt repo.
Pull Request -
State: closed - Opened by joehendrix about 5 years ago
#38 - Feature/lean4 evaluator
Pull Request -
State: closed - Opened by simonjwinwood over 5 years ago