Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Move block predicator to VCGeneration | 2012-06-18 | |
| | |||
* | GPUVerify: implement is-a-constant analysis | 2012-06-15 | |
| | | | | | | | | | | | | | This analysis is used to generate race checking invariants for arbitrary (thread-level) constant offsets, in place of invariant generators for four specific constants (thread-id, global-id, 2D thread-id and 2D global-id) which are subsumed by the new analysis. The main motivation is to be able to recognise offsets used by word level accesses into byte arrays, which are formed from linear combinations of thread IDs and constants. This change allows us to remove the 2D and global size analyses, resulting in a 536-line net reduction in total code size. | ||
* | Merging again | 2012-06-07 | |
|\ | |||
| * | Trying to merge with recent changes, failing. | 2012-06-05 | |
| |\ | |||
| | * | Some changes to support expanded use of z3api. | 2012-06-05 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Should not affect function of other provers. There is an option added in Check.cs to allow creation of a Checker with a user-specified ProverContext. Also, some extension of z3api prover context to support conversion of Z3 formulas back to VCExpr. Finally, some experimental code, not enabled, to allow conversion of loops to recursion with "head recursion" rather than "tail recursion" (i.e., recursive call before loop body rather than after). | ||
* | | | Boogie: add /printCFG command line option, which prints each ↵ | 2012-06-06 | |
|/ / | | | | | | | implementation's CFG in Graphviz format | ||
* | | moved class Macro to Absy | 2012-06-04 | |
| | | | | | | | | | | cleanup up DefineMacro Changed SI to use macros for reach info | ||
* | | Merge | 2012-06-01 | |
|\ \ | |||
* | | | changed behavior of InlinedEnsures so that free ensures is skipped unless an ↵ | 2012-06-01 | |
| | | | | | | | | | | | | attribute called :assume is there | ||
| * | | 1. Fix for free ensures in inlined procedures. Becomes a skip instead of an ↵ | 2012-06-01 | |
|/ / | | | | | | | | | | | | | assume. 2. Fix for deterministic loop extraction, and a new regression. 3. All regressions (including Dafny) except houdini pass, it is most likely related to the free ensures change. | ||
* | | No need for extra attributes in ExtractLoops | 2012-05-28 | |
| | | |||
* | | Better interface for adding skipped calls, and | 2012-05-26 | |
| | | | | | | | | adding extra recursion bound to some procedures. | ||
* | | Merge | 2012-05-25 | |
|\ \ | |||
* | | | Adding an option for deterministicExtractLoops, that uses an alternate way ↵ | 2012-05-25 | |
| | | | | | | | | | | | | | | | | | | to extract loops into procedures. Unsound for concurrency. Added a test in extractLoops directory. | ||
| * | | Merge | 2012-05-24 | |
| |\ \ | |/ / |/| | | |||
| * | | more refactoring in stratified inlining | 2012-05-24 | |
| | | | |||
* | | | Boogie: document /typeEncoding:m | 2012-05-22 | |
|/ / | |||
* | | Boogie: handle absolute paths on *nix correctly | 2012-05-02 | |
| | | | | | | | | | | | | Specifically, if the directory separator character is '/' and an unrecognised command line parameter begins with '/', treat it as a file path rather than an option. | ||
* | | Get Boogie and GPUVerify to compile and run with Mono | 2012-05-02 | |
| | | |||
* | | added counterexample generation based on labels back to stratified inlining | 2012-05-01 | |
| | | |||
* | | UseLabels=false when stratified inline is on | 2012-04-29 | |
| | | |||
* | | removed proccopybounding code | 2012-04-28 | |
| | | | | | | | | stratified inliinig is now run always with /doNotUseLabels | ||
* | | removed lazy inlining | 2012-04-28 | |
| | | |||
* | | unsat core for houdini | 2012-04-27 | |
| | | |||
* | | Added functionality to "skip" procedures. Some cleanup. | 2012-04-12 | |
| | | |||
* | | Fixed bug with triply nested maps and polymorphism (reported as Item # 10218). | 2012-04-04 | |
| | | |||
* | | added nonUniformUnfolding option | 2012-04-03 | |
| | | |||
* | | deleted the option UseUnsatCoreForInlining | 2012-04-02 | |
| | | | | | | | | | | Split ApiChecker.CheckAssumptions into two different methods, one which computes the unsatCore and one which does not Further edits to the MaxSat code | ||
* | | Emit of invariants now prints out the invariant attributes also | 2012-03-26 | |
| | | |||
* | | added attributes to loop invariants | 2012-03-23 | |
| | | |||
* | | more type checking for datatypes | 2012-03-18 | |
| | | |||
* | | Boogie: Simplified (and liberalized) parsing of string literals as attribute ↵ | 2012-03-12 | |
| | | | | | | | | parameters | ||
* | | updated Boogie strings so that they can refer to \" (and more) | 2012-03-12 | |
| | | | | | | | | fixed BCT :value | ||
* | | make the call to ProcessDataTypeConstructors in the right place | 2012-03-11 | |
| | | |||
* | | Boogie: map the given filename stdin.bpl to standard input | 2012-03-09 | |
| | | |||
* | | various refactorings related to houdini | 2012-03-02 | |
| | | |||
* | | verbose mode for stratified inlining. | 2012-02-29 | |
| | | |||
* | | bug fixes related to using ControlFlowFunction instead of labels | 2012-02-23 | |
| | | |||
* | | using model instead of labels | 2012-02-23 | |
|/ | |||
* | verbose mode | 2012-02-19 | |
| | |||
* | Use DateTime.UtcNow instead of DateTime.Now | 2012-01-11 | |
| | | | | see http://blogs.msdn.com/b/kirillosenkov/archive/2012/01/10/datetime-utcnow-is-generally-preferable-to-datetime-now.aspx | ||
* | Boogie: output number of proof obligations (asserts) along with timing ↵ | 2012-01-09 | |
| | | | | information when using the /trace option | ||
* | made delegate a datatype | 2011-12-30 | |
| | | | | added a DatatypeConstructor class | ||
* | fixed problems with datatypes | 2011-12-29 | |
| | | | | | removed stale contracts in stratified inlining added test to datatypes | ||
* | fixed a completeness problem in houdini with inlining | 2011-12-18 | |
| | |||
* | Fixed the Boogie build. | 2011-12-16 | |
| | |||
* | Dafny: Made sure that error locations refer to the Dafny program, even if ↵ | 2011-12-15 | |
| | | | | the /print option is used. | ||
* | Boogie: Changed Expr.Not to keep swap arguments rather change direction of ↵ | 2011-12-12 | |
| | | | | operator when negating <, <=, >=, or > | ||
* | Merge | 2011-12-07 | |
|\ | |||
| * | Merge | 2011-12-07 | |
| |\ |