Merge branch 'fix/virgile/logic-pp-bs-string' into 'master'

[logic-preprocess] take literal backslash (`\\`) into account in ACSL strings

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

src/kernel_internals/parsing/logic_preprocess.mll

@@ -434,6 +434,9 @@ and string annot = parse
   | "\\\"" { is_newline:=CHAR;
              Buffer.add_string preprocess_buffer "\\\"";
              string annot lexbuf }
+  | "\\\\" { is_newline:=CHAR;
+             Buffer.add_string preprocess_buffer "\\\\";
+             string annot lexbuf }
   | eof { abort_preprocess "eof while parsing a string literal" }
   | _ as c { is_newline:=CHAR;
              Buffer.add_char preprocess_buffer c;

tests/spec/oracle/preprocess.res.oracle

@@ -13,6 +13,10 @@
 [eva] Recording results for f
 [eva] Done for function f
 [eva] tests/spec/preprocess.c:25: assertion got status valid.
+[eva] tests/spec/preprocess.c:28: 
+  cannot evaluate ACSL term, unsupported ACSL construct: constant strings
+[eva:alarm] tests/spec/preprocess.c:28: Warning: 
+  assertion 'backslash_string' got status unknown.
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -21,3 +25,31 @@
 [eva:final-states] Values at end of function main:
   y_0 ∈ {84}
   __retres ∈ {0}
+/* Generated by Frama-C */
+int x = 1;
+/*@ predicate test(int x) = x ≥ 42;
+ */
+int y = 1;
+/*@ requires x_0 ≥ 42;
+    
+    behavior default:
+      ensures test(\result) ∧ 2 ≡ 2;
+ */
+int f(int x_0)
+{
+  int __retres;
+  __retres = x_0 + 42;
+  return __retres;
+}
+
+int main(void)
+{
+  int __retres;
+  int y_0 = f(42);
+  /*@ assert x ≡ 1; */ ;
+  /*@ assert backslash_string: *("\\" + 0) ≡ '\\'; */ ;
+  __retres = 0;
+  return __retres;
+}
+
+

tests/spec/preprocess.c

 /* run.config
-   OPT: -pp-annot -eva @EVA_CONFIG@ -journal-disable
+   OPT: -eva @EVA_CONFIG@ -journal-disable -print
 */
 
 // see bts 1357
@@ -23,5 +23,8 @@ int f(int x) { return (x + MIN_X); }
 int main() {
   int y = f(MIN_X);
   //@ assert (x) == 1;
+
+  // BTS 2307
+  /*@ assert backslash_string: "\\"[0] == '\\'; */
   return 0;
 }