From d9eea8a2167a59cde0fc8b6f7a3ba2a3e970772f Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 4 Aug 2024 14:02:53 +0200 Subject: [PATCH] Typo --- src/analyses/base.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 9d4e3be0d4..7afe8861b0 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2149,7 +2149,7 @@ struct end | _, _ when get_bool "sem.unknown_function.spawn" -> (* TODO: Remove sem.unknown_function.spawn check because it is (and should be) really done in LibraryFunctions. - But here we consider all non-ThreadCrate functions also unknown, so old-style LibraryFunctions access + But here we consider all non-ThreadCreate functions also unknown, so old-style LibraryFunctions access definitions using `Write would still spawn because they are not truly unknown functions (missing from LibraryFunctions). Need this to not have memmove spawn in SV-COMP. *) let shallow_args = LibraryDesc.Accesses.find desc.accs { kind = Spawn; deep = false } args in