From 7fbf9a0cee15ddec8987744e72bf6d3370901f59 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 13 Mar 2023 18:57:00 +0100
Subject: [PATCH] [tests] custom machdep validated
---
tests/misc/custom_machdep.ml | 14 ++++++++++++++
tests/misc/custom_machdep.yaml | 14 ++++++++++++++
tests/misc/oracle/custom_machdep.0.res.oracle | 2 +-
tests/misc/oracle/custom_machdep.1.res.oracle | 3 +--
4 files changed, 30 insertions(+), 3 deletions(-)
diff --git a/tests/misc/custom_machdep.ml b/tests/misc/custom_machdep.ml
index 859ea43d5d7..353ed1a7e93 100644
--- a/tests/misc/custom_machdep.ml
+++ b/tests/misc/custom_machdep.ml
@@ -54,6 +54,20 @@ let mach =
"edom", "33";
"eilseq", "84";
"erange", "34";
+ "eintr", "35";
+ "eagain", "36";
+ "ebadf", "37";
+ "efbig", "38";
+ "einval", "39";
+ "eio", "40";
+ "enospc", "41";
+ "eoverflow", "42";
+ "epipe", "43";
+ "espipe", "44";
+ "enxio", "45";
+ "emfile", "46";
+ "enomem", "47";
+ "enotsup", "48";
];
machdep_name = "custom_machdep";
}
diff --git a/tests/misc/custom_machdep.yaml b/tests/misc/custom_machdep.yaml
index 6e66f3e4667..c80687f42c7 100644
--- a/tests/misc/custom_machdep.yaml
+++ b/tests/misc/custom_machdep.yaml
@@ -50,4 +50,18 @@ errno:
edom: "33"
eilseq: "84"
erange: "34"
+ eintr: "35"
+ eagain: "36"
+ ebadf: "37"
+ efbig: "38"
+ einval: "39"
+ eio: "40"
+ enospc: "41"
+ eoverflow: "42"
+ epipe: "43"
+ espipe: "44"
+ enxio: "45"
+ emfile: "46"
+ enomem: "47"
+ enotsup: "48"
machdep_name: custom_machdep
diff --git a/tests/misc/oracle/custom_machdep.0.res.oracle b/tests/misc/oracle/custom_machdep.0.res.oracle
index dfa8454076f..b91b58058f4 100644
--- a/tests/misc/oracle/custom_machdep.0.res.oracle
+++ b/tests/misc/oracle/custom_machdep.0.res.oracle
@@ -19,7 +19,7 @@
int main(void)
{
int __retres;
- __retres = (int)2147483647;
+ __retres = 8388607;
return __retres;
}
diff --git a/tests/misc/oracle/custom_machdep.1.res.oracle b/tests/misc/oracle/custom_machdep.1.res.oracle
index 10262698fca..3675c7e7488 100644
--- a/tests/misc/oracle/custom_machdep.1.res.oracle
+++ b/tests/misc/oracle/custom_machdep.1.res.oracle
@@ -1,4 +1,3 @@
-[kernel] Registering machdep 'mach' as 'custom'
[kernel] Parsing custom_machdep.c (with preprocessing)
/* Generated by Frama-C */
#include "ctype.h"
@@ -19,7 +18,7 @@
int main(void)
{
int __retres;
- __retres = (int)2147483647;
+ __retres = 8388607;
return __retres;
}
--
GitLab