| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | fixed an issue with parsing floating points |  Checkmate50 | 2016-07-19 |
| | | |||
| * | Added and briefly tested the updated syntax. NaN/oo not supported yet | Checkmate50 | 2016-07-19 |
| | | |||
| * | rebuilt scanner and parser via coco | Checkmate50 | 2016-07-16 |
| | | |||
| * | Merging complete. Everything looks good *crosses fingers* | Checkmate50 | 2016-06-06 |
| | | |||
| * | 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 | ||
| * | added general floating point mantissa and exponent management | Dietrich | 2015-05-04 |
| | | |||
| * | added float type to the set array in Parser | Dietrich | 2015-04-26 |
| | | |||
| * | removed comments from Scanner.cs, changed the value of the float token kind ↵ | Dietrich | 2015-04-26 |
| | | | | | to 97/98 (from 135/136) | ||
| * | added float type to Arithmetic Expression and added a new float test | Dietrich | 2015-04-26 |
| | | |||
| * | added a collection of console writes for debugging. These should be removed ↵ | Dietrich | 2015-04-20 |
| | | | | | in a future commit | ||
| * | Added float type to the Parser and Scanner | Dietrich | 2015-04-20 |
| | | |||
| * | Scanner generation with Coco |  0biha | 2014-12-24 |
| | | |||
| * | Made invariant of class 'Scanner' robust by changing the design (replaced ↵ | 0biha | 2014-12-23 |
| | | | | | public field by private field + getter/setter). | ||
| * | Did more refactoring. | wuestholz | 2014-09-23 |
| | | |||
| * | Added /useBaseNameForFile command line argument. The Scanner |  Dan Liew | 2014-04-06 |
| | | | | | | | | | | | | | | and Parser constructors have been modified to take an optional argument specifying this and the ExecutionEngine passes for that value CommandLineOptions.Clo.UseBaseNameForFileName This option when true causes the basename of file to be used inside created Tokens instead of what the user passed on the command line which might be a relative or absolute path. The motivation for adding this option is that it is needed for the lit driven tests so that the output of Boogie can be reliably checked. | ||
| * | added syntax for par call and ParCallCmd | qadeer | 2013-12-16 |
| | | |||
| * | added parallel calls |  Unknown | 2013-03-01 |
| | | |||
| * | removed call forall and * args to calls | Unknown | 2013-02-23 |
| | | |||
| * | Boogie: added type 'real' with overloaded arithmetic operations plus real ↵ | boehmes | 2012-09-27 |
| | | | | | | | | | | division '/' and (uninterpreted) real exponentiation '**', real literals and coercion functions 'int' and 'real'; Integer operations 'div' and 'mod' are now mapped to corresponding SMT-LIB operations instead of treating them uninterpreted; Made unary minus valid Boogie syntax again (the expression '- e' used to be rewritten by the parser to '0 - e', now this is done when generating VCs); Extended the BigDec class with additional functionality; Added test cases for SMT-LIB prover backend (the Z3 API interface has been adapted accordingly, but is untested) | ||
| * | Boogie: new syntax for integer division and modulus: use div and mod instead ↵ | boehmes | 2012-09-27 |
| | | | | | of / and % | ||
| * | Boogie: Simplified (and liberalized) parsing of string literals as attribute ↵ |  Unknown | 2012-03-12 |
| | | | | | parameters | ||
| * | updated Boogie strings so that they can refer to \" (and more) |  qadeer | 2012-03-12 |
| | | | | | fixed BCT :value | ||
| * | Updated the Parser.cs and Scanner.cs files in Boogie and Dafny and removed ↵ | wuestholz | 2011-07-15 |
| | | | | | some trailing whitespace. | ||
| * | Factored out the ParserHelper class into a separate project and updated the ↵ | wuestholz | 2010-12-02 |
| | | | | | | | files generated by Coco/R. This was done to support sharing of the Coco/R .frame files with Spec#. | ||
| * | Boogie: | rustanleino | 2010-10-26 |
| | | | | | | | | | | * Updated Parser.cs/Scanner.cs to use new .frame files from boogiepartners. * It changes, for example, "syntax error:" to just "error:", so adjusted expected Test outputs. Dafny: * Ditto for its Parser.cs/Scanner.cs. * Added ability to provide a custom Errors handler for scanner/parser. * Added Test/dafny1/Cubes.dfy | ||
| * | Boogie: Committing changed source files | tabarbe | 2010-08-20 |
| | | |||
| * | Boogie: Renaming core sources in preparation for port commit | tabarbe | 2010-08-20 |
 |
index : debian-boogie | |
| Debian packaging for Boogie |
| summaryrefslogtreecommitdiff |