[eacsl] Add test for ACSL `check`

src/plugins/e-acsl/tests/constructs/acsl_check.c

+#include <stdio.h>
+
+/*@
+  check requires a != 0;
+  check ensures \result != 0;
+*/
+int f(int a) {
+  return a;
+}
+
+void g(int a, int * b) {
+  //@ check a / b[1] == 0;
+}
+
+int main() {
+  int a = 0;
+  int b[] = {1, 2, 3};
+  //@ check a == 1;
+  a = f(a);
+  fprintf(stderr, "SHOULD BE PRINTED IN EXECUTION LOG\n");
+  // Check that the RTEs are blocking even if the check is not.
+  g(a, b);
+  // Admits clauses are not translated
+  //@ admit a == 1;
+  //@ admit a == 2;
+  return a;
+}

src/plugins/e-acsl/tests/constructs/oracle_ci/acsl_check.res.oracle

+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/constructs/acsl_check.c:18: Warning: 
+  function __e_acsl_assert, behavior non_blocking: precondition got status invalid.
+[eva:alarm] tests/constructs/acsl_check.c:18: Warning: check got status invalid.
+[eva:alarm] tests/constructs/acsl_check.c:19: Warning: 
+  function __gen_e_acsl_f: precondition got status invalid.
+[eva:alarm] tests/constructs/acsl_check.c:4: Warning: 
+  function __e_acsl_assert, behavior non_blocking: precondition got status invalid.
+[eva:alarm] tests/constructs/acsl_check.c:5: Warning: 
+  function __e_acsl_assert, behavior non_blocking: precondition got status invalid.
+[eva:alarm] tests/constructs/acsl_check.c:5: Warning: 
+  function __gen_e_acsl_f: postcondition got status invalid.

src/plugins/e-acsl/tests/constructs/oracle_ci/gen_acsl_check.c

+/* Generated by Frama-C */
+#include "stddef.h"
+#include "stdio.h"
+char *__gen_e_acsl_literal_string;
+extern int __e_acsl_sound_verdict;
+
+/*@ check requires a ≢ 0;
+    check ensures \result ≢ 0; */
+int __gen_e_acsl_f(int a);
+
+int f(int a)
+{
+  return a;
+}
+
+void g(int a, int *b)
+{
+  {
+    int __gen_e_acsl_valid_read;
+    __e_acsl_store_block((void *)(& b),(size_t)8);
+    __e_acsl_assert((long)*(b + 1) != 0L,1,"RTE","g",
+                    "division_by_zero: (long)*(b + 1) != 0",
+                    "tests/constructs/acsl_check.c",12);
+    __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(b + 1),
+                                                  sizeof(int),(void *)b,
+                                                  (void *)(& b));
+    __e_acsl_assert(__gen_e_acsl_valid_read,1,"RTE","g",
+                    "mem_access: \\valid_read(b + 1)",
+                    "tests/constructs/acsl_check.c",12);
+    __e_acsl_assert(a / (long)*(b + 1) == 0L,0,"Assertion","g",
+                    "a / *(b + 1) == 0","tests/constructs/acsl_check.c",12);
+  }
+  /*@ check a / *(b + 1) ≡ 0; */ ;
+  __e_acsl_delete_block((void *)(& b));
+  return;
+}
+
+/*@ check requires a ≢ 0;
+    check ensures \result ≢ 0; */
+int __gen_e_acsl_f(int a)
+{
+  int __retres;
+  __e_acsl_assert(a != 0,0,"Precondition","f","a != 0",
+                  "tests/constructs/acsl_check.c",4);
+  __retres = f(a);
+  __e_acsl_assert(__retres != 0,0,"Postcondition","f","\\result != 0",
+                  "tests/constructs/acsl_check.c",5);
+  return __retres;
+}
+
+void __e_acsl_globals_init(void)
+{
+  static char __e_acsl_already_run = 0;
+  if (! __e_acsl_already_run) {
+    __e_acsl_already_run = 1;
+    __gen_e_acsl_literal_string = "SHOULD BE PRINTED IN EXECUTION LOG\n";
+    __e_acsl_store_block((void *)__gen_e_acsl_literal_string,
+                         sizeof("SHOULD BE PRINTED IN EXECUTION LOG\n"));
+    __e_acsl_full_init((void *)__gen_e_acsl_literal_string);
+    __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
+  }
+  return;
+}
+
+int main(void)
+{
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+  __e_acsl_globals_init();
+  int a = 0;
+  int b[3] = {1, 2, 3};
+  __e_acsl_store_block((void *)(b),(size_t)12);
+  __e_acsl_full_init((void *)(& b));
+  __e_acsl_assert(a == 1,0,"Assertion","main","a == 1",
+                  "tests/constructs/acsl_check.c",18);
+  /*@ check a ≡ 1; */ ;
+  a = __gen_e_acsl_f(a);
+  fprintf(stderr,__gen_e_acsl_literal_string); /* fprintf_va_1 */
+  g(a,b);
+  /*@ admit a ≡ 1; */ ;
+  /*@ admit a ≡ 2; */ ;
+  __e_acsl_delete_block((void *)(b));
+  __e_acsl_memory_clean();
+  return a;
+}
+
+

src/plugins/e-acsl/tests/constructs/oracle_dev/acsl_check.e-acsl.err.log

+tests/constructs/acsl_check.c: In function 'main'
+tests/constructs/acsl_check.c:18: Error: Assertion failed:
+	The failing predicate is:
+	a == 1.
+tests/constructs/acsl_check.c: In function 'f'
+tests/constructs/acsl_check.c:4: Error: Precondition failed:
+	The failing predicate is:
+	a != 0.
+tests/constructs/acsl_check.c: In function 'f'
+tests/constructs/acsl_check.c:5: Error: Postcondition failed:
+	The failing predicate is:
+	\result != 0.
+SHOULD BE PRINTED IN EXECUTION LOG