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

#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

#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

#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

#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