Merge branch 'feature/virgile/no-fork' into 'master'

More robust tests for builtins

See merge request frama-c/e-acsl!283

src/plugins/e-acsl/share/e-acsl/e_acsl_assert.h

@@ -58,15 +58,20 @@ static void exec_abort(int line, const char *file) {
   trace();
 #endif
 #endif
-  kill(getpid(), SIGABRT);
+ raise(SIGABRT);
 }
 
 /*! \brief Print a message to stderr and abort the execution */
 static void vabort(char *fmt, ...) {
   va_list va;
+  sigset_t defer_abrt;
+  sigemptyset(&defer_abrt);
+  sigaddset(&defer_abrt,SIGABRT);
+  sigprocmask(SIG_BLOCK,&defer_abrt,NULL);
   va_start(va,fmt);
   _format(NULL,_charc_stderr,fmt,va);
   va_end(va);
+  sigprocmask(SIG_UNBLOCK,&defer_abrt,NULL);
   runtime_abort();
 }
 

src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle

-[kernel:typing:implicit-function-declaration] tests/builtin/strcat.c:26: Warning: 
-  Calling undeclared function fork. Old style K&R code?
 [e-acsl] beginning translation.
 [e-acsl] Warning: annotating undefined function `exit':
   the generated program may miss memory instrumentation
   if there are memory-related annotations.
-[e-acsl] Warning: annotating undefined function `waitpid':
-  the generated program may miss memory instrumentation
-  if there are memory-related annotations.
 [e-acsl] Warning: annotating undefined function `strcat':
   the generated program may miss memory instrumentation
   if there are memory-related annotations.
@@ -15,8 +10,16 @@
   if there are memory-related annotations.
 [kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:169: Warning: 
   Neither code nor specification for function printf, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/builtin/strcat.c:26: Warning: 
-  Neither code nor specification for function fork, generating default assigns from the prototype
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/setjmp.h:47: Warning: 
+  Neither code nor specification for function sigsetjmp, generating default assigns from the prototype
+[kernel:annot:missing-spec] tests/builtin/signalled.h:14: Warning: 
+  Neither code nor specification for function signal_eval, generating default assigns from the prototype
+[kernel:annot:missing-spec] tests/builtin/signalled.h:18: Warning: 
+  Neither code nor specification for function get_jmp_ctxt, generating default assigns from the prototype
+[kernel:annot:missing-spec] tests/builtin/signalled.h:20: Warning: 
+  Neither code nor specification for function set_handler, generating default assigns from the prototype
+[kernel:annot:missing-spec] tests/builtin/signalled.h:22: Warning: 
+  Neither code nor specification for function test_successful, generating default assigns from the prototype
 [e-acsl] FRAMAC_SHARE/libc/string.h:409: Warning: 
   E-ACSL construct `logic function application' is not yet supported.
   Ignoring annotation.
@@ -59,10 +62,7 @@
 [e-acsl] FRAMAC_SHARE/libc/string.h:403: Warning: 
   E-ACSL construct `logic function returning an integer' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:92: Warning: 
-  E-ACSL construct `assigns clause in behavior' is not yet supported.
-  Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:86: Warning: 
+[e-acsl] FRAMAC_SHARE/libc/string.h:404: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
@@ -75,7 +75,6 @@
   __e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
   __e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
   __e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
-  testno ∈ {0}
   __gen_e_acsl_literal_string ∈ {0}
   __gen_e_acsl_literal_string_2 ∈ {0}
   __gen_e_acsl_literal_string_3 ∈ {0}
@@ -101,115 +100,13 @@
   __gen_e_acsl_literal_string_23 ∈ {0}
   __gen_e_acsl_literal_string_24 ∈ {0}
   __gen_e_acsl_literal_string_25 ∈ {0}
-  __gen_e_acsl_literal_string_26 ∈ {0}
-  __gen_e_acsl_literal_string_27 ∈ {0}
-  __gen_e_acsl_literal_string_28 ∈ {0}
-  __gen_e_acsl_literal_string_29 ∈ {0}
 [eva] using specification for function __e_acsl_memory_init
 [eva] using specification for function __e_acsl_store_block
 [eva] using specification for function __e_acsl_full_init
 [eva] using specification for function __e_acsl_mark_readonly
 [eva] tests/builtin/strcat.c:11: allocating variable __malloc_main_l11
