From 070460612e1f941a8e231d403ec407d5442c9f87 Mon Sep 17 00:00:00 2001 From: Pierre Nigron <pierre.nigron@cea.fr> Date: Mon, 17 Jul 2023 10:29:59 +0200 Subject: [PATCH] [tests] Update Oracles --- tests/cil/oracle/cpu_a.res.oracle | 2 ++ tests/cil/oracle/cpu_b.res.oracle | 2 ++ tests/misc/oracle/bts0990_link.res.oracle | 3 ++- tests/syntax/oracle/incompatible_qualifiers.1.res.oracle | 2 +- tests/syntax/oracle/inconsistent_decl.0.res.oracle | 3 ++- tests/syntax/oracle/inconsistent_decl.1.res.oracle | 3 ++- 6 files changed, 11 insertions(+), 4 deletions(-) diff --git a/tests/cil/oracle/cpu_a.res.oracle b/tests/cil/oracle/cpu_a.res.oracle index 6623ed53971..5869d63e5dd 100644 --- a/tests/cil/oracle/cpu_a.res.oracle +++ b/tests/cil/oracle/cpu_a.res.oracle @@ -1,5 +1,7 @@ [kernel] Parsing cpu_a.c (with preprocessing) [kernel] Parsing cpu_b.c (with preprocessing) +[kernel] cpu_b.c:7: Warning: + Integer compatibily is machine-dependant : unsigned short and unsigned int /* Generated by Frama-C */ typedef unsigned short DWORD; DWORD f(void) diff --git a/tests/cil/oracle/cpu_b.res.oracle b/tests/cil/oracle/cpu_b.res.oracle index 1567947463f..30fde145f12 100644 --- a/tests/cil/oracle/cpu_b.res.oracle +++ b/tests/cil/oracle/cpu_b.res.oracle @@ -1,5 +1,7 @@ [kernel] Parsing cpu_b.c (with preprocessing) [kernel] Parsing cpu_a.c (with preprocessing) +[kernel] cpu_a.c:6: Warning: + Integer compatibily is machine-dependant : unsigned int and unsigned short /* Generated by Frama-C */ typedef unsigned int DWORD; DWORD f(void); diff --git a/tests/misc/oracle/bts0990_link.res.oracle b/tests/misc/oracle/bts0990_link.res.oracle index 625dcbb43e3..2b6b54c6daa 100644 --- a/tests/misc/oracle/bts0990_link.res.oracle +++ b/tests/misc/oracle/bts0990_link.res.oracle @@ -1,7 +1,8 @@ [kernel] Parsing bts0990_link.i (no preprocessing) [kernel] Parsing bts0990_link_1.i (no preprocessing) [kernel] User Error: Incompatible declaration for s: - different type constructors: char * vs. char [100] + different type constructors: + char * and char [100] First declaration was at bts0990_link.i:8 Current declaration is at bts0990_link_1.i:4 [kernel] Frama-C aborted: invalid user input. diff --git a/tests/syntax/oracle/incompatible_qualifiers.1.res.oracle b/tests/syntax/oracle/incompatible_qualifiers.1.res.oracle index 04b6994f796..6b65e9711ff 100644 --- a/tests/syntax/oracle/incompatible_qualifiers.1.res.oracle +++ b/tests/syntax/oracle/incompatible_qualifiers.1.res.oracle @@ -17,7 +17,7 @@ void k(int *(*f)(int volatile )); fp1 *l(int *(*f)(int )); -int (***m(int *(*f)(int volatile )))(char const ); +fp1 **m(int *(*f)(int volatile )); fp1 * const *n(int *(*f)(int , fp1 **)); diff --git a/tests/syntax/oracle/inconsistent_decl.0.res.oracle b/tests/syntax/oracle/inconsistent_decl.0.res.oracle index eea070edfc9..60a0afd4ee0 100644 --- a/tests/syntax/oracle/inconsistent_decl.0.res.oracle +++ b/tests/syntax/oracle/inconsistent_decl.0.res.oracle @@ -3,7 +3,8 @@ Calling undeclared function f. Old style K&R code? [kernel] Parsing inconsistent_decl_2.i (no preprocessing) [kernel] User Error: Incompatible declaration for f: - different type constructors: int vs. double + different type constructors: + int and double First declaration was at inconsistent_decl.c:12 Current declaration is at inconsistent_decl_2.i:5 [kernel] Frama-C aborted: invalid user input. diff --git a/tests/syntax/oracle/inconsistent_decl.1.res.oracle b/tests/syntax/oracle/inconsistent_decl.1.res.oracle index eb9aa0b9008..1520423b3fd 100644 --- a/tests/syntax/oracle/inconsistent_decl.1.res.oracle +++ b/tests/syntax/oracle/inconsistent_decl.1.res.oracle @@ -4,7 +4,8 @@ Its formals will be inferred from actual arguments [kernel] Parsing inconsistent_decl_2.i (no preprocessing) [kernel] User Error: Incompatible declaration for f: - different type constructors: int vs. double + different type constructors: + int and double First declaration was at inconsistent_decl.c:8 Current declaration is at inconsistent_decl_2.i:5 [kernel] Frama-C aborted: invalid user input. -- GitLab