GaloisInc/saw-script issues and pull requests

#77 - Let SAW definition labels begin with underscore

Issue - State: closed - Opened by jpziegler almost 9 years ago
Labels: easy

#76 - fresh_symbolic and abc

Issue - State: closed - Opened by msaaltink almost 9 years ago

#75 - saw: Bad uninterpreted constant name?

Issue - State: closed - Opened by msaaltink almost 9 years ago - 2 comments
Labels: priority, maybe-fixed

#74 - internal error: esEval failed to evaluate expression

Issue - State: closed - Opened by hjroberts3141 almost 9 years ago - 2 comments
Labels: next

#73 - Unable to view SAW version

Issue - State: closed - Opened by jpziegler almost 9 years ago - 1 comment
Labels: easy

#72 - Simulation error: Invalid load address

Issue - State: closed - Opened by weaversa almost 9 years ago - 2 comments
Labels: obsolete

#71 - test00012 is broken

Issue - State: closed - Opened by robdockins almost 9 years ago - 2 comments

#70 - Better error message when LLVM function not found

Issue - State: closed - Opened by atomb almost 9 years ago

#69 - Initialize all Java fields to fresh values unless otherwise specified in `java_verify`

Issue - State: closed - Opened by atomb almost 9 years ago - 1 comment
Labels: enhancement, obsolete

#68 - Add `java_assert_eq` command

Issue - State: closed - Opened by atomb almost 9 years ago

#67 - "All paths yielded errors! To see details, use --errpaths."

Issue - State: closed - Opened by znewsham almost 9 years ago - 16 comments
Labels: maybe-fixed

#66 - writeSAIGInferLatches: domain or range not finite width:

Issue - State: closed - Opened by weaversa about 9 years ago - 6 comments

#65 - Pattern match failure when evaluating Cryptol list comprehensions with infinite streams

Issue - State: closed - Opened by brianhuffman about 9 years ago - 1 comment

#64 - SAW Simulator error: Verifier.SAW.Simulator.BitBlast.toBool [_,_,_,_,_,_,_,_]

Issue - State: closed - Opened by thoughtpolice about 9 years ago - 4 comments
Labels: maybe-fixed

#63 - Deprecate `external_aig_solver`

Issue - State: open - Opened by atomb about 9 years ago - 3 comments
Labels: enhancement

#62 - Unimplemented Primitives

Issue - State: closed - Opened by weaversa about 9 years ago - 4 comments

#61 - Choose better names for _assert, _assert_eq, and *_ensure_eq

Issue - State: closed - Opened by brianhuffman about 9 years ago - 1 comment
Labels: enhancement, obsolete, breaking

#60 - Using unint_z3 with uninterpreted functions of polymorphic types doesn't work

Issue - State: closed - Opened by brianhuffman about 9 years ago
Labels: priority

#59 - Uninformative error message "internal: esEval failed to evaluate expression"

Issue - State: closed - Opened by brianhuffman about 9 years ago

#58 - Fix test0001

Issue - State: closed - Opened by atomb about 9 years ago

#57 - Support arrays of bytes, chars, and shorts in java_symexec

Issue - State: closed - Opened by atomb about 9 years ago - 1 comment
Labels: maybe-fixed

#56 - Useful error message for non-terminating symbolic execution?

Issue - State: open - Opened by atomb about 9 years ago - 1 comment
Labels: question

#55 - Support ABC commands in SAWScript?

Issue - State: closed - Opened by atomb about 9 years ago - 1 comment
Labels: question

#54 - Look into making use of ABC's parallelism

Issue - State: closed - Opened by atomb about 9 years ago - 1 comment
Labels: question

#53 - Better error message when giving `ensure_eq` for a parameter

Issue - State: closed - Opened by atomb about 9 years ago

#52 - Add primitive for QBF generation

Issue - State: open - Opened by atomb about 9 years ago - 1 comment
Labels: enhancement

#51 - Make branch satisfiability checking optional in JSS and LSS interfaces

Issue - State: closed - Opened by atomb about 9 years ago - 1 comment

#50 - Make `java_var` emit an error when used with class type

Issue - State: closed - Opened by atomb about 9 years ago

#49 - Create "certified term" type

Issue - State: open - Opened by atomb about 9 years ago - 2 comments
Labels: enhancement

#48 - Tutorial example `dotprod` fails due to unimplemented primitives

Issue - State: closed - Opened by atomb about 9 years ago - 8 comments
Labels: bug

#47 - LLVM location expression "*(args[0])" not understood

Issue - State: closed - Opened by atomb about 9 years ago - 2 comments
Labels: bug, maybe-fixed

#46 - Track error conditions in Java and LLVM symbolic execution

Issue - State: closed - Opened by atomb about 9 years ago
Labels: enhancement

#45 - Make `print` and `show` display Cryptol, Java, and LLVM module contents

Issue - State: closed - Opened by atomb about 9 years ago - 2 comments
Labels: enhancement

#44 - Support multi-dimensional Java arrays

Issue - State: closed - Opened by atomb about 9 years ago - 3 comments
Labels: enhancement

#43 - Java code calling `Array.fill` fails

Issue - State: closed - Opened by atomb about 9 years ago
Labels: priority

#42 - When complaining about missing `java_modify`, print type

Issue - State: closed - Opened by atomb about 9 years ago

#41 - Make pedantic checks in `java_verify` optional

Issue - State: closed - Opened by atomb about 9 years ago - 3 comments
Labels: enhancement, wontfix, obsolete

#40 - Problem with SBV backend translation