-[eva] using specification for function fork
-[eva] using specification for function __e_acsl_builtin_strcat
-[eva] using specification for function __e_acsl_assert
-[eva] using specification for function __e_acsl_delete_block
-[eva:alarm] FRAMAC_SHARE/libc/string.h:399: Warning: 
-  function __gen_e_acsl_strcat: postcondition 'sum_of_lengths' got status unknown.
-[eva] using specification for function exit
-[eva] using specification for function __e_acsl_valid
-[eva] using specification for function waitpid
-[eva] using specification for function __e_acsl_initialized
-[eva:alarm] FRAMAC_SHARE/libc/sys/wait.h:86: Warning: 
-  function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/sys/wait.h:86: Warning: 
-  function __gen_e_acsl_waitpid: postcondition 'initialization,stat_loc_init_on_success' got status unknown.
-[eva:alarm] tests/builtin/strcat.c:26: Warning: 
-  accessing uninitialized left-value. assert \initialized(&process_status);
-[eva] using specification for function printf
+[eva] tests/builtin/strcat.c:12: allocating variable __malloc_main_l12
+[eva] using specification for function get_jmp_ctxt
 [eva:alarm] tests/builtin/strcat.c:27: Warning: 
-  accessing uninitialized left-value. assert \initialized(&process_status_0);
-[eva:alarm] tests/builtin/strcat.c:28: Warning: 
-  function __gen_e_acsl_strcat: precondition 'room_string' got status invalid.
-[eva:alarm] tests/builtin/strcat.c:28: Warning: 
-  accessing uninitialized left-value. assert \initialized(&process_status_1);
-[eva:alarm] tests/builtin/strcat.c:29: Warning: 
-  accessing left-value that contains escaping addresses.
-  assert ¬\dangling(&unalloc_str);
-[eva:alarm] tests/builtin/strcat.c:29: Warning: 
-  function __gen_e_acsl_strcat: precondition 'valid_string_dest' got status invalid.
-[eva:alarm] tests/builtin/strcat.c:29: Warning: 
-  accessing uninitialized left-value. assert \initialized(&process_status_2);
-[eva:alarm] tests/builtin/strcat.c:30: Warning: 
-  accessing left-value that contains escaping addresses.
-  assert ¬\dangling(&unalloc_str);
-[eva:alarm] tests/builtin/strcat.c:30: Warning: 
-  function __gen_e_acsl_strcat: precondition 'valid_string_src' got status invalid.
-[eva:alarm] tests/builtin/strcat.c:30: Warning: 
-  accessing uninitialized left-value. assert \initialized(&process_status_3);
-[eva:alarm] tests/builtin/strcat.c:31: Warning: 
-  function __gen_e_acsl_strcat: precondition 'valid_string_dest' got status invalid.
-[eva:alarm] tests/builtin/strcat.c:31: Warning: 
-  accessing uninitialized left-value. assert \initialized(&process_status_4);
-[eva:alarm] tests/builtin/strcat.c:32: Warning: 
-  function __gen_e_acsl_strcat: precondition 'valid_string_src' got status invalid.
-[eva:alarm] tests/builtin/strcat.c:32: Warning: 
-  accessing uninitialized left-value. assert \initialized(&process_status_5);
-[eva:alarm] tests/builtin/strcat.c:33: Warning: 
-  function __gen_e_acsl_strcat: precondition 'valid_string_dest' got status invalid.
-[eva:alarm] tests/builtin/strcat.c:33: Warning: 
-  accessing uninitialized left-value. assert \initialized(&process_status_6);
-[eva:alarm] tests/builtin/strcat.c:34: Warning: 
-  accessing uninitialized left-value. assert \initialized(&process_status_7);
-[eva:alarm] tests/builtin/strcat.c:35: Warning: 
-  accessing uninitialized left-value. assert \initialized(&process_status_8);
-[eva:alarm] tests/builtin/strcat.c:36: Warning: 
-  accessing uninitialized left-value. assert \initialized(&process_status_9);
-[eva] using specification for function __e_acsl_initialize
-[eva:alarm] tests/builtin/strcat.c:37: Warning: 
-  accessing uninitialized left-value. assert \initialized(&process_status_10);
-[eva] using specification for function __e_acsl_builtin_strncat
-[eva:alarm] FRAMAC_SHARE/libc/string.h:420: Warning: 
-  function __gen_e_acsl_strncat, behavior complete: postcondition 'sum_of_lengths' got status unknown.
-[eva:alarm] tests/builtin/strcat.c:40: Warning: 
-  accessing uninitialized left-value. assert \initialized(&process_status_11);
-[eva:alarm] tests/builtin/strcat.c:41: Warning: 
-  function __gen_e_acsl_strncat, behavior complete: precondition 'room_string' got status invalid.
-[eva:alarm] tests/builtin/strcat.c:41: Warning: 
-  accessing uninitialized left-value. assert \initialized(&process_status_12);
-[eva:alarm] tests/builtin/strcat.c:42: Warning: 
-  accessing left-value that contains escaping addresses.
-  assert ¬\dangling(&unalloc_str);
-[eva:alarm] tests/builtin/strcat.c:42: Warning: 
-  function __gen_e_acsl_strncat: precondition 'valid_string_dest' got status invalid.
-[eva:alarm] tests/builtin/strcat.c:42: Warning: 
-  accessing uninitialized left-value. assert \initialized(&process_status_13);
-[eva:alarm] tests/builtin/strcat.c:43: Warning: 
-  accessing left-value that contains escaping addresses.
-  assert ¬\dangling(&unalloc_str);
-[eva:alarm] tests/builtin/strcat.c:43: Warning: 
-  function __gen_e_acsl_strncat: precondition 'valid_nstring_src' got status invalid.
-[eva:alarm] tests/builtin/strcat.c:43: Warning: 
-  accessing uninitialized left-value. assert \initialized(&process_status_14);
-[eva:alarm] tests/builtin/strcat.c:44: Warning: 
-  function __gen_e_acsl_strncat: precondition 'valid_string_dest' got status invalid.
-[eva:alarm] tests/builtin/strcat.c:44: Warning: 
-  accessing uninitialized left-value. assert \initialized(&process_status_15);
-[eva:alarm] tests/builtin/strcat.c:45: Warning: 
-  function __gen_e_acsl_strncat: precondition 'valid_nstring_src' got status invalid.
-[eva:alarm] tests/builtin/strcat.c:45: Warning: 
-  accessing uninitialized left-value. assert \initialized(&process_status_16);
-[eva:alarm] tests/builtin/strcat.c:46: Warning: 
-  function __gen_e_acsl_strncat: precondition 'valid_string_dest' got status invalid.
-[eva:alarm] tests/builtin/strcat.c:46: Warning: 
-  accessing uninitialized left-value. assert \initialized(&process_status_17);
-[eva:alarm] FRAMAC_SHARE/libc/string.h:428: Warning: 
-  function __gen_e_acsl_strncat, behavior partial: postcondition 'sum_of_bounded_lengths' got status unknown.
-[eva:alarm] tests/builtin/strcat.c:48: Warning: 
-  accessing uninitialized left-value. assert \initialized(&process_status_18);
-[eva:alarm] tests/builtin/strcat.c:49: Warning: 
-  accessing uninitialized left-value. assert \initialized(&process_status_19);
-[eva:alarm] tests/builtin/strcat.c:50: Warning: 
-  accessing uninitialized left-value. assert \initialized(&process_status_20);
-[eva] using specification for function __e_acsl_memory_clean
+  out of bounds read. assert \valid_read(jmp_ctxt);
 [eva] done for function main

