From 5ff67448cf87313ba9009fa2a05e5e8a919e1bb8 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu, 4 Feb 2021 09:03:28 +0100
Subject: [PATCH] [tests] synchronize with frama-c/frama-c!3055
---
tests/stl/oracle/stl_system_error.res.oracle | 8 ++++++++
1 file changed, 8 insertions(+)
diff --git a/tests/stl/oracle/stl_system_error.res.oracle b/tests/stl/oracle/stl_system_error.res.oracle
index afad1e61..0560f74f 100644
--- a/tests/stl/oracle/stl_system_error.res.oracle
+++ b/tests/stl/oracle/stl_system_error.res.oracle
@@ -2196,6 +2196,14 @@ int *fgetws(int * __restrict ws, int n, FILE * __restrict stream);
}
*/
+/*@ requires valid_wstring_ws1: valid_read_wstring(ws1);
+ requires valid_wstring_ws2: valid_read_wstring(ws2);
+ assigns \result;
+ assigns \result
+ \from (indirect: *(ws1 + (0 ..))), (indirect: *(ws2 + (0 ..)));
+ */
+int wcscasecmp(int const *ws1, int const *ws2);
+
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
--
GitLab