Issue - State: closed - Opened by robdockins about 9 years ago - 4 comments
Labels: bug

#39 - Static member names should be resolvable based on the current class

Issue - State: closed - Opened by acfoltzer about 9 years ago - 1 comment
Labels: enhancement, obsolete

#38 - Unable to print help on "basic_ss" from saw

Issue - State: closed - Opened by jpziegler about 9 years ago
Labels: bug

#37 - Type variables from the Cryptol environment are not in scope within type brackets {| |}

Issue - State: closed - Opened by brianhuffman about 9 years ago - 1 comment

#36 - SAWScript type-brackets {| |} don't work for numeric types

Issue - State: closed - Opened by brianhuffman about 9 years ago

#35 - Printing of counterexamples sometimes fails with run-time type error

Issue - State: closed - Opened by brianhuffman about 9 years ago
Labels: bug

#34 - SAWScript variables of type `Type` should be added to Cryptol context

Issue - State: closed - Opened by brianhuffman over 9 years ago

#33 - Support for converting Cryptol values to other SAWScript types

Issue - State: closed - Opened by brianhuffman over 9 years ago - 2 comments
Labels: enhancement

#32 - Add "show" function of type "{a} a -> String"

Issue - State: closed - Opened by brianhuffman over 9 years ago
Labels: enhancement

#31 - Sandbox build failure

Issue - State: closed - Opened by abedra over 9 years ago - 3 comments
Labels: bug, external

#30 - Unsound compositional proof

Issue - State: closed - Opened by msaaltink over 9 years ago - 4 comments
Labels: bug, unsoundness

#29 - Add support for output in different bases

Issue - State: closed - Opened by jpziegler over 9 years ago - 2 comments
Labels: enhancement

#28 - Add support for ASCII output

Issue - State: closed - Opened by jpziegler over 9 years ago
Labels: enhancement

#27 - Failing due to -Werror

Issue - State: closed - Opened by weaversa over 9 years ago - 2 comments

#26 - Private Repos in build-sandbox.sh

Issue - State: closed - Opened by Hryo224 over 9 years ago
Labels: bug

#25 - Issuing prove_print command in interpreter results in extra output

Issue - State: closed - Opened by jpziegler over 9 years ago - 2 comments
Labels: better-in-python

#24 - Tutorial gives incorrect command-line arguments

Issue - State: closed - Opened by jpziegler over 9 years ago - 1 comment
Labels: bug, documentation

#23 - Friendly error message when classes.jar is missing

Issue - State: closed - Opened by joehendrix over 9 years ago - 1 comment
Labels: enhancement

#22 - saw: user error (Unimplemented global: Cryptol.ecInfFromThen)

Issue - State: closed - Opened by TomMD over 9 years ago

#21 - llvm_symexec does not typecheck its term arguments

Issue - State: closed - Opened by brianhuffman over 9 years ago - 2 comments
Labels: wontfix, maybe-fixed, obsolete

#20 - saw: user error (asFiniteType: unsupported argument type: Cryptol.Num)

Issue - State: closed - Opened by TomMD over 9 years ago - 5 comments

#19 - Unexpected types from llvm_symexec / abstract_symbolic

Issue - State: closed - Opened by TomMD over 9 years ago - 3 comments

#18 - Odd symbols being looked for in LLVM modules

Issue - State: closed - Opened by TomMD over 9 years ago - 2 comments

#17 - Relative filenames in scripts

Issue - State: closed - Opened by joehendrix over 9 years ago
Labels: enhancement, easy, priority

#16 - "No bindings" error should probably be 1-indexed.

Issue - State: closed - Opened by TomMD over 9 years ago - 4 comments
Labels: enhancement

#15 - Cryptol `type` bindings in `let` blocks are not in scope afterwards

Issue - State: closed - Opened by brianhuffman over 9 years ago - 1 comment
Labels: bug

#14 - iteOp: malformed arguments (muxBVal)

Issue - State: closed - Opened by msaaltink over 9 years ago

#13 - Support Cryptol's switch to `Data.Text` from `String`.

Issue - State: closed - Opened by ntc2 over 9 years ago - 1 comment
Labels: enhancement

#12 - saw: src/Data/ABC/GIA.hs:334:11-16: Assertion failed

Issue - State: closed - Opened by TomMD over 9 years ago - 1 comment

#11 - Unhandled exception (index out of bounds)

Issue - State: closed - Opened by TomMD over 9 years ago - 6 comments
Labels: bug

#10 - `prove` and `sat` fails on proof scripts of types other than `ProofScript SatResult`

Issue - State: closed - Opened by brianhuffman over 9 years ago

#9 - Redo the sawscript ProofScript primitives

Issue - State: closed - Opened by brianhuffman over 9 years ago - 6 comments
Labels: enhancement, tech-debt

#8 - llvm_extract and endianness

Issue - State: closed - Opened by msaaltink over 9 years ago - 2 comments

#7 - saw: user error (sbvCodeGen: invalid result type: not boolean or bitvector)

Issue - State: closed - Opened by msaaltink over 9 years ago - 2 comments
Labels: bug

#6 - SBV->C: Unexpected: mkConst: False

Issue - State: closed - Opened by msaaltink over 9 years ago - 4 comments
Labels: bug

#5 - Fix SBVParser mapping between internal types (lists of words) and external cryptol-style types

Issue - State: closed - Opened by brianhuffman over 9 years ago - 2 comments

#4 - Partially applied sawscript commands should print type of expected arguments

Issue - State: closed - Opened by brianhuffman over 9 years ago
Labels: enhancement

GitHub / GaloisInc/saw-script issues and pull requests