src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle

-[kernel:typing:implicit-function-declaration] tests/builtin/strlen.c:18: Warning: 
-  Calling undeclared function fork. Old style K&R code?
 [e-acsl] beginning translation.
 [e-acsl] Warning: annotating undefined function `abort':
   the generated program may miss memory instrumentation
@@ -7,9 +5,6 @@
 [e-acsl] Warning: annotating undefined function `exit':
   the generated program may miss memory instrumentation
   if there are memory-related annotations.
-[e-acsl] Warning: annotating undefined function `waitpid':
-  the generated program may miss memory instrumentation
-  if there are memory-related annotations.
 [e-acsl] Warning: annotating undefined function `strlen':
   the generated program may miss memory instrumentation
   if there are memory-related annotations.
@@ -18,8 +13,16 @@
   if there are memory-related annotations.
 [kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:169: Warning: 
   Neither code nor specification for function printf, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/builtin/strlen.c:18: Warning: 
-  Neither code nor specification for function fork, generating default assigns from the prototype
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/setjmp.h:47: Warning: 
+  Neither code nor specification for function sigsetjmp, generating default assigns from the prototype
+[kernel:annot:missing-spec] tests/builtin/signalled.h:14: Warning: 
+  Neither code nor specification for function signal_eval, generating default assigns from the prototype
+[kernel:annot:missing-spec] tests/builtin/signalled.h:18: Warning: 
+  Neither code nor specification for function get_jmp_ctxt, generating default assigns from the prototype
+[kernel:annot:missing-spec] tests/builtin/signalled.h:20: Warning: 
+  Neither code nor specification for function set_handler, generating default assigns from the prototype
+[kernel:annot:missing-spec] tests/builtin/signalled.h:22: Warning: 
+  Neither code nor specification for function test_successful, generating default assigns from the prototype
 [e-acsl] FRAMAC_SHARE/libc/stdlib.h:394: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
@@ -41,10 +44,7 @@
 [e-acsl] FRAMAC_SHARE/libc/string.h:127: Warning: 
   E-ACSL construct `logic function returning an integer' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:92: Warning: 
-  E-ACSL construct `assigns clause in behavior' is not yet supported.
-  Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:86: Warning: 
+[e-acsl] FRAMAC_SHARE/libc/string.h:127: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/stdlib.h:406: Warning: 
@@ -60,7 +60,6 @@
   __e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
   __e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
   __e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
-  testno ∈ {0}
   __gen_e_acsl_literal_string ∈ {0}
   __gen_e_acsl_literal_string_2 ∈ {0}
   __gen_e_acsl_literal_string_3 ∈ {0}
@@ -72,10 +71,6 @@
   __gen_e_acsl_literal_string_9 ∈ {0}
   __gen_e_acsl_literal_string_10 ∈ {0}
   __gen_e_acsl_literal_string_11 ∈ {0}
-  __gen_e_acsl_literal_string_12 ∈ {0}
-  __gen_e_acsl_literal_string_13 ∈ {0}
-  __gen_e_acsl_literal_string_14 ∈ {0}
-  __gen_e_acsl_literal_string_15 ∈ {0}
 [eva] using specification for function __e_acsl_memory_init
 [eva] using specification for function __e_acsl_store_block
 [eva] using specification for function __e_acsl_full_init
@@ -94,31 +89,7 @@
   function __gen_e_acsl_strdup, behavior allocation: postcondition 'result_valid_string_and_same_contents' got status invalid. (Behavior may be inactive, no reduction performed.)
 [eva:alarm] FRAMAC_SHARE/libc/string.h:456: Warning: 
   function __gen_e_acsl_strdup, behavior no_allocation: postcondition 'result_null' got status unknown. (Behavior may be inactive, no reduction performed.)
-[eva] using specification for function fork
-[eva] using specification for function __e_acsl_builtin_strlen
-[eva] using specification for function exit
-[eva] using specification for function __e_acsl_valid
-[eva] using specification for function __e_acsl_assert
-[eva] using specification for function waitpid
-[eva] using specification for function __e_acsl_initialized
-[eva:alarm] FRAMAC_SHARE/libc/sys/wait.h:86: Warning: 
-  function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/sys/wait.h:86: Warning: 
-  function __gen_e_acsl_waitpid: postcondition 'initialization,stat_loc_init_on_success' got status unknown.
+[eva] using specification for function get_jmp_ctxt
 [eva:alarm] tests/builtin/strlen.c:18: Warning: 
-  accessing uninitialized left-value. assert \initialized(&process_status);
-[eva] using specification for function printf
-[eva:alarm] tests/builtin/strlen.c:19: Warning: 
-  function __gen_e_acsl_strlen: precondition 'valid_string_s' got status invalid.
-[eva:alarm] tests/builtin/strlen.c:19: Warning: 
-  accessing uninitialized left-value. assert \initialized(&process_status_0);
-[eva:alarm] tests/builtin/strlen.c:20: Warning: 
-  accessing uninitialized left-value. assert \initialized(&process_status_1);
-[eva:alarm] tests/builtin/strlen.c:21: Warning: 
-  accessing uninitialized left-value. assert \initialized(&process_status_2);
-[eva] using specification for function __e_acsl_initialize
-[eva:alarm] tests/builtin/strlen.c:23: Warning: 
-  out of bounds write. assert \valid(heap_str + 7);
-[kernel] tests/builtin/strlen.c:23: Warning: 
-  all target addresses were invalid. This path is assumed to be dead.
+  out of bounds read. assert \valid_read(jmp_ctxt);
 [eva] done for function main