debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	fixed an issue with parsing floating points	Checkmate50	2016-07-19
\|
*	Added and briefly tested the updated syntax. NaN/oo not supported yet	Checkmate50	2016-07-19
\|
*	rebuilt scanner and parser via coco	Checkmate50	2016-07-16
\|
*	Merging complete. Everything looks good crosses fingers	Checkmate50	2016-06-06
\|
*	finished testing, fixed several minor compiler bugs	Checkmate50	2016-06-06
\|
*	Initial round of testing works with new syntax. Fixed an error where ↵	Checkmate50	2016-05-31
\| \| \| \|	floating points could not be given as a function argument
*	modified floating point syntax and modified floating point constants to use ↵	Checkmate50	2016-03-17
\| \| \| \|	bitvector values
*	Modified BigFloat and parser to accept correct SMT-LIB syntax	Checkmate50	2016-02-20
\|
*	Special fp types (such as infinity and NaN are now translated by boogie	Checkmate50	2015-11-29
\|
*	Added initial support for float addition	Checkmate50	2015-09-17
\|
*	Float type now works correctly for simple variable declaration and comparison.	Dietrich	2015-07-20
\|
*	Modified internal abstract float representation to allow user-defined ↵	Dietrich	2015-07-13
\| \| \| \|	mantissa and exponent
*	added interpretation of floating point constants to the parser	Dietrich	2015-05-18
\|
*	added decimal reading functionality to the float type	Dietrich	2015-05-05
\|
*	Finished up Parser modifications	Dietrich	2015-04-27
\|
*	removed the last console writes (used for testing)	Dietrich	2015-04-26
\|
*	Successfully parsed the float type	Dietrich	2015-04-26
\|
*	added float type to the set array in Parser	Dietrich	2015-04-26
\|
*	removed comments from Scanner.cs, changed the value of the float token kind ↵	Dietrich	2015-04-26
\| \| \| \|	to 97/98 (from 135/136)
*	added float type to Arithmetic Expression and added a new float test	Dietrich	2015-04-26
\|
*	renamed fp32 to BigFloat	Dietrich	2015-04-20
\|
*	added minor commenting to Parser.cs	Dietrich	2015-04-20
\|
*	added a collection of console writes for debugging. These should be removed ↵	Dietrich	2015-04-20
\| \| \| \|	in a future commit
*	Added float type to the Parser and Scanner	Dietrich	2015-04-20
\|
*	added float tipe to AbsyExpr and IntervalDomain. The methods added may ↵	Dietrich	2015-04-20
\| \| \| \|	require later modification
*	added float type definition to AbsyType and parser (parser definition may be ↵	Dietrich	2015-04-17
\| \| \| \|	unfinished)
*	adding references to the floating point type wherever references to the real ↵	Dietrich	2015-04-17
\| \| \| \|	type exist. This remains a work in progress
*	Add the ability to declare Expr to be immutable at construction time.	Dan Liew	2015-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.
*	Did more refactoring.	wuestholz	2014-09-23
\|
*	Added /useBaseNameForFile command line argument. The Scanner	Dan Liew	2014-04-06
\| \| \| \| \| \| \| \| \| \| \| \| \|	and Parser constructors have been modified to take an optional argument specifying this and the ExecutionEngine passes for that value CommandLineOptions.Clo.UseBaseNameForFileName This option when true causes the basename of file to be used inside created Tokens instead of what the user passed on the command line which might be a relative or absolute path. The motivation for adding this option is that it is needed for the lit driven tests so that the output of Boogie can be reliably checked.
*	bug fixes in Duplicate.cs and parsing of invariant attributes	qadeer	2013-12-22
\| \| \| \|	other bug fixes in QED stuff
*	regenerated after updating Parser.frame	qadeer	2013-12-16
\|
*	added syntax for par call and ParCallCmd	qadeer	2013-12-16
\|
*	Removed the remaining pure collections.	wuestholz	2013-07-23
\|
*	Fixed the Coco/R grammar and regenerated the parser.	wuestholz	2013-07-22
\|
*	All ...Seq classes now gone	Ally Donaldson	2013-07-22
\|
*	ExprSeq: farewell	Ally Donaldson	2013-07-22
\|
*	StringSeq: farewell	Ally Donaldson	2013-07-22
\|
*	CmdSeq: farewell	Ally Donaldson	2013-07-22
\|
*	Started to remove ...Seq classes	Ally Donaldson	2013-07-22
\|
*	More refactoring	Ally Donaldson	2013-07-22
\|
*	More refactoring	Ally Donaldson	2013-07-22
\|
*	More refactoring: PureCollections.Sequence not used anymore.	Ally Donaldson	2013-07-22
\|
*	More refactoring towards replacing PureCollections.Sequence with List	Ally Donaldson	2013-07-22
\|
*	Refactoring of TypeVariableSeq	Ally Donaldson	2013-07-22
\|
*	Refactoring of VariableSeq and TypeSeq	Ally Donaldson	2013-07-22
\|
*	Requires/EnsuresSeq replaced by List<Requires/Ensures>	Ally Donaldson	2013-07-22
\|
*	added parallel calls	Unknown	2013-03-01
\|
*	removed call forall and * args to calls	Unknown	2013-02-23
\|
*	Refactored code that generates an axiom for a function, and changed the ↵	Rustan Leino	2013-01-17
\| \| \| \|	pretty printing to always reflect when a function body is inlined