Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge branch 'upstream' into dfsg_freedfsg_free | Benjamin Barenblat | 2016-10-29 |
|\ | |||
| * | White space deltas. (I'm not sure why git thought I had changes in these ↵ | Rustan Leino | 2016-08-17 |
| | | | | | | | | files, but I suspect it has to do with line endings.) | ||
| * | Merge pull request #35 from Checkmate50/master | RustanLeino | 2016-08-17 |
| |\ | | | | | | | Floating Point Support | ||
| * \ | Merge pull request #42 from BarryBo/master | RustanLeino | 2016-08-15 |
| |\ \ | | | | | | | | | Fix deadlock in the new thread scheduler | ||
| | * | | Fix deadlock in the new thread scheduler | BarryBo | 2016-08-12 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Fix deadlock where a Boogie task schedules a task and waits on it. The .NET threadpool creates more threads than cores, up to a limit, which hides the issue. The new policy did not account for recursion and caused the newly-created tasks to wait forever for the earlier ones to complete. | ||
| * | | | Merge pull request #41 from BarryBo/master | RustanLeino | 2016-08-01 |
| |\| | | | | | | | | | | Run Boogie code on threads with large stacks | ||
| | | * | fixed an error where a -0 was not interpreted as a negative number | Checkmate50 | 2016-07-23 |
| | | | | |||
| | * | | Run Boogie code on threads with large stacks | BarryBo | 2016-07-22 |
| |/ / | | | | | | | | | | | | | | | | | | | Replace TaskScheduler.Default by a custom TaskScheduler. The .Default uses threadpool threads whose stack size is controlled by the host EXE header. The new ThreadTaskScheduler give Boogie control over the stack size, and defaults to 16mb. | ||
| | * | corrected minor error in test | Checkmate50 | 2016-07-22 |
| | | | |||
| | * | fixed the syntax on former tests and added two fp constant translation tests | Checkmate50 | 2016-07-22 |
| | | | |||
| | * | Removed automatic exponent shifting | Checkmate50 | 2016-07-22 |
| | | | |||
| | * | fixed an issue with parsing floating points | Checkmate50 | 2016-07-19 |
| | | | |||
| | * | Modified the float tests to match the updated syntax | Checkmate50 | 2016-07-19 |
| | | | |||
| | * | fixed floatceiling function | Checkmate50 | 2016-07-19 |
| | | | |||
| | * | Added and briefly tested the updated syntax. NaN/oo not supported yet | Checkmate50 | 2016-07-19 |
| | | | |||
| * | | update | Shaz Qadeer | 2016-07-19 |
| | | | |||
| * | | update | Shaz Qadeer | 2016-07-18 |
| | | | |||
| | * | Changed the syntax reading of the float type | Checkmate50 | 2016-07-16 |
| | | | |||
| | * | rebuilt scanner and parser via coco | Checkmate50 | 2016-07-16 |
| | | | |||
| | * | change to update | Checkmate50 | 2016-06-07 |
| | | | |||
| | * | removed an unnecessary type checking addition | Checkmate50 | 2016-06-07 |
| | | | |||
| | * | fixed some merging issues | Checkmate50 | 2016-06-07 |
| | | | |||
| | * | resolving conflicts | Checkmate50 | 2016-06-06 |
| | |\ | | |/ | |/| | |||
| | * | minor changes | Checkmate50 | 2016-06-06 |
| | | | |||
| | * | Merging complete. Everything looks good *crosses fingers* | Checkmate50 | 2016-06-06 |
| | | | |||
| | * | spacing change | Checkmate50 | 2016-06-06 |
| | | | |||
| | * | removed an unnecessary text file | Checkmate50 | 2016-06-06 |
| | | | |||
| | * | Polished up the floats test folder. Preparing to rebase | Checkmate50 | 2016-06-06 |
| | | | |||
| | * | finished testing, fixed several minor compiler bugs | Checkmate50 | 2016-06-06 |
| | | | |||
* | | | Merge branch 'upstream' into dfsg_free | Benjamin Barenblat | 2016-06-05 |
|\ \ \ | |||
| | | * | moved all the tests to the testing folder | Checkmate50 | 2016-05-31 |
| | | | | |||
| | | * | Initial round of testing works with new syntax. Fixed an error where ↵ | Checkmate50 | 2016-05-31 |
| | | | | | | | | | | | | | | | | floating points could not be given as a function argument | ||
| | * | | Add links to new documentation (not yet complete). | Dan Liew | 2016-04-20 |
| | | | | |||
| | * | | Rename DLLs to non-generic names by prefixing "Boogie". Project names and | akashlal | 2016-04-15 |
| |/ / | | | | | | | | | | namespaces remain the same. | ||
* | | | Make DFSG-clean | Benjamin Barenblat | 2016-03-31 |
| | | | |||
| | * | modified floating point syntax and modified floating point constants to use ↵ | Checkmate50 | 2016-03-17 |
| | | | | | | | | | | | | bitvector values | ||
| * | | Improve support for identifying unnecessary assumes. | Valentin Wüstholz | 2016-03-09 |
| | | | |||
| * | | Add support for weights on soft assumes. | Valentin Wüstholz | 2016-03-07 |
| | | | |||
| * | | Improve support for optimization and identifying unnecessary assumes. | Valentin Wüstholz | 2016-03-03 |
| | | | |||
| | * | Modified BigFloat and parser to accept correct SMT-LIB syntax | Checkmate50 | 2016-02-20 |
| | | | |||
| * | | Merge branch 'master' of https://github.com/boogie-org/boogie | Rustan Leino | 2016-02-12 |
| |\ \ | |||
| | * \ | Merge pull request #30 from qunyanm/type-parameter-bug-fix | RustanLeino | 2016-02-12 |
| | |\ \ | | | | | | | | | | | Bug fix in determining whether a type parameter is bounded | ||
| * | | | | Merge branch 'master' of https://github.com/boogie-org/boogie | Rustan Leino | 2016-02-12 |
| |\| | | | |||
| * | | | | (Honestly, I don't know what I'm doing. I'm trying to revert these changes, ↵ | Rustan Leino | 2016-02-12 |
| | | | | | | | | | | | | | | | | | | | | but Git doesn't actually say what sort of commit I'm doing. Well, here goes.) | ||
| | * | | | added an example | Shaz Qadeer | 2016-02-09 |
| | | | | | |||
| | * | | | another fix | Shaz Qadeer | 2016-01-26 |
| | | | | | |||
| | * | | | improved some of the annotations | Shaz Qadeer | 2016-01-21 |
| | | | | | |||
| | * | | | some fixes | Shaz Qadeer | 2016-01-19 |
| | | | | | |||
| | | * | | Bug fix in determining whether a type parameter is bounded | qunyanm | 2016-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. | ||
| | * | | updated the example to implement the allocation of thread identifiers; | Shaz Qadeer | 2016-01-17 |
| | | | | | | | | | | | | | | | | | | | | this example provides another illustration of abstracting ordinary variables by linear variables |