[examples] a few adaptions to the examples

Author: mattulbrich

examples/heap/information_flow/README-ArrayList.txt

@@ -0,0 +1,9 @@
+example.name = ArrayList
+example.path = Information Flow/Ghost State
+example.additionalFile1 = src/ArrayList.java
+
+A collection of examples for modelling dependencies / secure information flow using ghost state.
+
+ArrayList: A variation of the ArrayList class from the "list" example, where the proof obligations for the dependency contracts have been encoded into ghost state and method contracts. These method contract proof obligations should be verifiable without direct user interaction. The regular dependency proof obligations are meaningless here.
+
+  

examples/heap/removeDups/project.key

@@ -1,3 +1,34 @@
+\settings {
+"#Proof-Settings-Config-File
+#Mon Aug 03 16:58:18 CEST 2009
+[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
+[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_EXPAND
+[StrategyProperty]DEP_OPTIONS_KEY=DEP_OFF
+[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_OFF
+[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF
+[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_INVARIANT
+[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF
+[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF
+[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS
+[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_DEF_OPS
+[DecisionProcedure]Timeout=60
+[View]ShowWholeTaclet=false
+[View]MaxTooltipLines=40
+[General]DnDDirectionSensitive=true
+[General]StupidMode=true
+[General]OneStepSimplification=true
+[Strategy]Timeout=-1
+[Strategy]MaximumNumberOfAutomaticApplications=10000
+[Choice]DefaultChoices=assertions-assertions\:on, intRules-intRules\:arithmeticSemanticsIgnoringOF,initialisation-initialisation\:disableStaticInitialisation,programRules-programRules\:Java,runtimeExceptions-runtimeExceptions\:ban,JavaCard-JavaCard\\:on , Strings-Strings\\:on , modelFields-modelFields\\:showSatisfiability , bigint-bigint\\:on , sequences-sequences\\:on , reach-reach\\:on , integerSimplificationRules-integerSimplificationRules\\:full , optimisedSelectRules-optimisedSelectRules\\:on , wdOperator-wdOperator\\:L , wdChecks-wdChecks\\:off
+[DecisionProcedure]ActiveRule=_noname_
+[General]UseJML=true
+[View]HideClosedSubtrees=false
+[View]HideIntermediateProofsteps=false
+[Strategy]ActiveStrategy=JavaCardDLStrategy
+[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED
+"
+}
+
 \javaSource ".";
 
 \chooseContract

examples/index/samplesIndex.txt

@@ -40,7 +40,8 @@ heap/fm12_01_LRS/README.txt
 heap/permutedSum/README.txt
 
 heap/vacid0_01_SparseArray/README.txt
-heap/vacid0_05_RedBlackTrees/README.txt
+# Red-Black-Trees cannot be parsed currently
+# heap/vacid0_05_RedBlackTrees/README.txt
 heap/WeideEtAl_01_AddAndMultiply/README.txt
 heap/WeideEtAl_02_BinarySearch/README.txt