summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Merge branch 'upstream' into dfsg_freedfsg_freeGravatar Benjamin Barenblat2016-10-29
|\
| * White space deltas. (I'm not sure why git thought I had changes in these ↵Gravatar Rustan Leino2016-08-17
| | | | | | | | files, but I suspect it has to do with line endings.)
| * Merge pull request #35 from Checkmate50/masterGravatar RustanLeino2016-08-17
| |\ | | | | | | Floating Point Support
| * \ Merge pull request #42 from BarryBo/masterGravatar RustanLeino2016-08-15
| |\ \ | | | | | | | | Fix deadlock in the new thread scheduler
| | * | Fix deadlock in the new thread schedulerGravatar BarryBo2016-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/masterGravatar RustanLeino2016-08-01
| |\| | | | | | | | | | Run Boogie code on threads with large stacks
| | | * fixed an error where a -0 was not interpreted as a negative numberGravatar Checkmate502016-07-23
| | | |
| | * | Run Boogie code on threads with large stacksGravatar BarryBo2016-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 testGravatar Checkmate502016-07-22
| | |
| | * fixed the syntax on former tests and added two fp constant translation testsGravatar Checkmate502016-07-22
| | |
| | * Removed automatic exponent shiftingGravatar Checkmate502016-07-22
| | |
| | * fixed an issue with parsing floating pointsGravatar Checkmate502016-07-19
| | |
| | * Modified the float tests to match the updated syntaxGravatar Checkmate502016-07-19
| | |
| | * fixed floatceiling functionGravatar Checkmate502016-07-19
| | |
| | * Added and briefly tested the updated syntax. NaN/oo not supported yetGravatar Checkmate502016-07-19
| | |
| * | updateGravatar Shaz Qadeer2016-07-19
| | |
| * | updateGravatar Shaz Qadeer2016-07-18
| | |
| | * Changed the syntax reading of the float typeGravatar Checkmate502016-07-16
| | |
| | * rebuilt scanner and parser via cocoGravatar Checkmate502016-07-16
| | |
| | * 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
| | |\ | | |/ | |/|
| | * minor changesGravatar Checkmate502016-06-06
| | |
| | * Merging complete. Everything looks good *crosses fingers*Gravatar Checkmate502016-06-06
| | |
| | * spacing changeGravatar Checkmate502016-06-06
| | |
| | * removed an unnecessary text fileGravatar Checkmate502016-06-06
| | |
| | * Polished up the floats test folder. Preparing to rebaseGravatar Checkmate502016-06-06
| | |
| | * finished testing, fixed several minor compiler bugsGravatar Checkmate502016-06-06
| | |
* | | Merge branch 'upstream' into dfsg_freeGravatar Benjamin Barenblat2016-06-05
|\ \ \
| | | * moved all the tests to the testing folderGravatar Checkmate502016-05-31
| | | |
| | | * 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
| | * | Add links to new documentation (not yet complete).Gravatar Dan Liew2016-04-20
| | | |
| | * | Rename DLLs to non-generic names by prefixing "Boogie". Project names andGravatar akashlal2016-04-15
| |/ / | | | | | | | | | namespaces remain the same.
* | | Make DFSG-cleanGravatar Benjamin Barenblat2016-03-31
| | |
| | * 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
| | |
| * | Merge branch 'master' of https://github.com/boogie-org/boogieGravatar Rustan Leino2016-02-12
| |\ \
| | * \ Merge pull request #30 from qunyanm/type-parameter-bug-fixGravatar RustanLeino2016-02-12
| | |\ \ | | | | | | | | | | Bug fix in determining whether a type parameter is bounded
| * | | | Merge branch 'master' of https://github.com/boogie-org/boogieGravatar Rustan Leino2016-02-12
| |\| | |
| * | | | (Honestly, I don't know what I'm doing. I'm trying to revert these changes, ↵Gravatar Rustan Leino2016-02-12
| | | | | | | | | | | | | | | | | | | | but Git doesn't actually say what sort of commit I'm doing. Well, here goes.)
| | * | | added an exampleGravatar Shaz Qadeer2016-02-09
| | | | |
| | * | | another fixGravatar Shaz Qadeer2016-01-26
| | | | |
| | * | | improved some of the annotationsGravatar Shaz Qadeer2016-01-21
| | | | |
| | * | | some fixesGravatar Shaz Qadeer2016-01-19
| | | | |
| | | * | 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.
| | * | updated the example to implement the allocation of thread identifiers;Gravatar Shaz Qadeer2016-01-17
| | | | | | | | | | | | | | | | | | | | this example provides another illustration of abstracting ordinary variables by linear variables