summaryrefslogtreecommitdiff
path: root/Source
Commit message (Collapse)AuthorAge
* 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
* modified floating point syntax and modified floating point constants to use ↵Gravatar Checkmate502016-03-17
| | | | bitvector values
* Modified BigFloat and parser to accept correct SMT-LIB syntaxGravatar Checkmate502016-02-20
|
* Added several test cases and some basic documentation for fp usageGravatar Checkmate502016-01-04
|
* Special fp types (such as infinity and NaN are now translated by boogieGravatar Checkmate502015-11-29
|
* 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
* Modified BigFloat to avoid evaluating the floating point value before ↵Gravatar Checkmate502015-09-23
| | | | sending it to z3
* Added initial support for float additionGravatar Checkmate502015-09-17
|
* Float type now works correctly for simple variable declaration and comparison.Gravatar Dietrich2015-07-20
|
* Modified internal abstract float representation to allow user-defined ↵Gravatar Dietrich2015-07-13
| | | | mantissa and exponent
* added interpretation of floating point constants to the parserGravatar Dietrich2015-05-18
|
* Made significant changes to internal representation of BigFloat. Remains a ↵Gravatar Dietrich2015-05-07
| | | | work in progress
* added decimal reading functionality to the float typeGravatar Dietrich2015-05-05
|
* added general floating point mantissa and exponent managementGravatar Dietrich2015-05-04
|
* integrated the named float type to act as a real in boogieGravatar Dietrich2015-05-04
|
* Began adding the float type to VC expressionGravatar Dietrich2015-04-27
|
* Added float operations to AbsyExpr. Note that float operations work as real ↵Gravatar Dietrich2015-04-27
| | | | operations at the moment
* Finished up Parser modificationsGravatar Dietrich2015-04-27
|
* removed the last console writes (used for testing)Gravatar Dietrich2015-04-26
|
* Successfully parsed the float typeGravatar Dietrich2015-04-26
|
* added float type to the set array in ParserGravatar Dietrich2015-04-26
|
* removed comments from Scanner.cs, changed the value of the float token kind ↵Gravatar Dietrich2015-04-26
| | | | to 97/98 (from 135/136)
* added float type to Arithmetic Expression and added a new float testGravatar Dietrich2015-04-26
|
* renamed fp32 to BigFloatGravatar Dietrich2015-04-20
|
* added minor commenting to Parser.csGravatar Dietrich2015-04-20
|
* added a collection of console writes for debugging. These should be removed ↵Gravatar Dietrich2015-04-20
| | | | in a future commit
* Added float type to the Parser and ScannerGravatar Dietrich2015-04-20
|
* added float tipe to AbsyExpr and IntervalDomain. The methods added may ↵Gravatar Dietrich2015-04-20
| | | | require later modification
* added float type definition to AbsyType and parser (parser definition may be ↵Gravatar Dietrich2015-04-17
| | | | unfinished)
* adding references to the floating point type wherever references to the real ↵Gravatar Dietrich2015-04-17
| | | | type exist. This remains a work in progress
* Added the fp32 class, copied from the previously existing BigDec class. No ↵Gravatar Dietrich2015-04-17
| | | | significant changes from BigDec have been made
* Patch by Jeroen Ketema.Gravatar Dan Liew2015-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 propertiesGravatar akashlal2015-04-05
|
* Patch by Jeroen KetemaGravatar Dan Liew2015-03-27
| | | | Expose information about the predicate assigned to the immediate dominator of a CFG node.
* Compute MustReach information lazily, on-demandGravatar akashlal2015-03-16
|
* Added MustReach information to VC genGravatar akashlal2015-03-11
|
* If using -proverLog: make sure we flush after writing every lineGravatar Dan Liew2015-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)Gravatar Dan Liew2015-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 forGravatar Dan Liew2015-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.Gravatar qadeer2015-03-02
| | | | DoModSetAnalysis needs to run before the linear and mover type checking.
* Parse Bv valuesGravatar akashlal2015-03-02
|
* Fix using "mkbv" as a variable name in a boogie program. This wasGravatar Dan Liew2015-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 ↵Gravatar Dan Liew2015-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 takenGravatar Dan Liew2015-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.Gravatar Dan Liew2015-02-18
|\
* | Fix bug where some reserved Z3 keywords were not sanitizedGravatar Dan Liew2015-02-18
| | | | | | | | when generating the VC.
| * Eliminated calls to deprecated method.Gravatar wuestholz2015-02-18
| |
| * Added a setter for CommandLineOptions.ProverOptions and fixed several contracts.Gravatar wuestholz2015-02-18
|/
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 23:46:22 +0000