Ecosyste.ms: Issues

An open API service for providing issue and pull request metadata for open source projects.

GitHub / smackers/smack issues and pull requests

#100 - Integrate SVCOMP functionality

Pull Request - State: closed - Opened by MontyCarter over 9 years ago - 1 comment

#99 - Modularize smack.py

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

#98 - --debug to smack.py causes error in smack executable

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

#97 - Small fixes to build.sh

Pull Request - State: closed - Opened by MontyCarter over 9 years ago - 1 comment

#96 - Cannot build SMACK on cygwin - to_string not found

Issue - State: closed - Opened by zvonimir over 9 years ago - 1 comment
Labels: wontfix

#95 - Mark smackverify.py command line options as comment in generated bpl files

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

#94 - Corral internal error when --bit-precise --unroll 8 is invoked

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

#92 - Mutiple precedure declarations for a single function

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

#91 - Fix Boogie and Corral wrapper scripts so that each argument passed to

Pull Request - State: closed - Opened by delcypher over 9 years ago - 1 comment

#90 - Fix Boogie and Corral wrapper scripts so that each argument passed to

Pull Request - State: closed - Opened by delcypher over 9 years ago - 5 comments

#88 - Added Doxygen configuration file for generating documentation.

Pull Request - State: closed - Opened by jon-whit over 9 years ago

#87 - Boogie type error when verifying function contracts.

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

#86 - Model arbitrary integer size

Issue - State: closed - Opened by shaobo-he over 9 years ago - 17 comments
Labels: bug, wontfix

#85 - Feature/threaded tests

Pull Request - State: closed - Opened by jon-whit over 9 years ago - 1 comment

#84 - Other types of nondeterministic values.

Issue - State: closed - Opened by michael-emmi over 9 years ago

#83 - Parallelizing execution of regressions in regtest.py

Issue - State: closed - Opened by zvonimir over 9 years ago - 3 comments
Labels: enhancement

#82 - Added Jenkins Build Status Icon

Pull Request - State: closed - Opened by jon-whit over 9 years ago

#81 - Added Jenkins Build Status Icon

Pull Request - State: closed - Opened by jon-whit over 9 years ago

#80 - Added Jenkins Build Status Icon

Pull Request - State: closed - Opened by jon-whit over 9 years ago

#79 - Negative numbers cause problems with bit-precise

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

#78 - Fixed NUnit installation for the Boogie build process.

Pull Request - State: closed - Opened by jon-whit over 9 years ago

#77 - Pointer Tests Fail and Timeout

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

#76 - support for CVC4

Issue - State: closed - Opened by pdeligia over 9 years ago - 5 comments
Labels: enhancement

#75 - Initialization Function Support

Pull Request - State: closed - Opened by MontyCarter over 9 years ago - 1 comment

#74 - Feature/jenkins ci

Pull Request - State: closed - Opened by jon-whit over 9 years ago - 2 comments

#73 - smack gives erratic result when data can overflow

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

#72 - Concrete values of variables missing in error traces

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

#71 - SMACK can generate inconsistent axioms on variables using the ``unique`` keyword

Issue - State: closed - Opened by delcypher over 9 years ago - 3 comments
Labels: bug

#70 - bool-int type mismatch in assignment

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

#69 - Organize regression system

Issue - State: closed - Opened by zvonimir over 9 years ago - 1 comment
Labels: refactoring

#68 - Malloc, alloc, and free should probably be inlined when Boogie is called without unrolling

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

#67 - Repeating variables in modifies clauses

Issue - State: closed - Opened by zvonimir over 9 years ago - 5 comments
Labels: bug

#66 - Include NaN in floating point modelling

Issue - State: closed - Opened by delcypher over 9 years ago - 10 comments
Labels: bug

#65 - Added '-y' flag to the command 'add-apt-repository'.

Pull Request - State: closed - Opened by jon-whit over 9 years ago - 1 comment

#64 - Set up continuous integration for SMACK

Issue - State: closed - Opened by zvonimir over 9 years ago - 7 comments
Labels: enhancement

#63 - Cleaning up smack.h - do we still need boogie_si_record_int commented out stuff?

