Merge branch 'feature/basile/reactivate-builtin-tests' into 'master'

[eacsl] Reactivate tests for builtins

See merge request frama-c/frama-c!3217

src/plugins/e-acsl/Makefile.in

@@ -176,10 +176,8 @@ PLUGIN_TESTS_DIRS := \
 	full-mtracking \
 	format \
 	temporal \
-	special
-# [JS 2019/02/26] deactivate tests 'builtin' as long as setjmp/longjmp is not
-# supported.
-#	builtin
+	special \
+	builtin
 
 PLUGIN_TESTS_LIB := $(EACSL_PLUGIN_DIR)/tests/print.ml
 

src/plugins/e-acsl/src/code_generator/contract.ml

@@ -595,7 +595,7 @@ let check_complete_and_disjoint kf kinstr env contract =
     Cil.CurrentLoc.set contract.location;
     Options.warning
       ~current:true
-      "@[Some assumes clauses couldn't be translated.@ Ignoring complete and \
+      "@[Some assumes clauses could not be translated.@ Ignoring complete and \
        disjoint behaviors annotations.@]";
     env
   end

src/plugins/e-acsl/tests/bts/oracle_ci/bts2252.res.oracle

@@ -14,7 +14,7 @@
   E-ACSL construct `logic functions with labels' is not yet supported.
   Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/string.h:365: Warning: 
-  Some assumes clauses couldn't be translated.
+  Some assumes clauses could not be translated.
   Ignoring complete and disjoint behaviors annotations.
 [e-acsl] FRAMAC_SHARE/libc/string.h:365: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.

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

@@ -2,112 +2,105 @@
 [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 `fork':
+  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.
 [e-acsl] Warning: annotating undefined function `strncat':
   the generated program may miss memory instrumentation
   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] 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:421: Warning: 
-  E-ACSL construct `logic function application' is not yet supported.
-  Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:422: Warning: 
-  E-ACSL construct `logic function application' is not yet supported.
+[e-acsl] FRAMAC_SHARE/libc/string.h:432: Warning: 
+  E-ACSL construct `logic functions performing read accesses'
+  is not yet supported.
+  Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:440: Warning: 
+  E-ACSL construct `logic functions performing read accesses'
+  is not yet supported.
+  Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:426: Warning: 
+  E-ACSL construct `logic functions with labels' is not yet supported.
   Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/string.h:427: Warning: 
-  E-ACSL construct `logic function application' is not yet supported.
+  E-ACSL construct `logic functions with labels' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:435: Warning: 
-  E-ACSL construct `logic function application' is not yet supported.
+[e-acsl] FRAMAC_SHARE/libc/string.h:433: Warning: 
+  E-ACSL construct `logic functions performing read accesses'
+  is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:435: Warning: 
+[e-acsl] FRAMAC_SHARE/libc/string.h:441: Warning: 
+  E-ACSL construct `logic functions performing read accesses'
+  is not yet supported.
+  Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:425: Warning: 
+  Some assumes clauses could not be translated.
+  Ignoring complete and disjoint behaviors annotations.
+[e-acsl] FRAMAC_SHARE/libc/string.h:425: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:427: Warning: 
+[e-acsl] FRAMAC_SHARE/libc/string.h:430: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:425: Warning: 
+[e-acsl] FRAMAC_SHARE/libc/string.h:437: Warning: 
+  E-ACSL construct `logic functions performing read accesses'
+  is not yet supported.
+  Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:437: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:406: Warning: 
-  E-ACSL construct `logic function application' is not yet supported.
+[e-acsl] FRAMAC_SHARE/libc/string.h:445: Warning: 
+  E-ACSL construct `logic functions performing read accesses'
+  is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:407: Warning: 
-  E-ACSL construct `logic function application' is not yet supported.
+[e-acsl] FRAMAC_SHARE/libc/string.h:411: Warning: 
+  E-ACSL construct `logic functions with labels' is not yet supported.
+  Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:412: Warning: 
+  E-ACSL construct `logic functions with labels' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:408: Warning: 
-  E-ACSL construct `logic function returning an integer' is not yet supported.
+[e-acsl] FRAMAC_SHARE/libc/string.h:413: Warning: 
+  E-ACSL construct `logic functions performing read accesses'
+  is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:408: Warning: 
+[e-acsl] FRAMAC_SHARE/libc/string.h:410: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:411: Warning: 
-  E-ACSL construct `logic function returning an integer' is not yet supported.
+[e-acsl] FRAMAC_SHARE/libc/string.h:416: Warning: 
+  E-ACSL construct `logic functions performing read accesses'
+  is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:414: Warning: 
-  E-ACSL construct `logic function returning an integer' is not yet supported.
+[e-acsl] FRAMAC_SHARE/libc/string.h:419: Warning: 
+  E-ACSL construct `logic functions performing read accesses'
+  is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:415: Warning: 
-  E-ACSL construct `logic function returning an integer' is not yet supported.
+[e-acsl] FRAMAC_SHARE/libc/string.h:420: Warning: 
+  E-ACSL construct `logic functions performing read accesses'
+  is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:416: Warning: 
+[e-acsl] FRAMAC_SHARE/libc/unistd.h:856: Warning: 
+  E-ACSL construct `assigns clause in behavior' is not yet supported.
+  Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:79: 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 construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:470: Warning: 
+  E-ACSL construct `assigns clause in behavior' is not yet supported.
+  Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:472: Warning: 
+  E-ACSL construct `abnormal termination case in behavior'
+  is not yet supported.
+  Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
-[eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
-  __e_acsl_init ∈ [--..--]
-  __e_acsl_heap_allocation_size ∈ [--..--]
-  __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]
-  __e_acsl_sound_verdict ∈ [--..--]
-  __gen_e_acsl_literal_string ∈ {0}
-  __gen_e_acsl_literal_string_2 ∈ {0}
-  __gen_e_acsl_literal_string_3 ∈ {0}
-  __gen_e_acsl_literal_string_4 ∈ {0}
-  __gen_e_acsl_literal_string_5 ∈ {0}
-  __gen_e_acsl_literal_string_6 ∈ {0}
-  __gen_e_acsl_literal_string_7 ∈ {0}
-  __gen_e_acsl_literal_string_8 ∈ {0}
-  __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}
-  __gen_e_acsl_literal_string_16 ∈ {0}
-  __gen_e_acsl_literal_string_17 ∈ {0}
-  __gen_e_acsl_literal_string_18 ∈ {0}
-  __gen_e_acsl_literal_string_19 ∈ {0}
-  __gen_e_acsl_literal_string_20 ∈ {0}
-  __gen_e_acsl_literal_string_21 ∈ {0}
-  __gen_e_acsl_literal_string_22 ∈ {0}
-  __gen_e_acsl_literal_string_23 ∈ {0}
-  __gen_e_acsl_literal_string_24 ∈ {0}
-  __gen_e_acsl_literal_string_25 ∈ {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] 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: 
-  out of bounds read. assert \valid_read(jmp_ctxt);
-[eva] done for function main
+[eva:alarm] FRAMAC_SHARE/libc/unistd.h:859: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/unistd.h:859: Warning: 
+  function __gen_e_acsl_fork: postcondition 'result_ok_child_or_error' got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:416: Warning: 
+  function __gen_e_acsl_strcat: postcondition 'sum_of_lengths' got status unknown.

