From cf384a5acef4afa2e8004fd1006ac150d2a56f26 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr> Date: Mon, 4 Jul 2022 15:14:16 +0200 Subject: [PATCH] [Eva] Updates test oracles. --- tests/builtins/oracle/imprecise.res.oracle | 8 ++++---- tests/value/oracle/replace_by_show_each.res.oracle | 4 ++-- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/tests/builtins/oracle/imprecise.res.oracle b/tests/builtins/oracle/imprecise.res.oracle index c5d23a2cbd6..aac1b7410d2 100644 --- a/tests/builtins/oracle/imprecise.res.oracle +++ b/tests/builtins/oracle/imprecise.res.oracle @@ -228,16 +228,16 @@ [kernel] imprecise.c:114: approximating value to write. [eva:alarm] imprecise.c:116: Warning: assertion got status unknown. [eva] Recording results for many_writes -[kernel] imprecise.c:111: - more than 200(300) elements to enumerate. Approximating. -[kernel] imprecise.c:114: - more than 200(300) elements to enumerate. Approximating. [from] Computing for function many_writes [kernel] imprecise.c:111: more than 200(300) dependencies to update. Approximating. [kernel] imprecise.c:114: more than 200(300) dependencies to update. Approximating. [from] Done for function many_writes +[kernel] imprecise.c:111: + more than 200(300) elements to enumerate. Approximating. +[kernel] imprecise.c:114: + more than 200(300) elements to enumerate. Approximating. [eva] Done for function many_writes [eva] computing for function overlap <- main. Called from imprecise.c:151. diff --git a/tests/value/oracle/replace_by_show_each.res.oracle b/tests/value/oracle/replace_by_show_each.res.oracle index 85c7d6b9a71..18b7f724883 100644 --- a/tests/value/oracle/replace_by_show_each.res.oracle +++ b/tests/value/oracle/replace_by_show_each.res.oracle @@ -6,10 +6,10 @@ x ∈ {0} [eva] replace_by_show_each.c:23: Frama_C_show_each_2: [eva] replace_by_show_each.c:25: Frama_C_show_each_1: -[inout] Warning: no assigns clauses for function Frama_C_show_each_1. - Results will be imprecise. [from] Warning: no assigns clauses for function Frama_C_show_each_1. Results will be imprecise. +[inout] Warning: no assigns clauses for function Frama_C_show_each_1. + Results will be imprecise. [eva:alarm] replace_by_show_each.c:26: Warning: signed overflow. assert j + 1 ≤ 2147483647; [eva] Recording results for main -- GitLab