Ajout d'un test pour #714

tests/syntax/oracle/temporary_location.res.oracle

+[kernel] Parsing tests/syntax/temporary_location.c (with preprocessing)
+[kernel] __retres -> tests/syntax/temporary_location.c:7
+[kernel] __retres -> tests/syntax/temporary_location.c:7
+[kernel] __retres -> tests/syntax/temporary_location.c:7
+[kernel] __retres -> tests/syntax/temporary_location.c:17
+[kernel] tmp_0 -> tests/syntax/temporary_location.c:11
+[kernel] f -> tests/syntax/temporary_location.c:6
+[kernel] tmp_0 -> tests/syntax/temporary_location.c:11
+[kernel] __retres -> tests/syntax/temporary_location.c:17
+[kernel] x -> tests/syntax/temporary_location.c:15
+[kernel] tmp -> tests/syntax/temporary_location.c:16
+[kernel] x -> tests/syntax/temporary_location.c:15
+[kernel] x -> tests/syntax/temporary_location.c:15
+[kernel] x -> tests/syntax/temporary_location.c:15
+[kernel] x -> tests/syntax/temporary_location.c:15
+[kernel] y -> tests/syntax/temporary_location.c:16
+[kernel] tmp -> tests/syntax/temporary_location.c:16
+[kernel] __retres -> tests/syntax/temporary_location.c:17
+[kernel] y -> tests/syntax/temporary_location.c:16
+[kernel] __retres -> tests/syntax/temporary_location.c:17
+/* Generated by Frama-C */
+int f(void)
+{
+  int __retres;
+  __retres = 1;
+  return __retres;
+}
+
+int main(void)
+{
+  int __retres;
+  int tmp_0;
+  tmp_0 = f();
+  if (tmp_0) {
+    __retres = 0;
+    goto return_label;
+  }
+  else {
+    int tmp;
+    int x = 0;
+    tmp = x;
+    x ++;
+    int y = tmp + 1;
+    __retres = y + 3;
+    goto return_label;
+  }
+  return_label: return __retres;
+}
+
+

tests/syntax/temporary_location.c

+/* run.config
+   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+   OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -print
+*/
+
+int f(void) {
+    return 1;
+}
+
+int main(void) {
+    if(f()){
+        return 0;
+    }
+    else {
+        int x = 0;
+        int y = x++ + 1;
+        return y + 3;
+    }
+}

tests/syntax/temporary_location.ml

+open Cil_types
+
+class vis = object(_)
+  inherit Visitor.frama_c_inplace
+
+  method! vvrbl vi =
+    Kernel.result "%s -> %a" vi.vname Printer.pp_location vi.vdecl;
+    Cil.DoChildren
+  
+end
+
+let main () =
+  Ast.compute ();
+  Cil.visitCilFile (new vis :> Cil.cilVisitor) (Ast.get ())
+  
+let () =
+  Db.Main.extend main
+