Issue - State: closed - Opened by zvonimir over 9 years ago - 1 comment
Labels: refactoring

#62 - Division operation for bitvectors

Issue - State: closed - Opened by shaobo-he over 9 years ago - 1 comment
Labels: question

#61 - No time limit for Corral

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

#60 - Literal translation error for integers of which size shorter than 32

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

#59 - Global variables not cleaned up after being optimized

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

#58 - Turn assert and assume statements into macros

Issue - State: closed - Opened by zvonimir over 9 years ago - 3 comments
Labels: enhancement

#57 - Support projects with multiple files

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

#56 - Bit-vector extension for SMACK

Pull Request - State: closed - Opened by shaobo-he over 9 years ago

#55 - Implement function pointers of vararg functions properly

Issue - State: open - Opened by zvonimir almost 10 years ago
Labels: enhancement

#54 - Soundly model integer overflow

Issue - State: closed - Opened by zvonimir almost 10 years ago - 8 comments
Labels: enhancement

#53 - Leverage llvm.assume intrinsic in SMACK

Issue - State: closed - Opened by zvonimir almost 10 years ago - 4 comments
Labels: enhancement

#52 - Make boogie and corral outputs uniform

Issue - State: closed - Opened by zvonimir almost 10 years ago - 1 comment
Labels: enhancement

#51 - Replace __SMACK_assert/assume with just assert/assume

Issue - State: closed - Opened by zvonimir almost 10 years ago
Labels: refactoring

#50 - Loads and stores of floats.

Issue - State: closed - Opened by michael-emmi about 10 years ago - 1 comment

#49 - `llvm2bpl.py` failure

Issue - State: closed - Opened by michael-emmi about 10 years ago - 11 comments

#48 - `smackgen.py` fails when input file is llvm bitcode

Issue - State: closed - Opened by michael-emmi about 10 years ago - 5 comments

#47 - Mysterious failing assertion with passing struct arguments.

Issue - State: closed - Opened by michael-emmi over 10 years ago - 8 comments

#46 - Free cannot be passed as a function pointer

Issue - State: closed - Opened by zvonimir over 10 years ago - 1 comment
Labels: bug

#45 - Source function or global variable name matches a Boogie keyword

Issue - State: closed - Opened by zvonimir over 10 years ago - 2 comments
Labels: bug

#44 - Does SMACK unroll loops? Or does it try to infer loop invariants in some cases?

Issue - State: closed - Opened by rsinha over 10 years ago - 3 comments
Labels: enhancement

#43 - LLVM cmpxchg

Issue - State: closed - Opened by michael-emmi over 10 years ago - 5 comments
Labels: bug

#42 - Pointers to distinct regions should be distinct.

Issue - State: closed - Opened by michael-emmi over 10 years ago - 4 comments
Labels: enhancement

#41 - Struct initialization ignored.

Issue - State: closed - Opened by michael-emmi over 10 years ago
Labels: enhancement

#39 - Problem with building LLVM on cygwin with cmake

Issue - State: closed - Opened by zvonimir over 10 years ago - 2 comments
Labels: bug, wontfix

#38 - Write cmake-based build scripts

Issue - State: closed - Opened by zvonimir over 10 years ago
Labels: enhancement

#37 - Size axioms for struct constants causing inconsistencies

Issue - State: closed - Opened by zvonimir over 10 years ago - 3 comments

#36 - Inconsistent axioms with extern global variables

Issue - State: closed - Opened by michael-emmi over 10 years ago
Labels: bug

#35 - errror: more than one declaration of function/procedure

Issue - State: closed - Opened by dvalps over 10 years ago

#34 - Error when generating output Boogie file: Assertion 'isInt ( c) failed'

Issue - State: closed - Opened by dvalps over 10 years ago - 1 comment
Labels: duplicate

#33 - Adding support for bitvectors

Issue - State: closed - Opened by zvonimir almost 11 years ago - 4 comments
Labels: enhancement

#32 - smack.so: undefined symbol: _ZN4llvm9DebugFlagE

Issue - State: closed - Opened by thorstent almost 11 years ago - 1 comment

#31 - Poor handling of uninitialized variables

Issue - State: closed - Opened by michael-emmi almost 11 years ago - 5 comments
Labels: wontfix

