From 24e9c20ed711bfabb11d917937e3a36c23efa2b5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 16 Feb 2023 12:20:01 +0100
Subject: [PATCH] [libc] Fixes stub for getopt.

---
 share/libc/unistd.c                    |  4 ++--
 tests/libc/oracle/fc_libc.1.res.oracle |  5 ++---
 tests/libc/oracle/unistd_c.res.oracle  | 10 +++++-----
 3 files changed, 9 insertions(+), 10 deletions(-)

diff --git a/share/libc/unistd.c b/share/libc/unistd.c
index 3481dfecd31..e339084604f 100644
--- a/share/libc/unistd.c
+++ b/share/libc/unistd.c
@@ -36,8 +36,8 @@ int getopt(int argc, char * const argv[], const char *optstring) {
     return -1;
   }
   int nondet_ind = Frama_C_interval(1, argc - 1);
-  int nondet_indlen = Frama_C_interval(0, strlen(argv[nondet_ind]));
-  optarg = Frama_C_nondet_ptr(0, &argv[nondet_ind][nondet_indlen-1]);
+  int nondet_indlen = Frama_C_interval(0, strlen(argv[nondet_ind])-1);
+  optarg = Frama_C_nondet_ptr(0, &argv[nondet_ind][nondet_indlen]);
   optind = Frama_C_interval(1, argc + 1);
   return Frama_C_nondet(-1, Frama_C_unsigned_char_interval(0, UCHAR_MAX));
 }
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 8be076d9a80..57ab4d44afc 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -8600,11 +8600,10 @@ int getopt(int argc, char * const *argv, char const *optstring)
   }
   int nondet_ind = Frama_C_interval(1,argc - 1);
   tmp_0 = strlen((char const *)*(argv + nondet_ind));
-  tmp_1 = Frama_C_interval(0,(int)tmp_0);
+  tmp_1 = Frama_C_interval(0,(int)(tmp_0 - (size_t)1));
   int nondet_indlen = tmp_1;
   optarg = (char *)Frama_C_nondet_ptr((void *)0,
-                                      (void *)(*(argv + nondet_ind) + (
-                                               nondet_indlen - 1)));
+                                      (void *)(*(argv + nondet_ind) + nondet_indlen));
   optind = Frama_C_interval(1,argc + 1);
   tmp_2 = Frama_C_unsigned_char_interval((unsigned char)0,(unsigned char)255);
   tmp_3 = Frama_C_nondet(-1,(int)tmp_2);
diff --git a/tests/libc/oracle/unistd_c.res.oracle b/tests/libc/oracle/unistd_c.res.oracle
index 89baa329003..5321b25be6a 100644
--- a/tests/libc/oracle/unistd_c.res.oracle
+++ b/tests/libc/oracle/unistd_c.res.oracle
@@ -47,17 +47,17 @@
 [eva:final-states] Values at end of function getopt:
   Frama_C_entropy_source ∈ [--..--]
   optarg ∈
-        {{ NULL ; "-this" + {-1; 0; 1; 2; 3; 4} ;
-           "is a" + {-1; 0; 1; 2; 3; 4} ; "Test0" + {-1; 0; 1; 2; 3; 4} }}
+        {{ NULL ; "-this" + {0; 1; 2; 3; 4} ; "is a" + {0; 1; 2; 3; 4} ;
+           "Test0" + {0; 1; 2; 3; 4} }}
   optind ∈ {1; 2; 3; 4; 5}
   nondet_ind ∈ {1; 2; 3}
-  nondet_indlen ∈ {0; 1; 2; 3; 4; 5}
+  nondet_indlen ∈ {0; 1; 2; 3; 4}
   __retres ∈ [-1..255]
 [eva:final-states] Values at end of function main:
   Frama_C_entropy_source ∈ [--..--]
   optarg ∈
-        {{ NULL ; "-this" + {-1; 0; 1; 2; 3; 4} ;
-           "is a" + {-1; 0; 1; 2; 3; 4} ; "Test0" + {-1; 0; 1; 2; 3; 4} }}
+        {{ NULL ; "-this" + {0; 1; 2; 3; 4} ; "is a" + {0; 1; 2; 3; 4} ;
+           "Test0" + {0; 1; 2; 3; 4} }}
   optind ∈ {1; 2; 3; 4; 5}
   argc ∈ {4}
   argv[0] ∈ {{ "program_name" }}
-- 
GitLab