src/plugins/e-acsl/tests/builtin/oracle_dev/strcat.e-acsl.err.log

+TEST 1: OK: Expected execution at tests/builtin/strcat.c:27
+TEST 2: OK: Expected execution at tests/builtin/strcat.c:28
+strcat: insufficient space in destination string, available: 8 bytes, requires at least 9 bytes
+TEST 3: OK: Expected signal at tests/builtin/strcat.c:29
+strcat: destination string string unallocated
+TEST 4: OK: Expected signal at tests/builtin/strcat.c:30
+strcat: source string string unallocated
+TEST 5: OK: Expected signal at tests/builtin/strcat.c:31
+strcat: destination string string unallocated
+TEST 6: OK: Expected signal at tests/builtin/strcat.c:32
+strcat: source string string unallocated
+TEST 7: OK: Expected signal at tests/builtin/strcat.c:33
+strcat: destination string string is not writable
+TEST 8: OK: Expected signal at tests/builtin/strcat.c:34
+strcat: overlapping memory areas
+TEST 9: OK: Expected signal at tests/builtin/strcat.c:35
+strcat: overlapping memory areas
+TEST 10: OK: Expected signal at tests/builtin/strcat.c:36
+strcat: overlapping memory areas
+TEST 11: OK: Expected signal at tests/builtin/strcat.c:37
+TEST 12: OK: Expected execution at tests/builtin/strcat.c:38
+TEST 13: OK: Expected execution at tests/builtin/strcat.c:51
+strncat: insufficient space in destination string, available: 8 bytes, requires at least 9 bytes
+TEST 14: OK: Expected signal at tests/builtin/strcat.c:52
+strcat: destination string string unallocated
+TEST 15: OK: Expected signal at tests/builtin/strcat.c:53
+strncat: source string string unallocated
+TEST 16: OK: Expected signal at tests/builtin/strcat.c:54
+strcat: destination string string unallocated
+TEST 17: OK: Expected signal at tests/builtin/strcat.c:55
+strncat: source string string unallocated
+TEST 18: OK: Expected signal at tests/builtin/strcat.c:56
+strcat: destination string string is not writable
+TEST 19: OK: Expected signal at tests/builtin/strcat.c:57
+strcat: overlapping memory areas
+TEST 20: OK: Expected signal at tests/builtin/strcat.c:59
+strncat: insufficient space in destination string, available: 6 bytes, requires at least 7 bytes
+TEST 21: OK: Expected signal at tests/builtin/strcat.c:60
+strcat: overlapping memory areas
+TEST 22: OK: Expected signal at tests/builtin/strcat.c:61

src/plugins/e-acsl/tests/builtin/oracle_dev/strcmp.e-acsl.err.log

