summaryrefslogtreecommitdiff
path: root/Source/Core
Commit message (Collapse)AuthorAge
...
* | added general floating point mantissa and exponent managementGravatar Dietrich2015-05-04
| |
| * Add support for 'verified_under' attributes on procedure calls and invariants.Gravatar Valentin Wüstholz2015-04-29
| |
* | 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
* 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
| | | | | | | anything that implements the IAppliable interface. Type checking should never need to change the reference of a list of arguments (hence the removal of the ``ref`` keyword) and we need to use IList<Expr> instead of List<Expr> to allow NAryExpr to do its type checking.
* When an Expr immutable, never change Type reference if it has been set,Gravatar Dan Liew2015-02-12
| | | | even if the types are equivalent.
* Protect the Args field of NAryExpr when it is immutable.Gravatar Dan Liew2015-02-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * Made changing the reference throw an exception if the NAryExpr was constructed as immutable * Changed the type of NAryExpr.Args to be IList<Expr> rather than List<Expr> so that when the NAryExpr is immutable I can return ``_Args.AsReadOnly()`` (instead of ``_Args``) which returns a read only wrapper around the List<Expr> so that clients cannot change the list. I came across two problems * Making this change required changing types all over the place (from List<Expr> to IList<Expr>). I feel that changes are extensive enough that there's a good chance that out of tree clients using Boogie's libraries might break. I've waited for a code review but this didn't happen so I'm committing anyway. * I came across something that looks like bad design of the IAppliable interface which potentially breaks immutability enforcement. I've left this as a "FIXME" in this. Here's the problematic method. ``` Type Typecheck(ref List<Expr>/*!*/ args, out TypeParamInstantiation/*!*/ tpInstantiation, TypecheckingContext/*!*/ tc); ``` It potentially allows the instance of the args to be changed which seems very suspect.
* Fix performance issue in ComputeHashCode() methods of Expr classes.Gravatar Dan Liew2015-02-02
| | | | | | If constructing immutable Expr bottom up this would be very inefficient because the hashcode would be recomputed unnecessarily. Now just make ComputeHashCode() methods call GetHashCode() on Expr instead.
* Fix typechecking immutable Expr when we haveGravatar Dan Liew2015-01-31
| | | | | | | | | | | | <bool> == <bool> or <bool> != <bool> The type checker tries rewrite the Expr when it gets type checked which breaks immutability so disable doing this if the Expr is immutable.
* Made it produce slightly different passive commands for assignments to ↵Gravatar wuestholz2015-01-30
| | | | assumption variables.
* Protect the body of ForAllExpr, ExistsExpr and LambdaExpr when theyGravatar Dan Liew2015-01-29
| | | | are immutable. Add unit tests to check this.
* Fix ForAllExpr, ExistsExpr and LambdaExpr constructors so it is possibleGravatar Dan Liew2015-01-29
| | | | to set them as immutable (not currently enforced for these Expr types).
* Protect the NAryExpr.Fun field when the NAryExpr is immutable.Gravatar Dan Liew2015-01-29
| | | | | Add a unit test for this. We need to protect the Args field too but that is going to be much harder to enforce.
* Protect the Expr field of OldExpr if it is immutable. Add unit testGravatar Dan Liew2015-01-29
| | | | to check this is being enforced.
* Protect the Type field of an Expr if is Immutable. Note if the ExprGravatar Dan Liew2015-01-29
| | | | | | has never been type checked we allow the Type field to be set but once it has been set it cannot be changed to refer to a different Type.
* Protect the Name and Decl fields of IdentifierExpr when it isGravatar Dan Liew2015-01-29
| | | | | immutable by raising an exception if an attempt is made to modify it after construction.
* Prevent a BvConst being changed once constructed. The motivationGravatar Dan Liew2015-01-29
| | | | | | | for doing this is that we would like a LiteralExpr to be immutable when constructed but because the "Val" field can point to a BvConst which is an object it means that although the Val reference cannot change the BvConst could be changed.
* Add the ability to declare Expr to be immutable at construction time.Gravatar Dan Liew2015-01-29
| | | | | | | | | | | | This is currently not enforced (it really should be). So right now it only amounts to a promise by the client that the Expr will not be modified after it is constructed. We should actually enforce this by protecting various fields of the Expr classes so they can't be changed if an Expr is constructed as Immutable. The motivation for doing this is it allows the value of GetHashCode() to be cached. Expr classes now implement ComputeHashCode() to do the actuall hash code computation.
* 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
|
* 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.
* Fixes to StagedHoudiniGravatar Ally Donaldson2015-01-22
|
* MergeGravatar Ally Donaldson2015-01-13
|\
| * Merging changes from wuestholz/BoogieInvariantFixesIIIIGravatar wuestholz2015-01-13
| |\
| * \ Merging changes from 0biha/BoogieInvariantFixesIIIaGravatar wuestholz2015-01-13
| |\ \
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-14 05:22:15 +0000