#29 - Failures on Mavericks

Issue - State: closed - Opened by ethulhu almost 11 years ago - 5 comments
Labels: bug

#28 - No support for functions that return a structure

Issue - State: closed - Opened by zvonimir almost 11 years ago - 4 comments

#27 - Struct assignment not handled properly - missing static initializer

Issue - State: closed - Opened by zvonimir almost 11 years ago
Labels: bug

#26 - Problem loading smack.so with `opt -load smack.so`

Issue - State: closed - Opened by linser almost 11 years ago

#25 - Scripts failing SILENTLY when there is a problem.

Issue - State: closed - Opened by michael-emmi almost 11 years ago - 4 comments
Labels: enhancement

#24 - Upgrade to LLVM 3.3

Issue - State: closed - Opened by zvonimir almost 11 years ago
Labels: enhancement

#23 - ntdrivers-simplified regressions are failing

Issue - State: closed - Opened by zvonimir almost 11 years ago
Labels: bug

#22 - Uninitialized variables should have possibly-distinct values.

Issue - State: open - Opened by michael-emmi about 11 years ago - 7 comments
Labels: enhancement

#21 - Static global assignments are ignored.

Issue - State: closed - Opened by michael-emmi about 11 years ago - 1 comment
Labels: enhancement

#20 - Implement a memory model that is split based on alias analysis results

Issue - State: closed - Opened by zvonimir about 11 years ago
Labels: enhancement

#19 - Make SMACK's and Corral's source line annotations compatible

Issue - State: closed - Opened by zvonimir about 11 years ago - 1 comment
Labels: enhancement

#18 - Add support for Corral into SMACK's scripts

Issue - State: closed - Opened by zvonimir about 11 years ago
Labels: enhancement

#17 - memset and memcpy are not supported

Issue - State: closed - Opened by zvonimir over 11 years ago - 2 comments
Labels: enhancement

#16 - Function declarations are currently being ignored

Issue - State: closed - Opened by zvonimir over 11 years ago
Labels: bug

#15 - Map Boogie error trace back to the C source line numbers

Issue - State: closed - Opened by zvonimir over 11 years ago - 1 comment
Labels: enhancement

#14 - What to do when we must make unsound translational choices?

Issue - State: open - Opened by michael-emmi over 11 years ago - 6 comments

#13 - "Currently only up to 5 var arg parameters are supported"

Issue - State: closed - Opened by michael-emmi over 11 years ago - 1 comment

#12 - make install fails when installed files already exist.

Issue - State: closed - Opened by michael-emmi over 11 years ago - 4 comments

#11 - Compilation errors on Ubuntu with llvm-3.2-dev package

Issue - State: closed - Opened by michael-emmi over 11 years ago - 1 comment

#10 - Implement FunExpr class

Issue - State: closed - Opened by zvonimir over 11 years ago - 1 comment
Labels: refactoring

#9 - Support for inttoptr not implemented

Issue - State: closed - Opened by zvonimir over 11 years ago - 4 comments
Labels: enhancement

#8 - Another error message at the end of a.bpl

Issue - State: closed - Opened by sergiodop92 over 11 years ago - 1 comment
Labels: bug

#7 - Error message at the end of a.bpl

Issue - State: closed - Opened by sergiodop92 over 11 years ago - 1 comment
Labels: bug

#6 - Global variables are not being translated properly

Issue - State: closed - Opened by zvonimir over 11 years ago
Labels: bug

#5 - autoconf/mkinstalldirs: No such file or directory

Issue - State: closed - Opened by ghost over 11 years ago - 3 comments

#4 - Add SMACK to rise4fun

Issue - State: closed - Opened by zvonimir over 11 years ago - 1 comment
Labels: enhancement

#3 - Add support for function pointers

Issue - State: closed - Opened by zvonimir over 11 years ago
Labels: enhancement

#2 - Build a better infrastructure for regression testing

Issue - State: closed - Opened by zvonimir over 11 years ago - 1 comment
Labels: enhancement

#1 - Clean up scripts for generating bpl code and for running SMACK

Issue - State: closed - Opened by zvonimir over 11 years ago
Labels: refactoring