- Jan 29, 2014
-
-
Régis Blanc authored
-
- Jan 27, 2014
-
-
Régis Blanc authored
-
Régis Blanc authored
Previously, array access were generated via a code transformation in ArrayTransformation in xlang, where Array Select and Update were wrapped in if-then-else with an Error in the else branch. They are now natively supported in VC generation. Some testcases --- that would trigger bugs when --xlang is not used with functional array ---- are included in this commit The commit introduces a new abstraction to traverse Leon trees and collect path conditions. This traverser is used for the implementation of the VC generation for arrays.
-
Régis Blanc authored
-
- Jan 10, 2014
-
-
Etienne Kneuss authored
-
Etienne Kneuss authored
-
Etienne Kneuss authored
-
Etienne Kneuss authored
- remove superfluous implementations doing almost the same - introduce pre/post traversal and transformers as foreach/map/fold - Redefine other operations exists, contains, as folds - Fix freshenLocals bug found by Ravi
-
- Dec 16, 2013
-
-
Etienne Kneuss authored
- Simplify code generation by replacing CompilationEnvironment with a simple scope state. - Support Choose construct in both evaluators. - Introduce RecursiveEvaluator (renamed from Naive) and TracingEvaluator which tracks intermediate values as well. - Introduce offset as well as ranged positions, extract all positions from trees. Try to propagate them as much as possible. Introduced .copiedFrom - Remove dead-code, and improve TreeOps a bit. - Introduce Pretty-printer arguments
-
- Dec 03, 2013
-
-
Etienne Kneuss authored
-
Etienne Kneuss authored
-
- Dec 02, 2013
-
-
Etienne Kneuss authored
-
Etienne Kneuss authored
-
Etienne Kneuss authored
-
Etienne Kneuss authored
-
- Nov 29, 2013
-
-
Etienne Kneuss authored
-
Etienne Kneuss authored
-
- Nov 20, 2013
-
-
Etienne Kneuss authored
-
Etienne Kneuss authored
-
Ivan Kuraj authored
-
Ivan Kuraj authored
-
Etienne Kneuss authored
-
- Nov 15, 2013
-
-
Etienne Kneuss authored
-
Etienne Kneuss authored
-
- Nov 13, 2013
-
-
Etienne Kneuss authored
-
Etienne Kneuss authored
-
Etienne Kneuss authored
-
- Nov 12, 2013
-
-
Etienne Kneuss authored
-
Etienne Kneuss authored
-
Nicolas Voirol authored
-
Nicolas Voirol authored
small issues in the ChainProcessor system. Some tests ending in .BAK should be runnable but can't for now because of a memory leak somewhere in the framework.
-
Nicolas Voirol authored
-
Nicolas Voirol authored
-
- Nov 08, 2013
-
-
Etienne Kneuss authored
-
- Nov 07, 2013
-
-
Etienne Kneuss authored
-
- Oct 25, 2013
-
-
Etienne Kneuss authored
-
- Oct 23, 2013
-
-
Etienne Kneuss authored
-
- Oct 18, 2013
-
-
Etienne Kneuss authored
-
- Oct 16, 2013
-
-
Etienne Kneuss authored
-
- Oct 10, 2013
-
-
Etienne Kneuss authored
-