From 8f2038542bcb8ec93b6c6447f38d098cff98fc2c Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 5 Jan 2022 19:21:13 +0100 Subject: Split eval_local_function_call_symbolic to isolate a function which can be reused for non-local function calls --- src/Utils.ml | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 src/Utils.ml (limited to 'src/Utils.ml') diff --git a/src/Utils.ml b/src/Utils.ml new file mode 100644 index 00000000..a285e869 --- /dev/null +++ b/src/Utils.ml @@ -0,0 +1,6 @@ +exception Found +(** Utility exception + + When looking for something while exploring a term, it can be easier to + just throw an exception to signal we found what we were looking for. + *) -- cgit v1.2.3 From f2fb0dc39cfa9aef2b16963d3f8a270ec45bae5e Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 6 Jan 2022 14:43:35 +0100 Subject: Make good progress on implementing utilities to test symbolic execution --- src/Utils.ml | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) (limited to 'src/Utils.ml') diff --git a/src/Utils.ml b/src/Utils.ml index a285e869..16ee7252 100644 --- a/src/Utils.ml +++ b/src/Utils.ml @@ -1,3 +1,20 @@ +(* Split a list at a given index [i] (the first list contains all the elements + up to element of index [i], not included, the second one contains the remaining + elements. Note that the first returned list has length [i]. +*) +let rec list_split_at (ls : 'a list) (i : int) = + if i < 0 then raise (Invalid_argument "list_split_at take positive integers") + else if i = 0 then ([], ls) + else + match ls with + | [] -> + raise + (Failure + "The int given to list_split_at should be <= the list's length") + | x :: ls' -> + let ls1, ls2 = list_split_at ls' (i - 1) in + (x :: ls1, ls2) + exception Found (** Utility exception -- cgit v1.2.3