[test] added test

- style fixed
MchKosticyn · Dec 4, 2023 · c20533d · c20533d
1 parent bebc3bd
commit c20533d
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 2 deletions.
diff --git 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
@@ -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
@@ -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() =