synchronize with frama-c master

c-testsuite/.frama-c/00210.parse/framac.ast

@@ -14,14 +14,14 @@ int ( __attribute__((__noinline__)) actual_function)(void)
 }
 
 /*@ assigns \result;
-    assigns \result \from (indirect: *( + (0 ..))), (indirect: param0);
+    assigns \result \from (indirect: *(param0 + (0 ..))), (indirect: param1);
  */
-int printf_va_1(char const *, int param0);
+int printf_va_1(char const *param0, int param1);
 
 /*@ assigns \result;
-    assigns \result \from (indirect: *( + (0 ..))), (indirect: param0);
+    assigns \result \from (indirect: *(param0 + (0 ..))), (indirect: param1);
  */
-int printf_va_2(char const *, int param0);
+int printf_va_2(char const *param0, int param1);
 
 int main(void)
 {

c-testsuite/.frama-c/00214.parse/framac.ast

@@ -3,8 +3,8 @@ typedef unsigned long size_t;
 size_t _brk_start;
 size_t _brk_end;
 /*@ assigns \result;
-    assigns \result \from (indirect: *( + (0 ..))); */
-int printf_va_1(char const *);
+    assigns \result \from (indirect: *(param0 + (0 ..))); */
+int printf_va_1(char const *param0);
 
 void *extend_brk(size_t size, size_t align)
 {
@@ -18,12 +18,12 @@ void *extend_brk(size_t size, size_t align)
 }
 
 /*@ assigns \result;
-    assigns \result \from (indirect: *( + (0 ..))); */
-int printf_va_2(char const *);
+    assigns \result \from (indirect: *(param0 + (0 ..))); */
+int printf_va_2(char const *param0);
 
 /*@ assigns \result;
-    assigns \result \from (indirect: *( + (0 ..))); */
-int printf_va_3(char const *);
+    assigns \result \from (indirect: *(param0 + (0 ..))); */
+int printf_va_3(char const *param0);
 
 static void get_args(int a, int b)
 {
@@ -33,8 +33,8 @@ static void get_args(int a, int b)
 }
 
 /*@ assigns \result;
-    assigns \result \from (indirect: *( + (0 ..))); */
-int printf_va_4(char const *);
+    assigns \result \from (indirect: *(param0 + (0 ..))); */
+int printf_va_4(char const *param0);
 
 void bla(void)
 {
@@ -60,12 +60,12 @@ _Bool chk(unsigned long addr, unsigned long limit, unsigned long size)
 }
 
 /*@ assigns \result;
-    assigns \result \from (indirect: *( + (0 ..))); */
-int printf_va_5(char const *);
+    assigns \result \from (indirect: *(param0 + (0 ..))); */
+int printf_va_5(char const *param0);
 
 /*@ assigns \result;
-    assigns \result \from (indirect: *( + (0 ..))); */
-int printf_va_6(char const *);
+    assigns \result \from (indirect: *(param0 + (0 ..))); */
+int printf_va_6(char const *param0);
 
 int main(void)
 {

c-testsuite/.frama-c/00217.parse/framac.ast

@@ -12,9 +12,9 @@ char t[10] =
    (char)'\000'};
 /*@ assigns \result;
     assigns \result
-      \from (indirect: *( + (0 ..))), (indirect: *(param0 + (0 ..)));
+      \from (indirect: *(param0 + (0 ..))), (indirect: *(param1 + (0 ..)));
  */
-int printf_va_1(char const *, char *param0);
+int printf_va_1(char const *param0, char *param1);
 
 int main(void)
 {

c-testsuite/.frama-c/00218.parse/framac.ast

@@ -32,8 +32,8 @@ int blah(void)
 }
 
 /*@ assigns \result;
-    assigns \result \from (indirect: *( + (0 ..))); */
-int printf_va_1(char const *);
+    assigns \result \from (indirect: *(param0 + (0 ..))); */
+int printf_va_1(char const *param0);
 
 int convert_like_real(tree convs)
 {

frama-c @ d518abcc

-Subproject commit 1b16ab8f41f92f6efaed2ff992f933c424d15d75
+Subproject commit d518abcc12ec3caa149c728aea351e509205b1c8

kilo/.frama-c/kilo.eva/alarms.csv

@@ -581,5 +581,5 @@ FRAMAC_SHARE/libc	string.h	121	memmove	precondition	Unknown	valid_src: valid_rea
 FRAMAC_SHARE/libc	string.h	131	memset	precondition	Unknown	valid_s: valid_or_empty(s, n)
 FRAMAC_SHARE/libc	string.h	141	strlen	precondition	Unknown	valid_string_s: valid_read_string(s)
 FRAMAC_SHARE/libc	unistd.h	867	ftruncate	assigns clause	Unknown	assigns \nothing;
-FRAMAC_SHARE/libc	unistd.h	867	ftruncate	from clause	Unknown	assigns \result \from \nothing;
+FRAMAC_SHARE/libc	unistd.h	867	ftruncate	from clause	Unknown	assigns \result \from __x0, __x1;
 FRAMAC_SHARE/libc	unistd.h	1141	write	precondition	Unknown	buf_has_room: \valid_read((char *)buf + (0 .. count - 1))

kilo/.frama-c/kilo.eva/warnings.log

@@ -2,6 +2,7 @@ kilo.c:985:[eva:garbled-mix] warning: The specification of function vsnprintf ha
 (s + (0 .. n - 1)).
 kilo.c:1269:[eva:locals-escaping] warning: locals {__va_args} escaping the scope of a block of main through E
 kilo.c:818:[kernel:annot:missing-spec] warning: Neither code nor specification for function ftruncate, generating default assigns from the prototype
+kilo.c:818:[eva:garbled-mix] warning: The specification of function ftruncate has generated a garbled mix for assigns clause \result.
 kilo.c:830:[eva:locals-escaping] warning: locals {__va_args_14} escaping the scope of a block of editorSave through E
 kilo.c:824:[eva:locals-escaping] warning: locals {__va_args} escaping the scope of a block of editorSave through E
 kilo.c:1014:[eva:locals-escaping] warning: locals {__va_args} escaping the scope of a block of editorFind through E