From 3ad6b396681e0cb936eba09c4d7b6ebed882a0a2 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 29fa74c5a9..4e523fe1ee 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2168,7 +2168,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