summaryrefslogtreecommitdiff
path: root/Source/Core/AbsyExpr.cs
Commit message (Expand)AuthorAge
* modified floating point syntax and modified floating point constants to use b...Gravatar Checkmate502016-03-17
* 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
* Modified internal abstract float representation to allow user-defined mantiss...Gravatar Dietrich2015-07-13
* 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
* added float type to Arithmetic Expression and added a new float testGravatar Dietrich2015-04-26
* renamed fp32 to BigFloatGravatar Dietrich2015-04-20
* added a collection of console writes for debugging. These should be removed ...Gravatar Dietrich2015-04-20
* added float tipe to AbsyExpr and IntervalDomain. The methods added may requi...Gravatar Dietrich2015-04-20
* adding references to the floating point type wherever references to the real ...Gravatar Dietrich2015-04-17
* 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 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
* Worked on the verification result caching (statement checksums).Gravatar wuestholz2015-01-26
* Made invariant of class 'IfThenElse' robust by changing the designGravatar 0biha2015-01-01
* Worked on more native support for partially-verified assertions.Gravatar wuestholz2014-12-28
* Fixed issue with resolution of function calls.Gravatar wuestholz2014-11-26
* Fix FunctionCall.Resolve() so that when the function is resolved the type bec...Gravatar Dan Liew2014-11-25
* Fix bug in FunctionCall that caused the ExprTypeChecking.FunctionCall()Gravatar Dan Liew2014-11-25
* fixed various CodeContracts issues.Gravatar qadeer2014-09-18
* Added missing Expr.Neg() static method.Gravatar Dan Liew2014-08-15
* Minor refactoringGravatar wuestholz2014-08-03
* MergeGravatar Dan Rosén2014-08-01
|\
* | Add alpha equivalence check for Expr, and use it when lambda liftingGravatar Dan Rosén2014-08-01
| * Fix bug in NAryExpr where is was possible for A.Equals(B) to returnGravatar Dan Liew2014-07-29
| * Fix bug in NAryExpr where Equals() override was not correctly implemented.Gravatar Dan Liew2014-07-28
|/
* Fix nasty bug introduced by commit 61a94f409975.Gravatar Dan Liew2014-07-15
* Refactored how checksums are computed.Gravatar wuestholz2014-07-13
* Did some refactoring, fixed minor issues, and made it apply the more advanced...Gravatar wuestholz2014-07-06
* Add some pretty-printing, on by default. Turn off with the flag "/pretty:0"Gravatar Dan Rosén2014-06-24
* Add isBvConst and asBvConst accessors to LiteralExpr to match theGravatar Dan Liew2014-05-28
* Recursive walking of Exprs doesn't play nice when the depth of the AST is high.Gravatar akashlal2014-01-07
* Resolved some issues with data races.Gravatar wuestholz2013-07-23
* All ...Seq classes now goneGravatar Ally Donaldson2013-07-22
* ExprSeq: farewellGravatar Ally Donaldson2013-07-22
* Started to remove ...Seq classesGravatar Ally Donaldson2013-07-22
* More refactoringGravatar Ally Donaldson2013-07-22