From c20533db35938c4c1eead446bb99e84901bf05ed Mon Sep 17 00:00:00 2001
From: Mikhail Kosticyn <mishakosticyn@yandex.ru>
Date: Mon, 4 Dec 2023 15:17:15 +0300
Subject: [PATCH] [test] added test

- style fixed
---
 VSharp.SILI.Core/Memory.fs  |  2 ++
 VSharp.Test/Tests/Lists.cs  | 11 ++++++++++-
 VSharp.Utils/MemoryGraph.fs |  1 -
 3 files changed, 12 insertions(+), 2 deletions(-)

diff --git a/VSharp.SILI.Core/Memory.fs b/VSharp.SILI.Core/Memory.fs
index 499a24d34..ccc7eff3f 100644
--- a/VSharp.SILI.Core/Memory.fs
+++ b/VSharp.SILI.Core/Memory.fs
@@ -811,6 +811,7 @@ module internal Memory =
         | ConcreteHeapAddress concreteAddress, None when cm.Contains concreteAddress ->
             let data = cm.GetAllArrayData concreteAddress
             readSymbolicIndexFromConcreteArray state concreteAddress data indices arrayType
+        // TODO: remember all concrete data from 'ConcreteMemory' and add it to symbolic constant [Test: ConcreteDictionaryTest1]
         | _ -> readArrayIndexSymbolic state address indices arrayType
 
 // ------------------------------- Array writing -------------------------------
@@ -904,6 +905,7 @@ module internal Memory =
         match address.term with
         | ConcreteHeapAddress address when cm.Contains address ->
             cm.ReadClassField address field |> objToTerm state field.typ
+        // TODO: remember all concrete field values from 'ConcreteMemory' and add it to symbolic constant [Test: ConcreteDictionaryTest1]
         | _ -> readClassFieldSymbolic state address field
 
     let readStaticField state typ (field : fieldId) =
diff --git a/VSharp.Test/Tests/Lists.cs b/VSharp.Test/Tests/Lists.cs
index 3d5d80bdc..8191470d7 100644
--- a/VSharp.Test/Tests/Lists.cs
+++ b/VSharp.Test/Tests/Lists.cs
@@ -833,7 +833,7 @@ public static int ConcreteDictionaryTest(int v)
             return 0;
         }
 
-        [Ignore("needs fix")]
+        [Ignore("fix composition with concrete memory")]
         public static int ConcreteDictionaryTest1(int a, int b)
         {
             var d = new Dictionary<int, List<int>>();
@@ -848,6 +848,15 @@ public static int ConcreteDictionaryTest1(int a, int b)
             return 2;
         }
 
+        [TestSvm(100)]
+        public static int ListContains(int a, int b)
+        {
+            var l = new List<int> {2, 3, b, 5};
+            if (l.Contains(a))
+                return 1;
+            return 0;
+        }
+
         [Ignore("Support rendering recursive arrays")]
         public static object[] ConcreteRecursiveArray()
         {
diff --git a/VSharp.Utils/MemoryGraph.fs b/VSharp.Utils/MemoryGraph.fs
index f73f350f6..a1d8a0e51 100644
--- a/VSharp.Utils/MemoryGraph.fs
+++ b/VSharp.Utils/MemoryGraph.fs
@@ -189,7 +189,6 @@ with
                 t.MethodMocks |> Seq.map (fun m -> m.ReturnValues |> Array.map encode) |> Array.ofSeq
             outImplementations =
                 t.MethodMocks |> Seq.map (fun m -> m.OutValues |> Array.map (Array.map encode)) |> Seq.toArray
-                
         }
 
     member x.Decode() =