summaryrefslogtreecommitdiff
path: root/Source/VCExpr
Commit message (Collapse)AuthorAge
* Changed the syntax reading of the float typeGravatar Checkmate502016-07-16
|
* Merging complete. Everything looks good *crosses fingers*Gravatar Checkmate502016-06-06
|
* modified floating point syntax and modified floating point constants to use ↵Gravatar Checkmate502016-03-17
| | | | bitvector values
* 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
|
* 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
|
* 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 a setter for CommandLineOptions.ProverOptions and fixed several contracts.Gravatar wuestholz2015-02-18
|
* Minor change to the encoding of partially verified assertions as VCGravatar wuestholz2015-01-30
|
* Change the return type of StandardVisitor.VisitLiteralExpr() fromGravatar Dan Liew2015-01-25
| | | | | | | | | | | | | LiteralExpr to Expr. Enforcing the return type be LiteralExpr is too restrictive. There is precedence for this. For example VisitNAryExpr() returns an Expr not an NAryExpr. Unfortunately this a breaking API change so anyone who subclasses the StandardVisitor (or one of its sub classes) and overrides this method will get compilation errors until they change the return type. a visitor that does constant folding of an Expr tree
* Change the return type of StandardVisitor.VisitExistsExpr() fromGravatar Dan Liew2015-01-25
| | | | | | | | | | | | | | ExistsExpr to Expr. Enforcing the return type be ExistsExpr is too restrictive. For example it prevents anyone from implementing a visitor that does constant folding of an Expr tree. There is precedence for this. For example VisitNAryExpr() returns an Expr not an NAryExpr. Unfortunately this a breaking API change so anyone who subclasses the StandardVisitor (or one of its sub classes) and overrides this method will get compilation errors until they change the return type. a visitor that does constant folding of an Expr tree
* Change the return type of StandardVisitor.VisitForAllExpr() fromGravatar Dan Liew2015-01-25
| | | | | | | | | | | | | | ForAllExpr to Expr. Enforcing the return type be ForAllExpr is too restrictive. For example it prevents anyone from implementing a visitor that does constant folding of an Expr tree. There is precedence for this. For example VisitNAryExpr() returns an Expr not an NAryExpr. Unfortunately this a breaking API change so anyone who subclasses the StandardVisitor (or one of its sub classes) and overrides this method will get compilation errors until they change the return type. a visitor that does constant folding of an Expr tree
* Change the return type of StandardVisitor.VisitBvExtractExpr() fromGravatar Dan Liew2015-01-25
| | | | | | | | | | | | | | BvExtractExpr to Expr. Enforcing the return type be BvExtractExpr is too restrictive. For example it prevents anyone from implementing a visitor that does constant folding of an Expr tree. There is precedence for this. For example VisitNAryExpr() returns an Expr not an NAryExpr. Unfortunately this a breaking API change so anyone who subclasses the StandardVisitor (or one of its sub classes) and overrides this method will get compilation errors until they change the return type. a visitor that does constant folding of an Expr tree
* Change the return type of StandardVisitor.VisitBvConcatExpr() fromGravatar Dan Liew2015-01-25
| | | | | | | | | | | | | BvConcatExpr to Expr. Enforcing the return type be BvConcatExpr is too restrictive. For example it prevents anyone from implementing a visitor that does constant folding of an Expr tree. There is precedence for this. For example VisitNAryExpr() returns an Expr not an NAryExpr. Unfortunately this a breaking API change so anyone who subclasses the StandardVisitor (or one of its sub classes) and overrides this method will get compilation errors until they change the return type.
* Made invariant of class 'Trigger' robust byGravatar 0biha2015-01-01
| | | | | | -replacing public field by private field + getter -using read-only wrappers (to avoid leaking) -cloning the tr list in the setter and constructor (to avoid capturing)
* more work on reducing call stack consumptionGravatar qadeer2014-12-18
|
* patched two occurrences of StackOverflowException on benchmarks from IronCladGravatar qadeer2014-12-16
|
* Fix nasty bug introduced by commit 61a94f409975.Gravatar Dan Liew2014-07-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | There were many calls in the code to ``` new TokenTextWriter("<buffer>", buffer, false) ``` Prior to 61a94f409975 this was a call to the following constructor ``` TokenTextWriter(string filename, TextWriter writer, bool setTokens) ``` After that commit these then became calls to ``` TokenTextWriter(string filename, TextWriter writer, bool pretty) ``` An example of where this would cause issues was if ToString() was called on an AbsyCmd then the its token would be modified because the setTokens parameter was effectively set to True when the original intention was for it to be set to false! To fix this I've * Removed the default parameter value for pretty and fixed all uses so that we pass false where it was implicitly being set before * Where the intention was to set setTokens to false this has been fixed so it is actually set to false! Unfortunately I couldn't find a way of observing this bug from the Boogie executable so I couldn't create a test case. I could only observe it when I was using Boogie's APIs.
* (Fixed and) strengthened contracts of ReadOnlyVisitor. The postconditions ↵Gravatar Rustan Leino2014-02-24
| | | | | | of its methods now demand the return value to equal the given node. Changed read-only visitors to extend from ReadOnlyVisitor instead of just StandardVisitor.
* Fix Boogie so it compiled with mono. Patch by Dan Liew.Gravatar Ally Donaldson2014-01-14
|
* added syntax for par call and ParCallCmdGravatar qadeer2013-12-16
|
* added the QED build configurationGravatar qadeer2013-12-02
|
* fixed bugGravatar qadeer2013-09-09
|
* fixed the problem with codexprsGravatar qadeer2013-09-07
| | | | now positive/negative context is detected and appropriate translation is done
* When a codeexpr is used at the top-level in an assume statement, we use the ↵Gravatar qadeer2013-09-04
| | | | alternative existential semantics.
* Avoid another potential data race.Gravatar wuestholz2013-07-23
|
* Resolved some issues with data races.Gravatar wuestholz2013-07-23
|
* Did some refactoring.Gravatar wuestholz2013-07-23
|
* Minor fixGravatar wuestholz2013-07-23
|
* Did some refactoring.Gravatar wuestholz2013-07-23
|
* Use 'All' and 'Any' instead of 'Contract.ForAll' and 'Contract.Exists' in ↵Gravatar wuestholz2013-07-22
| | | | code (as opposed to contracts).
* All ...Seq classes now goneGravatar Ally Donaldson2013-07-22
|
* ExprSeq: farewellGravatar Ally Donaldson2013-07-22
|
* RESeq: farewellGravatar Ally Donaldson2013-07-22
|
* BlockSeq: farewellGravatar Ally Donaldson2013-07-22
|
* CmdSeq: farewellGravatar Ally Donaldson2013-07-22
|
* Started to remove ...Seq classesGravatar Ally Donaldson2013-07-22
|
* More refactoringGravatar Ally Donaldson2013-07-22
|
* More refactoringGravatar Ally Donaldson2013-07-22
|
* More refactoring towards replacing PureCollections.Sequence with ListGravatar Ally Donaldson2013-07-22
|
* MergeGravatar Ally Donaldson2013-07-22
|\
* | Refactoring of TypeVariableSeqGravatar Ally Donaldson2013-07-22
| |
* | Changed Has method of PureSequence to Contains to make refactoring easier.Gravatar Ally Donaldson2013-07-22
| |
| * mergeGravatar Pantazis Deligiannis2013-07-22
| |\ | |/ |/|
* | Refactoring of VariableSeq and TypeSeqGravatar Ally Donaldson2013-07-22
| |
* | Requires/EnsuresSeq replaced by List<Requires/Ensures>Gravatar Ally Donaldson2013-07-22
| |
| * MergeGravatar Pantazis Deligiannis2013-07-15
|/|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 23:44:40 +0000