diff --git a/tests/misc/custom_machdep.ml b/tests/misc/custom_machdep.ml index 859ea43d5d791e301d341c8d31ee8e78e63de703..353ed1a7e9320a55a26961c0a6e59c533ce9e742 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 6e66f3e4667510741e042e14385e8e63964dff42..c80687f42c7e9131b35087845516230cead5fdee 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 dfa8454076f143b1f9a7fd8f5d71a56519f74ab5..b91b58058f4486e6d3e8c821c1de66e82feabaf6 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 10262698fca641f0558ec346f437476b0285b833..3675c7e748885404d5de8fd617fcacf6db3dffd0 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; }