summaryrefslogtreecommitdiff
path: root/Source
Commit message (Collapse)AuthorAge
* change to updateGravatar Checkmate502016-06-07
|
* removed an unnecessary type checking additionGravatar Checkmate502016-06-07
|
* fixed some merging issuesGravatar Checkmate502016-06-07
|
* resolving conflictsGravatar Checkmate502016-06-06
|\
* | Merging complete. Everything looks good *crosses fingers*Gravatar Checkmate502016-06-06
| |
* | finished testing, fixed several minor compiler bugsGravatar Checkmate502016-06-06
| |
* | Initial round of testing works with new syntax. Fixed an error where ↵Gravatar Checkmate502016-05-31
| | | | | | | | floating points could not be given as a function argument
| * Rename DLLs to non-generic names by prefixing "Boogie". Project names andGravatar akashlal2016-04-15
| | | | | | | | namespaces remain the same.
* | modified floating point syntax and modified floating point constants to use ↵Gravatar Checkmate502016-03-17
| | | | | | | | bitvector values
| * Improve support for identifying unnecessary assumes.Gravatar Valentin Wüstholz2016-03-09
| |
| * Add support for weights on soft assumes.Gravatar Valentin Wüstholz2016-03-07
| |
| * Improve support for optimization and identifying unnecessary assumes.Gravatar Valentin Wüstholz2016-03-03
| |
* | Modified BigFloat and parser to accept correct SMT-LIB syntaxGravatar Checkmate502016-02-20
| |
| * Bug fix in determining whether a type parameter is boundedGravatar qunyanm2016-01-19
| | | | | | | | | | | | When checking whether a type parameter could be determined from the bound variable types, we mistakenly compare equality between a TypeVarable and a VCExprVar, instead of between two VCExprVars.
* | Added several test cases and some basic documentation for fp usageGravatar Checkmate502016-01-04
| |
| * Minor changeGravatar Valentin Wüstholz2015-12-29
| |
| * Fix issue with ids for assume-statements.Gravatar Valentin Wüstholz2015-12-28
| |
| * Improve precision of abstract interpreter for modulo operations.Gravatar Valentin Wüstholz2015-12-28
| |
| * Enable optimization for more prover queries.Gravatar Valentin Wüstholz2015-12-27
| |
| * Remove unused file.Gravatar Valentin Wüstholz2015-12-03
| |
| * Remove workaround for older versions of Z3.Gravatar Valentin Wüstholz2015-12-02
| |
| * Use the EndCurly token when creating the ReturnCmd for unifiedExitGravatar qunyanm2015-12-02
| | | | | | | | | | | | | | | | When there are more than one exit blocks, an unified exit block is created which includes a ReturnCmd. However, the ReturnCmd is created with NoToken. This causes the line/column number reported for a failed postcondition to be (0,0). The right token should be the EndCurly since the ReturnCmd is in the exit block.
* | Special fp types (such as infinity and NaN are now translated by boogieGravatar Checkmate502015-11-29
| |
| * Add simplified may-unverified analysis and instrumentation.Gravatar Valentin Wüstholz2015-11-20
| |
| * Fix issue with partially-verified assertions.Gravatar Valentin Wüstholz2015-11-19
| |
| * Minor changesGravatar Valentin Wüstholz2015-11-19
| |
| * Add experimental support for optimization (requires Z3 build after changeset ↵Gravatar Valentin Wüstholz2015-11-18
| | | | | | | | 9cba63c31f6f1466dd4ef442bb840d1ab84539c7).
| * Fix issue #25.Gravatar Valentin Wüstholz2015-11-17
| |
| * Add support for identifying unnecessary assumes.Gravatar Valentin Wüstholz2015-11-16
| |
| * Document the new behaviour of the ``-proc:`` command line optionGravatar Dan Liew2015-10-31
| | | | | | | | in the output of Boogie's help.
| * Added wild card matching for /proc flagGravatar Shaobo2015-10-31
| |
| * Add support for annotating implementations with k-ind. depth.Gravatar Valentin Wüstholz2015-10-29
| |
| * fix for deterministicExtractLoops for nested loopsGravatar Shuvendu Lahiri2015-10-27
| |
| * Bug fix for deterministExtractLoops for Shaobo's exampleGravatar Shuvendu Lahiri2015-10-26
| |
| * bug fix in the type checking of calls to atomic proceduresGravatar Shaz Qadeer2015-10-16
| |
* | Floating point constants given as integers are now translated correctlyGravatar Checkmate502015-10-14
| |
* | Modified translation so that z3 runs with type checking for simple binary ↵Gravatar Checkmate502015-10-14
| | | | | | | | operations
| * bug fixGravatar Shaz Qadeer2015-10-09
| |
| * removed an extraneous warningGravatar Shaz Qadeer2015-10-08
| |
| * Merge branch 'master' of https://github.com/boogie-org/boogieGravatar Shaz Qadeer2015-10-01
| |\
| * | added a fix to check all layers: created layer of actions or layers inGravatar Shaz Qadeer2015-10-01
| | | | | | | | | | | | requires, ensures, or asserts
| | * Improve output for diagnosing timeouts.Gravatar Valentin Wüstholz2015-10-01
| |/
| * another fix requested by ChrisGravatar Shaz Qadeer2015-10-01
| | | | | | | | verification is performed now for all created layers
| * Improve output for diagnosing timeouts.Gravatar Valentin Wüstholz2015-09-30
| |
| * updateGravatar Shaz Qadeer2015-09-28
| |
| * cleaned up some namesGravatar Shaz Qadeer2015-09-28
| |
| * a bug fixGravatar Shaz Qadeer2015-09-27
| |
| * fixed a small bugGravatar Shaz Qadeer2015-09-27
| |
| * removed a warningGravatar Shaz Qadeer2015-09-26
| |
| * added introduced and ghost local variablesGravatar Shaz Qadeer2015-09-25
| |