summaryrefslogtreecommitdiff
path: root/Source/Core
Commit message (Expand)AuthorAge
* modified floating point syntax and modified floating point constants to use b...Gravatar Checkmate502016-03-17
* Modified BigFloat and parser to accept correct SMT-LIB syntaxGravatar Checkmate502016-02-20
* Special fp types (such as infinity and NaN are now translated by boogieGravatar Checkmate502015-11-29
* Modified translation so that z3 runs with type checking for simple binary ope...Gravatar Checkmate502015-10-14
* Modified BigFloat to avoid evaluating the floating point value before sending...Gravatar Checkmate502015-09-23
* 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 mantiss...Gravatar Dietrich2015-07-13
* added interpretation of floating point constants to the parserGravatar Dietrich2015-05-18
* added decimal reading functionality to the float typeGravatar Dietrich2015-05-05
* added general floating point mantissa and exponent managementGravatar 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
* 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 t...Gravatar Dietrich2015-04-26
* 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
* Added float type to the Parser and ScannerGravatar Dietrich2015-04-20
* added float tipe to AbsyExpr and IntervalDomain. The methods added may requi...Gravatar Dietrich2015-04-20
* added float type definition to AbsyType and parser (parser definition may be ...Gravatar Dietrich2015-04-17
* adding references to the floating point type wherever references to the real ...Gravatar Dietrich2015-04-17
* VC gen for security propertiesGravatar akashlal2015-04-05
* Eliminated calls to deprecated method.Gravatar wuestholz2015-02-18
* Added a setter for CommandLineOptions.ProverOptions and fixed several contracts.Gravatar wuestholz2015-02-18
* Protect Bitvector field of BvExtractExpr when it is immutable.Gravatar Dan Liew2015-02-12
* Protect E0 and E1 in BvConcatExpr if Expr is immutable.Gravatar Dan Liew2015-02-12
* Fix what looked like a serious design issue when Type checkingGravatar Dan Liew2015-02-12
* When an Expr immutable, never change Type reference if it has been set,Gravatar Dan Liew2015-02-12
* Protect the Args field of NAryExpr when it is immutable.Gravatar Dan Liew2015-02-12
* Fix performance issue in ComputeHashCode() methods of Expr classes.Gravatar Dan Liew2015-02-02
* Fix typechecking immutable Expr when we haveGravatar Dan Liew2015-01-31
* Made it produce slightly different passive commands for assignments to assump...Gravatar wuestholz2015-01-30
* Protect the body of ForAllExpr, ExistsExpr and LambdaExpr when theyGravatar Dan Liew2015-01-29
* Fix ForAllExpr, ExistsExpr and LambdaExpr constructors so it is possibleGravatar Dan Liew2015-01-29
* Protect the NAryExpr.Fun field when the NAryExpr is immutable.Gravatar Dan Liew2015-01-29
* Protect the Expr field of OldExpr if it is immutable. Add unit testGravatar Dan Liew2015-01-29
* Protect the Type field of an Expr if is Immutable. Note if the ExprGravatar Dan Liew2015-01-29
* Protect the Name and Decl fields of IdentifierExpr when it isGravatar Dan Liew2015-01-29
* Prevent a BvConst being changed once constructed. The motivationGravatar Dan Liew2015-01-29
* Add the ability to declare Expr to be immutable at construction time.Gravatar Dan Liew2015-01-29
* Fixed minor issue.Gravatar wuestholz2015-01-26
* Worked on the verification result caching (statement checksums).Gravatar wuestholz2015-01-26
* Minor changeGravatar wuestholz2015-01-26
* Minor changeGravatar wuestholz2015-01-26
* Worked on the verification result caching (trace output).Gravatar wuestholz2015-01-26
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 08:57:34 +0000