+TEST 1: OK: Expected execution at tests/builtin/strcmp.c:32
+TEST 2: OK: Expected execution at tests/builtin/strcmp.c:33
+TEST 3: OK: Expected execution at tests/builtin/strcmp.c:34
+strcmp: string 1 string not NUL-terminated
+TEST 4: OK: Expected signal at tests/builtin/strcmp.c:37
+strcmp: string 2 string not NUL-terminated
+TEST 5: OK: Expected signal at tests/builtin/strcmp.c:39
+strcmp: string 1 string not NUL-terminated
+TEST 6: OK: Expected signal at tests/builtin/strcmp.c:41
+strcmp: string 2 string not NUL-terminated
+TEST 7: OK: Expected signal at tests/builtin/strcmp.c:43
+strcmp: string 2 string unallocated
+TEST 8: OK: Expected signal at tests/builtin/strcmp.c:45
+strcmp: string 1 string unallocated
+TEST 9: OK: Expected signal at tests/builtin/strcmp.c:46
+strcmp: string 1 string unallocated
+TEST 10: OK: Expected signal at tests/builtin/strcmp.c:51
+strcmp: string 2 string unallocated
+TEST 11: OK: Expected signal at tests/builtin/strcmp.c:52
+TEST 12: OK: Expected execution at tests/builtin/strcmp.c:64
+TEST 13: OK: Expected execution at tests/builtin/strcmp.c:65
+TEST 14: OK: Expected execution at tests/builtin/strcmp.c:66
+TEST 15: OK: Expected execution at tests/builtin/strcmp.c:68
+TEST 16: OK: Expected execution at tests/builtin/strcmp.c:69
+TEST 17: OK: Expected execution at tests/builtin/strcmp.c:73
+TEST 18: OK: Expected execution at tests/builtin/strcmp.c:75
+TEST 19: OK: Expected execution at tests/builtin/strcmp.c:77
+TEST 20: OK: Expected execution at tests/builtin/strcmp.c:79
+strncmp: string 2 string has insufficient length
+TEST 21: OK: Expected signal at tests/builtin/strcmp.c:82
+strncmp: string 2 string has insufficient length
+TEST 22: OK: Expected signal at tests/builtin/strcmp.c:84
+strncmp: string 2 string has insufficient length
+TEST 23: OK: Expected signal at tests/builtin/strcmp.c:85
+strncmp: string 1 string has insufficient length
+TEST 24: OK: Expected signal at tests/builtin/strcmp.c:87

src/plugins/e-acsl/tests/builtin/oracle_dev/strcpy.e-acsl.err.log

+TEST 1: OK: Expected execution at tests/builtin/strcpy.c:21
+TEST 2: OK: Expected execution at tests/builtin/strcpy.c:22
+strlen: insufficient space in destination string, at least 5 bytes required
+TEST 3: OK: Expected signal at tests/builtin/strcpy.c:23
+strlen: destination string space unallocated or cannot be written
+TEST 4: OK: Expected signal at tests/builtin/strcpy.c:24
+strlen: destination string space unallocated or cannot be written
+TEST 5: OK: Expected signal at tests/builtin/strcpy.c:25
+TEST 6: OK: Expected execution at tests/builtin/strcpy.c:26
+strcpy: overlapping memory areas
+TEST 7: OK: Expected signal at tests/builtin/strcpy.c:27
+TEST 8: OK: Expected execution at tests/builtin/strcpy.c:28
+strcpy: overlapping memory areas
+TEST 9: OK: Expected signal at tests/builtin/strcpy.c:29
+TEST 10: OK: Expected execution at tests/builtin/strcpy.c:32
+strncpy: insufficient space in destination string , at least 6 bytes required
+TEST 11: OK: Expected signal at tests/builtin/strcpy.c:33
+strncpy: destination string  space unallocated or cannot be written
+TEST 12: OK: Expected signal at tests/builtin/strcpy.c:34
+strncpy: destination string  space unallocated or cannot be written
+TEST 13: OK: Expected signal at tests/builtin/strcpy.c:35
+TEST 14: OK: Expected execution at tests/builtin/strcpy.c:36
+strncpy: overlapping memory areas
+TEST 15: OK: Expected signal at tests/builtin/strcpy.c:37
+TEST 16: OK: Expected execution at tests/builtin/strcpy.c:38
+strncpy: overlapping memory areas
+TEST 17: OK: Expected signal at tests/builtin/strcpy.c:39

src/plugins/e-acsl/tests/builtin/oracle_dev/strlen.e-acsl.err.log

+TEST 1: OK: Expected execution at tests/builtin/strlen.c:18
+TEST 2: OK: Expected execution at tests/builtin/strlen.c:19
+TEST 3: OK: Expected execution at tests/builtin/strlen.c:20
+TEST 4: OK: Expected execution at tests/builtin/strlen.c:21
+strlen: input string not NUL-terminated
+TEST 5: OK: Expected signal at tests/builtin/strlen.c:25
+strlen: input string not NUL-terminated
+TEST 6: OK: Expected signal at tests/builtin/strlen.c:26
+strlen: input string unallocated
+TEST 7: OK: Expected signal at tests/builtin/strlen.c:28