Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merging complete. Everything looks good *crosses fingers* | Checkmate50 | 2016-06-06 |
| | |||
* | finished testing, fixed several minor compiler bugs | 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 | ||
* | modified floating point syntax and modified floating point constants to use ↵ | Checkmate50 | 2016-03-17 |
| | | | | bitvector values | ||
* | Modified BigFloat and parser to accept correct SMT-LIB syntax | Checkmate50 | 2016-02-20 |
| | |||
* | Added several test cases and some basic documentation for fp usage | Checkmate50 | 2016-01-04 |
| | |||
* | Special fp types (such as infinity and NaN are now translated by boogie | Checkmate50 | 2015-11-29 |
| | |||
* | Floating point constants given as integers are now translated correctly | Checkmate50 | 2015-10-14 |
| | |||
* | Modified translation so that z3 runs with type checking for simple binary ↵ | Checkmate50 | 2015-10-14 |
| | | | | operations | ||
* | Modified BigFloat to avoid evaluating the floating point value before ↵ | Checkmate50 | 2015-09-23 |
| | | | | sending it to z3 | ||
* | Added initial support for float addition | Checkmate50 | 2015-09-17 |
| | |||
* | Float type now works correctly for simple variable declaration and comparison. | Dietrich | 2015-07-20 |
| | |||
* | Modified internal abstract float representation to allow user-defined ↵ | Dietrich | 2015-07-13 |
| | | | | mantissa and exponent | ||
* | added interpretation of floating point constants to the parser | Dietrich | 2015-05-18 |
| | |||
* | Made significant changes to internal representation of BigFloat. Remains a ↵ | Dietrich | 2015-05-07 |
| | | | | work in progress | ||
* | added decimal reading functionality to the float type | Dietrich | 2015-05-05 |
| | |||
* | added general floating point mantissa and exponent management | Dietrich | 2015-05-04 |
| | |||
* | integrated the named float type to act as a real in boogie | Dietrich | 2015-05-04 |
| | |||
* | Began adding the float type to VC expression | Dietrich | 2015-04-27 |
| | |||
* | Added float operations to AbsyExpr. Note that float operations work as real ↵ | Dietrich | 2015-04-27 |
| | | | | operations at the moment | ||
* | Finished up Parser modifications | Dietrich | 2015-04-27 |
| | |||
* | removed the last console writes (used for testing) | Dietrich | 2015-04-26 |
| | |||
* | Successfully parsed the float type | Dietrich | 2015-04-26 |
| | |||
* | 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 |
| | |||
* | renamed fp32 to BigFloat | Dietrich | 2015-04-20 |
| | |||
* | added minor commenting to Parser.cs | Dietrich | 2015-04-20 |
| | |||
* | 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 |
| | |||
* | added float tipe to AbsyExpr and IntervalDomain. The methods added may ↵ | Dietrich | 2015-04-20 |
| | | | | require later modification | ||
* | added float type definition to AbsyType and parser (parser definition may be ↵ | Dietrich | 2015-04-17 |
| | | | | unfinished) | ||
* | adding references to the floating point type wherever references to the real ↵ | Dietrich | 2015-04-17 |
| | | | | type exist. This remains a work in progress | ||
* | Added the fp32 class, copied from the previously existing BigDec class. No ↵ | Dietrich | 2015-04-17 |
| | | | | significant changes from BigDec have been made | ||
* | Patch by Jeroen Ketema. | Dan Liew | 2015-04-05 |
| | | | | | | Drop the “basic” block predication algorithm. Block predication is only used by GPUVerify, and then only in the “smart” version as the basic algorithm does not perform very well. As a consequence this code is essentially dead. | ||
* | VC gen for security properties | akashlal | 2015-04-05 |
| | |||
* | Patch by Jeroen Ketema | Dan Liew | 2015-03-27 |
| | | | | Expose information about the predicate assigned to the immediate dominator of a CFG node. | ||
* | Compute MustReach information lazily, on-demand | akashlal | 2015-03-16 |
| | |||
* | Added MustReach information to VC gen | akashlal | 2015-03-11 |
| | |||
* | If using -proverLog: make sure we flush after writing every line | Dan Liew | 2015-03-10 |
| | | | | | | | | | otherwise if either of the following happens * if the solver hangs and we do CTRL+C * if Boogie crashes then some lines will be missing from the log. | ||
* | Work around bug in Z3 4.3.2 and newer (https://z3.codeplex.com/workitem/188) | Dan Liew | 2015-03-10 |
| | | | | | | where setting produce-unsat-cores to true has no effect unless the option is set last. This makes the Test/houdini/testUnsatCore.bpl test pass under Linux using Z3 4.3.2 | ||
* | Fix bug in BigDec.FloorCeiling() which gave the wrong answers for | Dan Liew | 2015-03-10 |
| | | | | | negative numbers. I have decided that this method will floor towards negative infinity rather than zero to match SMT-LIBv2's to_int function. | ||
* | fixed crash reported by Dan. | qadeer | 2015-03-02 |
| | | | | DoModSetAnalysis needs to run before the linear and mover type checking. | ||
* | Parse Bv values | akashlal | 2015-03-02 |
| | |||
* | Fix using "mkbv" as a variable name in a boogie program. This was | Dan Liew | 2015-02-27 |
| | | | | | taken from ``bv_decl_plugin::get_op_names(...)`` in ``src/ast/bv_decl_plugin.cpp`` in the Z3 4.3.2 source code. | ||
* | Fix using reserved Z3 keywords for real/int arithmetic operators. These are ↵ | Dan Liew | 2015-02-27 |
| | | | | | | | taken from `` arith_decl_plugin::get_op_names(...)`` from ``src/ast/arith_decl_plugin.cpp`` in the Z3 4.3.2 source code. | ||
* | Fix using reserved Z3 keywords for float operators. These are taken | Dan Liew | 2015-02-27 |
| | | | | | from ``float_decl_plugin::get_op_names(..)`` in ``src/ast/float_decl_plugin.cpp`` from the Z3 4.3.2 source code. | ||
* | Merge. | Dan Liew | 2015-02-18 |
|\ | |||
* | | Fix bug where some reserved Z3 keywords were not sanitized | Dan Liew | 2015-02-18 |
| | | | | | | | | when generating the VC. | ||
| * | Eliminated calls to deprecated method. | wuestholz | 2015-02-18 |
| | |