debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
...
*	Translate AddressOf expressions correctly.	Mike Barnett	2011-11-16
\| \| \| \|	Fixes for problems when translating generic type parameters.
*	Load all assemblies before doing anything else so that the unification for	Mike Barnett	2011-11-16
\| \| \| \| \| \| \| \| \| \|	the Core Assembly identity can happen correctly. Cache things in the sink based on the mangled name rather than the interned key: this prevents clashes in the Boogie program, but might mask some errors due to different types/members with the same full name (minus the assembly name of course). Translate generic parameters as Ref instead of Box if they are constrained to be a reference or struct (since we translate structs as Ref). [Experimental]
*	For some reason, these didn't get into the last commit.	Mike Barnett	2011-11-14
\|
*	Trying to get the generics translation correct...	Mike Barnett	2011-11-14
\|
*	moved the addition of selectors and testers to program.Resolve	qadeer	2011-11-11
\|
*	Many, many bug fixes related to generics and some other random problems.	Mike Barnett	2011-11-10
\|
*	change in model parsing with datatype values	qadeer	2011-11-07
\|
*	Don't wipe out existing attributes when adding {:extern}	Mike Barnett	2011-11-01
\|
*	Major changes to the translator traversers because they now are based on the	Mike Barnett	2011-10-31
\| \| \| \| \| \| \| \|	new traversers. (The old ones have been marked as obsolete.) All types are now encoded as "datatypes" in Boogie. So non-generic types are nullary functions and generic types just have at least one type argument. Lots of other fixes: string encoding of names is now done by negating Boogie's regular expression for identifiers, etc.
*	Fixed the generation of names for datatype functions to use the API for	Mike Barnett	2011-10-31
\| \| \| \| \| \|	getting SMT-approved names. Fixed a bug in VisitDistinctOp where a bad axiom was being generated when no grouping had more than one occurrence.
*	Don't let /s be specified for stub files. (But keep the old code in case we	Mike Barnett	2011-10-23
\| \| \| \|	go back to it.)
*	Fixed two bugs related to structs: now a struct that is declared without an	Mike Barnett	2011-09-01
\| \| \| \| \| \| \| \| \| \|	initial value is getting allocated. Also, deferring ctor calls within a struct ctor do not result in an attempt to allocate a new struct and assign it to "this". Restart the temporary variable counter on entry to each method. (This makes the regressions less noisy because a change in the number of temporaries created for one method will not change the names of the temporaries in other methods.)
*	more string mangling	qadeer	2011-08-31
\|
*	delegates/events implemented as multisets rather than linked lists	qadeer	2011-08-30
\|
*	Merge	qadeer	2011-08-26
\|\
* \|	a small bug in GeneralHeap translation	qadeer	2011-08-26
\| \|
\| *	(phone)data on results of analyses on market apps	t-espave	2011-08-26
\| \|
* \|	Merge	qadeer	2011-08-26
\|\\|
* \|	some more string munging	qadeer	2011-08-26
\| \|
\| *	(bct) removed ad-hoc string replacements, the problem is actually the encoding	t-espave	2011-08-25
\| \|
* \|	fixed a bug: do not include the invoke procedure for thread delegates in the ↵	qadeer	2011-08-25
\| \| \| \| \| \| \| \|	set of initially declared procedures. The principle is that any procedure whose body will be created dynamically, its header should also be created dynamically
* \|	fixed bug	qadeer	2011-08-23
\|/
*	(phone bct) boolean binding of control enabledness ignored (for now)	t-espave	2011-08-22
\| \| \| \|	tracking Page virtual overrides
*	(phone bct) minor bugfixes found playing around with apps	t-espave	2011-08-19
\|
*	continuned phone bct docs	t-espave	2011-08-19
\|
*	fix in event translation for whole program analysis	qadeer	2011-08-17
\|
*	Merge	qadeer	2011-08-17
\|\
* \|	added RealModulus	qadeer	2011-08-17
\| \|
\| *	(phone) documentation	t-espave	2011-08-17
\|/
*	(bct) skeleton of plugin infrastructure. for now the code is essentially the ↵	t-espave	2011-08-16
\| \| \| \| \| \|	same I will open a plugin branch to make more deeper changes until everything is stable
*	(phone) fixed problem with unknown type anonymous controls	t-espave	2011-08-16
\|
*	Merge	t-espave	2011-08-16
\|\
* \|	saving navigation bad smells report	t-espave	2011-08-16
\| \|
\| *	Made the split fields heap agree with the naming convention used for fields that	Mike Barnett	2011-08-16
\| \| \| \| \| \| \| \| \| \|	the general heap uses. Updated regressions.
* \|	(BCT) starting translators-as-plugins impl	t-espave	2011-08-15
\|/
*	Better message when an error happens.	Mike Barnett	2011-08-15
\| \| \| \| \|	AssertionInjector: Check for invalid source locations (FeeFee) so they don't confuse the injection.
*	cleaning up & refactor	t-espave	2011-08-15
\|
*	workaround corral bug (cannot handle parallel assignments)	qadeer	2011-08-12
\|
*	various fixes to deal with bug in generic delegates	qadeer	2011-08-12
\|
*	Merge	qadeer	2011-08-11
\|\
* \|	fixes for bug with generic delegates	qadeer	2011-08-11
\| \|
\| *	Merge	t-espave	2011-08-11
\| \|\
\| * \|	(phone) cancel/navigation on back key is now deep through calls. More info ↵	t-espave	2011-08-11
\| \| \| \| \| \| \| \| \| \| \| \|	reported at end of analysis
\| \| *	Fixed problem where events in stubs were generating duplicate declarations.	Mike Barnett	2011-08-11
\| \| \|
\| \| *	Added references to the AssertionInjector project so it can build again.	Mike Barnett	2011-08-11
\| \|/
\| *	(BCT) BREAKING CHANGE	t-espave	2011-08-11
\| \| \| \| \| \| \| \|	BCT now links to CCI in CodeBox, get the CodeBox tree into C:\CCICodeBox
\| *	(phone) fixed issues with anonymous xaml declarations.	t-espave	2011-08-10
\|/
*	(phone) back key handling via delegate detected	t-espave	2011-08-10
\| \| \| \|	back key handling code not reflected in nav graph - usually the programmer's intent
*	(phone) slicing to avoid self loops	t-espave	2011-08-09
\|
*	phone nav building stats	t-espave	2011-08-09
\|