summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Fix for AbsHoudiniGravatar akashlal2015-05-01
|
* AbsHoudini: made disjunct bound a parameterGravatar akashlal2015-05-01
|
* Add support for 'verified_under' attributes on procedure calls and invariants.Gravatar Valentin Wüstholz2015-04-29
|
* Try to add build status icon for the Windows build.Gravatar Dan Liew2015-04-28
|
* Try to fix the emission of invalid SMT-LIBv2 queries when Boogie has aGravatar Dan Liew2015-04-26
| | | | | variable that begins with a ``.``. This was't an issue for Z3 which ignores this but CVC4 is stricter and will emit an error
* Minor fixes for AbsHoudiniGravatar Akash Lal2015-04-23
|
* renamed og to civlGravatar qadeer2015-04-22
|
* Better error messageGravatar akashlal2015-04-21
|
* added more examplesGravatar qadeer2015-04-18
|
* patched ghost checkingGravatar qadeer2015-04-18
|
* changed aux attribute to ghostGravatar qadeer2015-04-18
|
* fixed the treatment of externGravatar qadeer2015-04-17
|
* first check inGravatar qadeer2015-04-16
|
* patched the type checker to deal with modularityGravatar qadeer2015-04-16
|
* Note that CVC4 support is experimental.Gravatar Dan Liew2015-04-05
|
* Fix typo in README.md spotted by Jeroen Ketema.Gravatar Dan Liew2015-04-05
|
* 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.
* Disable test is ``Test/Secure``. They aren't set up properly.Gravatar Dan Liew2015-04-05
|
* Some test cases for SecureVCGen (disabled for lit currently)Gravatar akashlal2015-04-05
|
* VC gen for security propertiesGravatar akashlal2015-04-05
|
* Fix ``Test/test15/CaptureState.bpl`` test under Linux.Gravatar Dan Liew2015-04-03
|
* Fix ``livevars/daytona_bug2_ioctl_example_2.bpl`` test under Linux.Gravatar Dan Liew2015-04-03
|
* Add TravisCI build status icon to README.mdGravatar Dan Liew2015-04-03
|
* Clean up .gitignore fileGravatar Dan Liew2015-04-03
|
* Remove some old mercurial files.Gravatar Dan Liew2015-04-03
|
* Add .travis.yml file for TravisCI builds.Gravatar Dan Liew2015-04-03
|
* Add initial README.mdGravatar Dan Liew2015-04-03
|
* Add LICENSE file.Gravatar Dan Liew2015-04-01
|
* updated the example to include atomic specifications (sent by Suha)Gravatar qadeer2015-03-29
|
* 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.
* fix from Serdar and SuhaGravatar qadeer2015-02-24
|
* 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
|/
* 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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-29 00:05:36 +0000